Yoh Tanimoto

Tipo di issue: - Errore o mancanza nella dashboard Il grafico dei nuovi casi, alle 18:52 il 5 maggio 2021, non corrispondono ai dati giornalieri (per esempio, ieri 9116 nuovi...

Authentication failed for a repository with restricted permission

7

### The problem I cannot push a commit to a remote repository or publish a new branch to a repository where I only have a permission to edit non-master-branch. Other...

feat(MeasureTheory/Integral/linearRieszMarkovKakutani) prove that the Riesz content is indeed a content

17

define `rieszContentAux` under `Λ : C(X, ℝ) →ₗ[ℝ] ℝ) (hΛ : ∀ (f : C(X, ℝ)), 0 ≤ f → 0 ≤ Λ f)` and prove that it is a...

feat(Analysis/Normed/Group/SeparationQuotient): add normed lifts and `mk`

1

Define the `mk` and lifts of normed spaces and normed groups by the inseparable setoid as `NormedAddGroupHom`, `CLM`, etc. Motivation: In the GNS representation, operators in the original C^*-algebra are...

feat(Topology/UnitInterval): add unitInterval as Submonoid

3

add the definition of `UnitInterval` as Submonoid of `Real`. motivation: This enables the use of `prod_mem`. suggested in #12266

feat(Topology/UrysohnsLemma): add variations of Urysohn's lemma

3

add variations of Urysohn's lemma: - In a normal space `X`, for a closed set `t` and an open set `s` such that `t ⊆ s`, there is a continuous...