ofFun — Mathlib

English

For a distance function d on a set X with appropriate axioms, the induced UniformSpace has a HasBasis given by the sets {x,y : d(x,y) < ε} for ε>0 (and a nonempty base).

Русский

Для функции расстояния d на наборе X с нужными аксиомами получаем HasBasis униформного пространства по множествам {x,y : d(x,y) < ε} при ε>0.

LaTeX

$$$\text{HasBasis }\mathcal{U}_{d}((0,∞)):\text{ basis consists of } \{(x,y): d(x,y) < ε\}$$$

Lean4

/-- Define a `UniformSpace` using a "distance" function. The function can be, e.g., the
distance in a (usual or extended) metric space or an absolute value on a ring. -/
def ofFun [AddCommMonoid M] [PartialOrder M] (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 < ε) :
    UniformSpace X :=
  .ofCore
    { uniformity := ⨅ r > 0, 𝓟 {x | d x.1 x.2 < r}
      refl := le_iInf₂ fun r hr => principal_mono.2 <| idRel_subset.2 fun x => by simpa [refl]
      symm :=
        tendsto_iInf_iInf fun r =>
          tendsto_iInf_iInf fun _ => tendsto_principal_principal.2 fun x hx => by rwa [mem_setOf, symm]
      comp :=
        le_iInf₂ fun r hr =>
          let ⟨δ, h0, hδr⟩ := half r hr;
          le_principal_iff.2 <|
            mem_of_superset (mem_lift' <| mem_iInf_of_mem δ <| mem_iInf_of_mem h0 <| mem_principal_self _)
              fun (x, z) ⟨y, h₁, h₂⟩ => (triangle _ _ _).trans_lt (hδr _ h₁ _ h₂) }

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