map_gfp

Mathlib.Order.FixedPoints

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

English

The GFP point is a fixed point of f.

Русский

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

LaTeX

$$$f(\mathrm{gfp}(f)) = \mathrm{gfp}(f).$$$

Lean4

@[simp]
theorem map_gfp : f f.gfp = f.gfp :=
  f.dual.map_lfp

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

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

Разделы

Аффилиация

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