inseparable_iff_ker_uniformity — Mathlib

English

For x, y in a uniform space α, x and y are inseparable if and only if the pair (x, y) belongs to the kernel of the uniformity 𝓤α, i.e., is contained in every entourage in 𝓤α.

Русский

Пусть x, y ∈ α в равномерном пространстве; пары неразделимы тогда, когда (x, y) принадлежит ядру равномерности 𝓤α, то есть лежит во всех entourages 𝓤α.

LaTeX

$$$\text{Inseparable}(x,y) \;\Longleftrightarrow\; (x,y) \in (\mathcal{U}\,\alpha).\ker$$$

Lean4

theorem inseparable_iff_ker_uniformity {x y : α} : Inseparable x y ↔ (x, y) ∈ (𝓤 α).ker :=
  (𝓤 α).basis_sets.inseparable_iff_uniformity

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