fix_eq — Mathlib

English

The value produced by WellFoundedGT.fix is defined by a recursive equation: fix F x equals F x applied to the function y ↦ fix F y.

Русский

Значение, получаемое через WellFoundedGT.fix, задается рекурсивно: fix F x = F x (λ y, fix F y).

LaTeX

$$$\text{WellFoundedGT.fix } F x = F x \bigl( \lambda y, \text{WellFoundedGT.fix } F y \bigr)$$$

Lean4

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

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