Theorems · Theorem · functional analysis

Seminorm.uniformSpace_eq_of_hasBasis

∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {ι : Sort u_12} [inst_3 : UniformSpace E] [IsUniformAddGroup E] [ContinuousConstSMul 𝕜 E] {p' : ι → Prop}
  {s : ι → Set E} (p : Seminorm 𝕜 E),
  (nhds 0).HasBasis p' s →
    (∃ r, p.closedBall 0 r ∈ nhds 0) →
      (∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i) → inst_3 = PseudoMetricSpace.toUniformSpace

Defined in

Mathlib.Analysis.Seminorm

Cited by

1 results in Mathlib

Foundations

Depth 162 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldAddCommGroupModuleUniformSpaceIsUniformAddGroupContinuousConstSMul