Theorems · Theorem · general topology

PairReduction.edist_le_of_mem_pairSet

∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {n : ℕ} {J : Finset T} [inst_1 : DecidableEq T],
  1 < a → ↑J.card ≤ a ^ n → ∀ {s t : T}, (s, t) ∈ PairReduction.pairSet J a c → edist s t ≤ ↑n * c

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

PseudoEMetricSpaceDecidableEq