English
Given a distance-like function d, a reflexivity, symmetry, triangle inequality, and a half-condition, the uniformity built from d has a HasBasis with thresholds ε>0.
Русский
Дано значение d, рефлексивность, симметричность, неравенство треугольника и условие half; получаемая униформность имеет базис по ε>0.
LaTeX
$$$\text{HasBasis }\mathcal{U}([d])((0,∞))\text{ with } \{ (x,y): d(x,y)<ε \}$$$
Lean4
theorem hasBasis_ofFun [AddCommMonoid M] [LinearOrder M] (h₀ : ∃ x : M, 0 < x) (d : X → X → M) (refl : ∀ x, d x x = 0)
(symm : ∀ x y, d x y = d y x) (triangle : ∀ x y z, d x z ≤ d x y + d y z)
(half : ∀ ε > (0 : M), ∃ δ > (0 : M), ∀ x < δ, ∀ y < δ, x + y < ε) :
𝓤[.ofFun d refl symm triangle half].HasBasis ((0 : M) < ·) (fun ε => {x | d x.1 x.2 < ε}) :=
hasBasis_biInf_principal'
(fun ε₁ h₁ ε₂ h₂ =>
⟨min ε₁ ε₂, lt_min h₁ h₂, fun _x hx => lt_of_lt_of_le hx (min_le_left _ _), fun _x hx =>
lt_of_lt_of_le hx (min_le_right _ _)⟩)
h₀
