lfp_le_fixed

Mathlib.Order.FixedPoints

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

English

The least fixed point of an endomorphism is a fixed point of the corresponding function.

Русский

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

LaTeX

$$$\text{IsFixedPt } f\; f.lfp$$$

Lean4

theorem lfp_le_fixed {a : α} (h : f a = a) : f.lfp ≤ a :=
  f.lfp_le h.le

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

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

Разделы

Аффилиация

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