Theorems · Theorem · general topology

Metric.ediam_pi_le_of_le

∀ {ι : Type u_3} {X : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → PseudoEMetricSpace (X i)]
  {s : (i : ι) → Set (X i)} {c : ENNReal}, (∀ (b : ι), Metric.ediam (s b) ≤ c) → Metric.ediam (Set.univ.pi s) ≤ c

Defined in

Mathlib.Topology.EMetricSpace.Diam

Cited by

3 results in Mathlib

Foundations

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

Assumes

FintypePseudoEMetricSpace