map_le_gfp

Mathlib.Order.FixedPoints

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

English

If a ≤ gfp, then gfp ≤ f(a) and monotone mapping preserves GFP around a.

Русский

Если a ≤ gfp, тогда gfp ≤ f(a) и отображение сохраняет GFP вокруг a.

LaTeX

$$$a \le \mathrm{gfp}(f) \Rightarrow \mathrm{gfp}(f) \le f(a).$$$

Lean4

theorem map_le_gfp {a : α} (ha : a ≤ f.gfp) : f a ≤ f.gfp :=
  f.dual.lfp_le_map ha

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

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

Разделы

Аффилиация

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