English
The value defined by IsWellFounded.fix satisfies the defining equation with respect to previous values.
Русский
Значение, заданное через IsWellFounded.fix, удовлетворяет определяющему уравнению относительно предыдущих значений.
LaTeX
$$$\\forall C:(\\alpha \\to \\mathrm{Sort}^*),\\; (F:\\forall x:\\alpha, (\\forall y:\\alpha, r\\,y\\,x \\to C\\,y) \\to C\\,x) \\Rightarrow \\forall x,\\; IsWellFounded.fix r F\\ x = F x (\\lambda y _ , IsWellFounded.fix r F y)$$$
Lean4
/-- Creates data, given a way to generate a value from all that compare as less under a well-founded
relation. See also `IsWellFounded.fix_eq`. -/
def fix {C : α → Sort*} : (∀ x : α, (∀ y : α, r y x → C y) → C x) → ∀ x : α, C x :=
wf.fix
