le_gfp — Mathlib

English

Let α be a complete lattice and f: α → α monotone. If a ≤ f(a), then a ≤ gfp(f).

Русский

Пусть α — полная решетка и f: α → α монотонна. Тогда из a ≤ f(a) следует a ≤ gfp(f).

LaTeX

$$$\text{Let } \alpha \text{ be a complete lattice and } f: \alpha \to \alpha \text{ monotone. If } a \le f(a) \text{ then } a \le f^{\text{gfp}}$.$$

Lean4

theorem le_gfp {a : α} (h : a ≤ f a) : a ≤ f.gfp :=
  le_sSup h

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