wf_isOption — Mathlib

English

The relation IsOption on games is well-founded; there exists a foundation that every nonempty chain of options descends finitely.

Русский

Отношение IsOption на играх является нормально основанным; существует основание, что любая бесконечная последовательность ходов опций заканчивается.

LaTeX

$$$\operatorname{WellFounded}(\mathrm{IsOption})$$$

Lean4

theorem wf_isOption : WellFounded IsOption :=
  ⟨fun x =>
    moveRecOn x fun x IHl IHr =>
      Acc.intro x fun y h => by
        induction h with
        | moveLeft i => exact IHl i
        | moveRight j => exact IHr j⟩

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