English
If the topology on E is induced by a separating family of seminorms p, then E is a T1 space. Equivalently, if hp := WithSeminorms p and for every nonzero x there exists i with p_i(x) ≠ 0, then E is T1.
Русский
Если топология на E задаётся разделяющим семинормов p, то E является T1-пространством. Иными словами, если hp := WithSeminorms p и для каждого неположительного элемента x существует i с p_i(x) ≠ 0, тогда E — T1 пространство.
LaTeX
$$$hp:\\; WithSeminorms\\ p \\ ;\\ h:\\; \\forall x\\, x\\neq 0\\rightarrow \\exists i\\, p_i(x)\\neq 0 \\Rightarrow T1Space\\; E$$$
Lean4
/-- A separating family of seminorms induces a T₁ topology. -/
theorem T1_of_separating (hp : WithSeminorms p) (h : ∀ x, x ≠ 0 → ∃ i, p i x ≠ 0) : T1Space E :=
by
have := hp.topologicalAddGroup
refine IsTopologicalAddGroup.t1Space _ ?_
rw [← isOpen_compl_iff, hp.isOpen_iff_mem_balls]
rintro x (hx : x ≠ 0)
obtain ⟨i, pi_nonzero⟩ := h x hx
refine ⟨{ i }, p i x, by positivity, subset_compl_singleton_iff.mpr ?_⟩
rw [Finset.sup_singleton, mem_ball, zero_sub, map_neg_eq_map, not_lt]
