t0Space_iff_uniformity — Mathlib

English

A space α is T0 if and only if for any x ≠ y there exists an entourage r ∈ 𝓤α with (x, y) ∉ r.

Русский

Пространство α является T0 тогда и только тогда, когда для любых различных x, y существует entourages r ∈ 𝓤α такие, что (x, y) ∉ r.

LaTeX

$$$T0Space(\alpha) \iff \forall x,y,\, x\neq y \Rightarrow \exists r \in 𝓤(\alpha), (x,y) \notin r$$$

Lean4

theorem t0Space_iff_uniformity : T0Space α ↔ ∀ x y, (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y := by
  simp only [t0Space_iff_inseparable, inseparable_iff_ker_uniformity, mem_ker]

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