le_lfpApprox — Mathlib

English

If initial data bounds an element x above the fixed point, then for any ordinal a, the lfpApprox follows a certain inequality and equality pattern with the predecessor steps.

Русский

Если начальные данные ограничивают элемент x выше фиксированной точки, то для любого ординала a аппроксимация lfp следует определённой схеме неравенств и равенств с предыдущими шагами.

LaTeX

$$$ (0 \\le a) \\rightarrow \\mathrm{lfpApprox}(f,x,a+1) = f(\\mathrm{lfpApprox}(f,x,a)) $$$

Lean4

theorem le_lfpApprox {a : Ordinal} : x ≤ lfpApprox f x a :=
  by
  rw [lfpApprox]
  apply le_sSup
  simp only [exists_prop, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, true_or]

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