t1Space — Mathlib

English

If R has a T1 topology, then V inherits T1 properties from SeparatingDual R V.

Русский

Если R имеет топологическое пространство T1, то V наследует T1-построение через SeparatingDual R V.

LaTeX

$$SeparatingDual Real V ⟹ t1Space V$$

Lean4

protected theorem t1Space [T1Space R] : T1Space V :=
  by
  apply t1Space_iff_exists_open.2 (fun x y hxy ↦ ?_)
  rcases exists_separating_of_ne (R := R) hxy with ⟨f, hf⟩
  exact ⟨f ⁻¹' {f y}ᶜ, isOpen_compl_singleton.preimage f.continuous, hf, by simp⟩

Похожие утверждения