Theorems · Definition · general topology

PiCountable.dist

{ι : Type u_2} → [Encodable ι] → {F : ι → Type u_3} → [(i : ι) → PseudoMetricSpace (F i)] → Dist ((i : ι) → F i)

Given a countable family of metric spaces, one may put a distance on their product Π i, E i. It is highly non-canonical, though, and therefore not registered as a global instance. The distance we use here is dist x y = ∑' i, min (1/2)^(encode i) (dist (x i) (y i)).

Defined in

Mathlib.Topology.MetricSpace.PiNat

Cited by

3 results in Mathlib

Foundations

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

Assumes

EncodablePseudoMetricSpace