Theorems · Theorem · general topology

PairReduction.iSup_edist_pairSet

∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T] {E : Type u_2}
  [inst_2 : PseudoEMetricSpace E],
  1 < a → ∀ (f : T → E), ⨆ s, ⨆ t, edist (f ↑s) (f ↑↑t) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)

Defined in

Mathlib.Topology.EMetricSpace.PairReduction

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpaceDecidableEqPseudoEMetricSpace