t0Space_iff_uniformity' — Mathlib

English

A space α is T0 if and only if there exists a pairwise separation property expressed by a uniformity basis: x ≠ y implies there exists an i with p(i) such that (x, y) ∉ s(i).

Русский

Пусть α - пространство, для которого существует базис равномерности: x ≠ y тогда существует i, такое что p(i) и (x,y) ∉ s(i).

LaTeX

$$$T0Space(\alpha) \iff \text{Pairwise} \; (x,y) => \exists i, p(i) \land (x,y) \notin s(i)$$$

Lean4

theorem t0Space_iff_uniformity' : T0Space α ↔ Pairwise fun x y ↦ ∃ r ∈ 𝓤 α, (x, y) ∉ r := by
  simp [t0Space_iff_not_inseparable, inseparable_iff_ker_uniformity]

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