le_lfp

Mathlib.Order.FixedPoints

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

English

If a is a lower bound of f.lfp, then a ≤ f.lfp; equivalently, f.lfp is the greatest lower bound compatible with f.

Русский

Если a ниже, чем f.lfp, тогда a ≤ f.lfp; эквивалентно тому, что f.lfp является наибольшей нижней гранью.

LaTeX

$$$a \le f.lfp \quad\Rightarrow\quad a \le f.lfp$$$

Lean4

theorem le_lfp {a : α} (h : ∀ b, f b ≤ b → a ≤ b) : a ≤ f.lfp :=
  le_sInf h

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

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

Разделы

Аффилиация

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