English
Two uniform structures coincide if their basis around 0 matches the seminorm-induced structure.
Русский
Две униформные структуры совпадают, если их базисы вокруг 0 совпадают с базисом, порожденным семинормой.
LaTeX
$$$ 𝓤 E = p.toAddGroupSeminorm.toSeminormedAddGroup.toUniformSpace. $$$
Lean4
theorem uniformSpace_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) :
‹UniformSpace E› = p.toAddGroupSeminorm.toSeminormedAddGroup.toUniformSpace :=
by
refine IsUniformAddGroup.ext ‹_› p.toAddGroupSeminorm.toSeminormedAddCommGroup.to_isUniformAddGroup ?_
apply le_antisymm
· rw [← @comap_norm_nhds_zero E p.toAddGroupSeminorm.toSeminormedAddGroup, ← tendsto_iff_comap]
suffices Continuous p from this.tendsto' 0 _ (map_zero p)
rcases h₁ with ⟨r, hr⟩
exact p.continuous' hr
· rw [(@NormedAddCommGroup.nhds_zero_basis_norm_lt E p.toAddGroupSeminorm.toSeminormedAddGroup).le_basis_iff hb]
simpa only [subset_def, mem_ball_zero] using h₂
