Theorems · Theorem · measure theory

Besicovitch.TauPackage.color_lt

∀ {α : Type u_1} [inst : MetricSpace α] {β : Type u} [inst_1 : Nonempty β] (p : Besicovitch.TauPackage β α)
  {i : Ordinal.{u}}, i < p.lastStep → ∀ {N : ℕ}, IsEmpty (Besicovitch.SatelliteConfig α N p.τ) → p.color i < N

If there are no configurations of satellites with N+1 points, one never uses more than N distinct families in the Besicovitch inductive construction.

Defined in

Mathlib.MeasureTheory.Covering.Besicovitch

Cited by

1 results in Mathlib

Foundations

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

Assumes

MetricSpaceNonempty