Theorems · Definition · general topology

PiNat.metricSpace

{E : ℕ → Type u_1} →
  [inst : (n : ℕ) → TopologicalSpace (E n)] → [∀ (n : ℕ), DiscreteTopology (E n)] → MetricSpace ((n : ℕ) → E n)

Metric space structure on Π (n : ℕ), E n when the spaces E n have the discrete topology, 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. Warning: this definition makes sure that the topology is defeq to the original product topology, but it does not take care of a possible uniformity. If the E n have a uniform structure, then there will be two non-defeq uniform structures on Π n, E n, the product one and the one coming from the metric structure. In this case, use metricSpaceOfDiscreteUniformity instead.

Defined in

Mathlib.Topology.MetricSpace.PiNat

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceDiscreteTopology