color

Mathlib.MeasureTheory.Covering.Besicovitch

URI: https://scilib.ai/kg/mathlib#Besicovitch.TauPackage.color

Lean4

/-- Group the balls into disjoint families, by assigning to a ball the smallest color for which
it does not intersect any already chosen ball of this color. -/
noncomputable def color : Ordinal.{u} → ℕ
  | i =>
    let A : Set ℕ :=
      ⋃ (j : { j // j < i }) (_ :
        (closedBall (p.c (p.index j)) (p.r (p.index j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
        {color j}
    sInf (univ \ A)
termination_by i => i
decreasing_by exact j.2

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru