le_nextFixed

Mathlib.Order.FixedPoints

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

English

A refinement of GFP infimum bound with min-like constructions preserves bounds.

Русский

Уточнение нижних границ GFP через минимальные конструирования сохраняет границы.

LaTeX

$$$(\mathrm{gfp}\big(\mathrm{min}\, (\mathrm{const}(\alpha)\, x) \; f\big)) \le x$.$$

Lean4

theorem le_nextFixed {x : α} (hx : x ≤ f x) : x ≤ f.nextFixed x hx :=
  f.dual.prevFixed_le hx

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

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

Разделы

Аффилиация

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