English
A family of seminorms is separating if and only if it induces a T1 topology. In particular, (∀ x, x ≠ 0 → ∃ i, p_i x ≠ 0) iff T1Space E.
Русский
Семинормы разделяющие тогда и только тогда, когда они порождают топологию T1. В частности: (∀ x, x ≠ 0 → ∃ i, p_i x ≠ 0) эквивалентно T1Space E.
LaTeX
$$$hp:\\; WithSeminorms\\ p\\ ;\\ (\\forall x\\, x\\neq 0\\rightarrow \\exists i\\, p_i x\\neq 0)\\ \\iff\\ T1Space\\; E$$$
Lean4
/-- A family of seminorms inducing a T₁ topology is separating. -/
theorem separating_of_T1 [T1Space E] (hp : WithSeminorms p) (x : E) (hx : x ≠ 0) : ∃ i, p i x ≠ 0 :=
by
have := ((t1Space_TFAE E).out 0 9).mp (inferInstanceAs <| T1Space E)
by_contra! h
refine hx (this ?_)
rw [hp.hasBasis_zero_ball.specializes_iff]
rintro ⟨s, r⟩ (hr : 0 < r)
simp only [ball_finset_sup_eq_iInter _ _ _ hr, mem_iInter₂, mem_ball_zero, h, hr, forall_true_iff]
