t0Space_iff_ker_uniformity — Mathlib

English

A space α is T0 if and only if the kernel of the uniformity 𝓤α equals the diagonal, i.e., (𝓤α).ker = diagonal α.

Русский

Пространство α является T0 тогда, когда ядро равномерности равно диагонали: (𝓤α).ker = диагональ(α).

LaTeX

$$$T0Space(α) \iff (𝓤(α)).ker = \Delta(α)$$$

Lean4

theorem t0Space_iff_ker_uniformity : T0Space α ↔ (𝓤 α).ker = diagonal α :=
  by
  simp_rw [t0Space_iff_uniformity, subset_antisymm_iff, diagonal_subset_iff, subset_def, Prod.forall, Filter.mem_ker,
    mem_diagonal_iff, iff_self_and]
  exact fun _ x s hs ↦ refl_mem_uniformity hs

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