Theorems · Theorem · measure theory

Besicovitch.SatelliteConfig.h

∀ {α : Type u_1} [inst : MetricSpace α] {N : ℕ} {τ : ℝ} (self : Besicovitch.SatelliteConfig α N τ),
  Pairwise fun i j =>
    self.r i ≤ dist (self.c i) (self.c j) ∧ self.r j ≤ τ * self.r i ∨
      self.r j ≤ dist (self.c j) (self.c i) ∧ self.r i ≤ τ * self.r j

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