Theorems · Definition · general topology

PiCountable.edist

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

Given a countable family of extended metric spaces, one may put an extended 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 edist x y = ∑' i, min (1/2)^(encode i) (edist (x i) (y i)).

Defined in

Mathlib.Topology.MetricSpace.PiNat

Cited by

5 results in Mathlib

Foundations

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

Assumes

EncodableEDist