isFixedPt_gfp

Mathlib.Order.FixedPoints

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

English

The greatest fixed point of f is a fixed point of f.

Русский

Наибольшая фиксированная точка f является фиксированной точкой f.

LaTeX

$$$\text{Let } f: \alpha \to \alpha \text{ be monotone. Then } f(\mathrm{gfp}(f)) = \mathrm{gfp}(f).$$$

Lean4

theorem isFixedPt_gfp : IsFixedPt f f.gfp :=
  f.dual.isFixedPt_lfp

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

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

Разделы

Аффилиация

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