English
A family of seminorms is separating iff it induces a T1 topology. More precisely, under hp, the separating condition (∀ x, x ≠ 0 → ∃ i, p_i x ≠ 0) is equivalent to T1Space E.
Русский
Семинормы разделяющие эквивалентны тому, что порождаемая ими топология является T1. При условии hp разделяющее свойство (∀ x, x ≠ 0 → ∃ i, p_i x ≠ 0) эквивалентно T1Space E.
LaTeX
$$$hp:\\; WithSeminorms\\ p\\;\\Rightarrow\\ (\\forall x, x\\neq 0 \\rightarrow \\exists i,\\ p_i x \\neq 0) \\iff T1Space\\; E$$$
Lean4
theorem withSeminorms_of_nhds [IsTopologicalAddGroup E] (p : SeminormFamily 𝕜 E ι)
(h : 𝓝 (0 : E) = p.moduleFilterBasis.toFilterBasis.filter) : WithSeminorms p :=
by
refine ⟨IsTopologicalAddGroup.ext inferInstance p.addGroupFilterBasis.isTopologicalAddGroup ?_⟩
rw [AddGroupFilterBasis.nhds_zero_eq]
exact h
