fix_eq — Mathlib

English

The value of WellFoundedLT.fix is constructed from the preceding ones by the equality fix F x = F x (λ y x, WellFoundedLT.fix F y).

Русский

Значение WellFoundedLT.fix строится из предыдущих с помощью равенства: fix F x = F x (λ y, WellFoundedLT.fix F y).

LaTeX

$$$\\forall {C:α\\to \\mathrm{Sort*}} (F:\\forall x:α, (\\forall y:α, y

Lean4

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

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