isGreatest_gfp

Mathlib.Order.FixedPoints

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

English

The GFP is the greatest fixed point of f.

Русский

gfp — наибольшая фиксированная точка функции f.

LaTeX

$$$\mathrm{gfp}(f) \in \{a \mid f(a)=a\} \quad \text{and} \quad \forall x (f(x)=x) \Rightarrow \mathrm{gfp}(f) \ge x$.$$

Lean4

theorem isGreatest_gfp : IsGreatest (fixedPoints f) f.gfp :=
  f.dual.isLeast_lfp

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

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

Разделы

Аффилиация

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