Theorems · Theorem · general topology

PiCountable.dist_summable

∀ {ι : Type u_2} [inst : Encodable ι] {F : ι → Type u_3} [inst_1 : (i : ι) → PseudoMetricSpace (F i)]
  (x y : (i : ι) → F i), Summable fun i => min (2⁻¹ ^ Encodable.encode i) (dist (x i) (y i))

Defined in

Mathlib.Topology.MetricSpace.PiNat

Cited by

1 results in Mathlib

Foundations

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

Assumes

EncodablePseudoMetricSpace