Theorems · Definition · general topology

PairReduction.logSizeBallSeq

{T : Type u_1} →
  [PseudoEMetricSpace T] →
    [DecidableEq T] → (J : Finset T) → J.Nonempty → ENNReal → ENNReal → ℕ → PairReduction.logSizeBallStruct T

We recursively define a log-size ball sequence (Vᵢ, tᵢ, rᵢ) by * V₀ = J, t₀ is chosen arbitrarily in J, r₀ is the log-size radius of t₀ in V₀ * Vᵢ₊₁ = Vᵢ \ {x ∈ V | d(t, x) ≤ (rᵢ - 1)c}, tᵢ₊₁ is chosen arbitrarily in Vᵢ₊₁, rᵢ₊₁ is the log-size radius of tᵢ₊₁ in Vᵢ₊₁.

Defined in

Mathlib.Topology.EMetricSpace.PairReduction

Cited by

26 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpaceDecidableEq