nfp_le_fp

Mathlib.SetTheory.Ordinal.FixedPoint

URI: https://scilib.ai/kg/mathlib#Ordinal.nfp_le_fp

English

If f is monotone and a ≤ b and f b ≤ b, then nfp f a ≤ b.

Русский

Если f монотонна, a ≤ b и f b ≤ b, то nfp f a ≤ b.

LaTeX

$$$$ \text{If } \operatorname{Monotone}(f) \text{ and } a \le b \text{ and } f b \le b, \ \ nfp f a \le b. $$$$

Lean4

theorem nfp_le_fp (H : Monotone f) {a b} (ab : a ≤ b) (h : f b ≤ b) : nfp f a ≤ b :=
  nfpFamily_le_fp (fun _ => H) ab fun _ => h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru