isGreatest_gfp_le

Mathlib.Order.FixedPoints

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

English

The GFP is the greatest a with a ≤ f(a).

Русский

gfp — наибольшая такая точка, что a ≤ f(a).

LaTeX

$$$\{a \in \alpha \mid a \le f(a)\}$ имеет наибольший элемент, который равен \mathrm{gfp}(f).$$$

Lean4

theorem isGreatest_gfp_le : IsGreatest {a | a ≤ f a} f.gfp :=
  f.dual.isLeast_lfp_le

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

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

Разделы

Аффилиация

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