gfpApprox_le — Mathlib

English

The GFP approximation as a function of the index is monotone with respect to the index in the dual lattice, mirroring the lfpApprox monotonicity.

Русский

Аппроксимация GFP как функция индекса монотонна по индексу в двойной решётке, отражая монотонность lfpApprox.

LaTeX

$$$ \\text{Monotone}(\\mathrm{gfpApprox}) $$$

Lean4

theorem gfpApprox_le {a : Ordinal} : gfpApprox f x a ≤ x :=
  le_lfpApprox f.dual x

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