lfp_le_map — Mathlib

English

The lfp respects map composition: lfp ≤ f(a) whenever lfp ≤ a and f is order-preserving.

Русский

Наименьшая фиксированная точка сохраняет композицию отображений: lfp ≤ f(a) при lfp ≤ a и монотонности f.

LaTeX

$$$\text{lfp} \le f(a)\;\text{при} \; \text{lfp} \le a$$$

Lean4

theorem lfp_le_map {a : α} (ha : f.lfp ≤ a) : f.lfp ≤ f a :=
  calc
    f.lfp = f f.lfp := f.map_lfp.symm
    _ ≤ f a := f.mono ha

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