fix_eq — Mathlib

English

The value from IsWellFounded.fix is built from the previous ones as specified.

Русский

Значение из IsWellFounded.fix строится из предыдущих значений в соответствии с заданием.

LaTeX

$$$\\forall {C} (F : \\alpha \\to (\\forall y:\\alpha, r\\,y\\,x \\to C\\,y) \\to C\\,x), \\; \\forall x,\\\\; IsWellFounded.fix r F x = F x (\\\\lambda y _, IsWellFounded.fix r F y)$$$

Lean4

/-- The value from `IsWellFounded.fix` is built from the previous ones as specified. -/
theorem fix_eq {C : α → Sort*} (F : ∀ x : α, (∀ y : α, r y x → C y) → C x) :
    ∀ x, fix r F x = F x fun y _ => fix r F y :=
  wf.fix_eq F

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