index — Mathlib

Lean4
/-- Choose inductively large balls with centers that are not contained in the union of already
chosen balls. This is a transfinite induction. -/
noncomputable def index : Ordinal.{u} → β
  | i =>
    -- `Z` is the set of points that are covered by already constructed balls
    let Z :=
      ⋃ j : { j // j < i },
        ball (p.c (index j))
          (p.r (index j))
            -- `R` is the supremum of the radii of balls with centers not in `Z`

    let R := iSup fun b : { b : β // p.c b ∉ Z } => p.r b
    Classical.epsilon fun b : β => p.c b ∉ Z ∧ R ≤ p.τ * p.r b
termination_by i => i
decreasing_by exact j.2
Похожие утверждения