Theorems · Theorem · general topology

EMetric.pair_reduction

∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a : ENNReal} {n : ℕ} {J : Finset T},
  ↑J.card ≤ a ^ n →
    ∀ (c : ENNReal) (E : Type u_2) [inst_1 : PseudoEMetricSpace E],
      ∃ K ⊆ J ×ˢ J,
        ↑K.card ≤ a * ↑J.card ∧
          (∀ (s t : T), (s, t) ∈ K → edist s t ≤ ↑n * c) ∧
            ∀ (f : T → E), ⨆ s, ⨆ t, edist (f ↑s) (f ↑↑t) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)

Pair Reduction: Given pseudometric spaces T and E, c ≥ 0, and a finite subset J of T such that |J| ≤ aⁿ for some a ≥ 0 and n : ℕ, pair_reduction states that there exists a set K ⊆ J² such that for any function f : T → E: 1. |K| ≤ a|J| 2. ∀ (s, t) ∈ K, d(s, t) ≤ cn 3. sup_{s, t ∈ J : d(s, t) ≤ c} d(f(s), f(t)) ≤ 2 sup_{(s, t) ∈ K} d(f(s), f(t))

Defined in

Mathlib.Topology.EMetricSpace.PairReduction

Cited by

0 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpacePseudoEMetricSpace