gfp_gfp

Mathlib.Order.FixedPoints

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

← MathLib Explorer

English

The GFP is a fixed point of f.

Русский

GFP является фиксированной точкой функции f.

LaTeX

$$$\mathrm{IsFixedPt}(\mathrm{coeff}(f), \mathrm{gfp}(f))$ or simply $f(\mathrm{gfp}(f)) = \mathrm{gfp}(f)$.$$

Lean4

theorem gfp_gfp (h : α →o α →o α) : (gfp.comp h).gfp = h.onDiag.gfp :=
  @lfp_lfp αᵒᵈ _ <| (OrderHom.dualIso αᵒᵈ αᵒᵈ).symm.toOrderEmbedding.toOrderHom.comp h.dual

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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