English
From a distance, construct a uniform basis using neighborhoods { (a,b) : edist(a,b) < ε }.
Русский
Исходя из расстояния, строится базис равномерности с окрестностями { (a,b) : edist(a,b) < ε }.
LaTeX
$$$ (\text{uniformSpaceOfEDist})\text{Basis} \Rightarrow (\mathcal{U} α).HasBasis \, \{ε>0\} \{ (a,b): edist(a,b)<ε \} $$$
Lean4
/-- Creating a uniform space from an extended distance. We assume that
there is a preexisting topology, for which the neighborhoods can be expressed using the distance,
and we make sure that the uniform space structure we construct has a topology which is defeq
to the original one. -/
@[reducible]
noncomputable def uniformSpaceOfEDistOfHasBasis [TopologicalSpace α] (edist : α → α → ℝ≥0∞)
(edist_self : ∀ x : α, edist x x = 0) (edist_comm : ∀ x y : α, edist x y = edist y x)
(edist_triangle : ∀ x y z : α, edist x z ≤ edist x y + edist y z)
(basis : ∀ x, (𝓝 x).HasBasis (fun c ↦ 0 < c) (fun c ↦ {y | edist x y < c})) : UniformSpace α :=
.ofFunOfHasBasis edist edist_self edist_comm edist_triangle
(fun ε ε0 =>
⟨ε / 2, ENNReal.half_pos ε0.ne', fun _ h₁ _ h₂ => (ENNReal.add_lt_add h₁ h₂).trans_eq (ENNReal.add_halves _)⟩)
basis
