English
Characterization of uniformities by a distance function D: a filter U on α×α equals the biinf of principal filters of { (a,b) : D(a,b) < ε } for ε > z.
Русский
Характеризация равномерностей по функции расстояния D: фильтр U на α×α равен biInf (главные фильтры) множества { (a,b) : D(a,b) < ε } при ε > z.
LaTeX
$$$ U = \bigsqcap_{\epsilon > z} 𝓟\{ p : α×α \mid D(p.1,p.2) < \epsilon \} $$$
Lean4
/-- Characterizing uniformities associated to a (generalized) distance function `D`
in terms of the elements of the uniformity. -/
theorem uniformity_dist_of_mem_uniformity [LT β] {U : Filter (α × α)} (z : β) (D : α → α → β)
(H : ∀ s, s ∈ U ↔ ∃ ε > z, ∀ {a b : α}, D a b < ε → (a, b) ∈ s) : U = ⨅ ε > z, 𝓟 {p : α × α | D p.1 p.2 < ε} :=
HasBasis.eq_biInf ⟨fun s => by simp only [H, subset_def, Prod.forall, mem_setOf]⟩
