Theorems · Theorem · measure theory

Besicovitch.SatelliteConfig.hlast

∀ {α : Type u_1} [inst : MetricSpace α] {N : ℕ} {τ : ℝ} (self : Besicovitch.SatelliteConfig α N τ),
  ∀ i < Fin.last N, self.r i ≤ dist (self.c i) (self.c (Fin.last N)) ∧ self.r (Fin.last N) ≤ τ * self.r i

Defined in

Mathlib.MeasureTheory.Covering.Besicovitch

Cited by

3 results in Mathlib

Foundations

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

Assumes

MetricSpace