uniformity_eq_of_hasBasis — Mathlib

English

A HasBasis structure on nhds(0) yields equality of uniform spaces with the seminorm structure.

Русский

Наличие базиса на 𝓝(0) даёт равенство униформных структур с семинормой.

LaTeX

$$$ (nhds 0).HasBasis p' s \\Rightarrow 𝓤 E = p.toAddGroupSeminorm.toSeminormedAddGroup.toUniformSpace. $$$

Lean4

theorem uniformity_eq_of_hasBasis {ι} [UniformSpace E] [IsUniformAddGroup E] [ContinuousConstSMul 𝕜 E] {p' : ι → Prop}
    {s : ι → Set E} (p : Seminorm 𝕜 E) (hb : (𝓝 0 : Filter E).HasBasis p' s) (h₁ : ∃ r, p.closedBall 0 r ∈ 𝓝 0)
    (h₂ : ∀ i, p' i → ∃ r > 0, p.ball 0 r ⊆ s i) : 𝓤 E = ⨅ r > 0, 𝓟 {x | p (x.1 - x.2) < r} := by
  rw [uniformSpace_eq_of_hasBasis p hb h₁ h₂]; rfl

Похожие утверждения