specializes_iff_uniformity — Mathlib

English

In a uniform space, specialization of points is characterized by the basis of the uniformity: x specializes y iff for every basis set s_i with i in index set, (x,y) ∈ s_i whenever p i holds.

Русский

В равномерном пространстве специализация точек задаётся через базис униформности: x specializes y тогда и только если для каждого базисного множества s_i в индексе i, (x,y) ∈ s_i при выполнении условия p i.

LaTeX

$$$\\forall x,y,\\ specializ es(x,y) \\iff \\forall i, p(i) \\to (x,y) \\in s(i)$$$

Lean4

theorem specializes_iff_uniformity {ι : Sort*} {p : ι → Prop} {s : ι → Set (α × α)} (h : (𝓤 α).HasBasis p s) {x y : α} :
    x ⤳ y ↔ ∀ i, p i → (x, y) ∈ s i :=
  (nhds_basis_uniformity h).specializes_iff

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