isLeast_lfp_le — Mathlib

English

Let α be a complete lattice and f: α → α be monotone. Then the least post-fixed point of f, namely f.lfp, is the least element a such that f(a) ≤ a.

Русский

Пусть α — полная решетка и f: α → α монотонна. Тогда наименьшая постфиксная точка отображения f равна f.lfp и является наименьшим элементом a, удовлетворяющим f(a) ≤ a.

LaTeX

$$$\text{Let } \alpha \text{ be a complete lattice and } f: \alpha \to \alpha \text{ monotone. Then } f\!\left(\mathrm{lfp}(f)\right) \le \mathrm{lfp}(f) \text{ and }\forall a (f(a) \le a \Rightarrow \mathrm{lfp}(f) \le a).$$$

Lean4

theorem isLeast_lfp_le : IsLeast {a | f a ≤ a} f.lfp :=
  ⟨f.map_lfp.le, fun _ => f.lfp_le⟩

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