English
Given a distance function dist and a topology on α compatible with it, one can define a pseudo-metric space structure whose open sets correspond to that topology.
Русский
Дано расстояние и топология, совместимая с ним; можно определить псевдометрическое пространство, структура которого согласуется с данной топологией.
LaTeX
$$$\text{PseudoMetricSpace}(\alpha)$ со структурой dist, dist\_self, dist\_triangle совместима с топологией H.$$
Lean4
/-- Construct a pseudo-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) : PseudoMetricSpace α :=
{ dist := dist
dist_self := dist_self
dist_comm := dist_comm
dist_triangle := dist_triangle
toUniformSpace :=
(UniformSpace.ofDist dist dist_self dist_comm dist_triangle).replaceTopology <|
TopologicalSpace.ext_iff.2 fun s ↦
(H s).trans <|
forall₂_congr fun x _ ↦
((UniformSpace.hasBasis_ofFun (exists_gt (0 : ℝ)) dist dist_self dist_comm dist_triangle
UniformSpace.ofDist_aux).comap
(Prod.mk x)).mem_iff.symm
uniformity_dist := rfl
toBornology := Bornology.ofDist dist dist_comm dist_triangle
cobounded_sets := rfl }
