Theorems · Definition · general topology

PiNat.metricSpaceOfDiscreteUniformity

{E : ℕ → Type u_2} →
  [inst : (n : ℕ) → UniformSpace (E n)] →
    (∀ (n : ℕ), uniformity (E n) = Filter.principal SetRel.id) → MetricSpace ((n : ℕ) → E n)

Metric space structure on Π (n : ℕ), E n when the spaces E n have the discrete uniformity, where the distance is given by dist x y = (1/2)^n, where n is the smallest index where x and y differ. Not registered as a global instance by default.

Defined in

Mathlib.Topology.MetricSpace.PiNat

Cited by

0 results in Mathlib

Foundations

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

Assumes

UniformSpace