gfp_le

Mathlib.Order.FixedPoints

URI: https://scilib.ai/kg/mathlib#OrderHom.gfp_le

English

If a is an upper bound for all b with b ≤ f(b), then f.gfp ≤ a.

Русский

Если a является верхней границей для всех b, удовлетворяющих b ≤ f(b), то f.gfp ≤ a.

LaTeX

$$$\text{If } \forall b, (b \le f(b) \Rightarrow b \le a), \text{ then } f^{\mathrm{gfp}} \le a$.$$

Lean4

theorem gfp_le {a : α} (h : ∀ b, b ≤ f b → b ≤ a) : f.gfp ≤ a :=
  sSup_le h

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

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

Разделы

Аффилиация

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