Theorems · Definition · general topology

MetricSpace.ofDistTopology

{α : Type u} →
  [inst : TopologicalSpace α] →
    (dist : α → α → ℝ) →
      (∀ (x : α), dist x x = 0) →
        (∀ (x y : α), dist x y = dist y x) →
          (∀ (x y z : α), dist x z ≤ dist x y + dist y z) →
            (∀ (s : Set α), IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ (y : α), dist x y < ε → y ∈ s) →
              (∀ (x y : α), dist x y = 0 → x = y) → MetricSpace α

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.

Defined in

Mathlib.Topology.MetricSpace.Defs

Cited by

0 results in Mathlib

Foundations

Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace