isLeast_lfp — Mathlib

English

Let α be a complete lattice and f: α → α be monotone. Then the least fixed point of f is the least element of the set {a ∈ α | f(a) = a}.

Русский

Пусть α является полной решёткой, а f: α → α монотонна. Тогда наименьшая фиксированная точка f есть наименьшее элемент множества {a ∈ α | f(a) = a}.

LaTeX

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

Lean4

theorem isLeast_lfp : IsLeast (fixedPoints f) f.lfp :=
  ⟨f.isFixedPt_lfp, fun _ => f.lfp_le_fixed⟩

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