English
From a distance function on a topological space that is compatible with the topology, one can construct a metric space structure.
Русский
Из функции расстояния совместимой с топологией можно построить метрическое пространство.
LaTeX
$$Definition of a MetricSpace from a compatible distance: $\\mathrm{MetricSpace\\,ofDistTopology}(dist, dist\\_self, dist\\_comm, dist\\_triangle, H, eq\\_of\\_dist\\_eq\\_zero)$.$$
Lean4
/-- Construct a metric space structure whose underlying topological space structure
(definitionally) agrees which a pre-existing topology which is compatible with a given distance
function. -/
def ofDistTopology {α : Type u} [TopologicalSpace α] (dist : α → α → ℝ) (dist_self : ∀ x : α, dist x x = 0)
(dist_comm : ∀ x y : α, dist x y = dist y x) (dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z)
(H : ∀ s : Set α, IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ y, dist x y < ε → y ∈ s)
(eq_of_dist_eq_zero : ∀ x y : α, dist x y = 0 → x = y) : MetricSpace α :=
{ PseudoMetricSpace.ofDistTopology dist dist_self dist_comm dist_triangle H with
eq_of_dist_eq_zero := eq_of_dist_eq_zero _ _ }
