nextFixed_le

Mathlib.Order.FixedPoints

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

← MathLib Explorer

English

If x ≤ f(x) then x ≤ nextFixed(x).

Русский

Если x ≤ f(x), тогда x ≤ nextFixed(x).

LaTeX

$$$x \le f(x) \Rightarrow x \le \mathrm{nextFixed}(x, hx).$$$

Lean4

theorem nextFixed_le {x : α} (hx : x ≤ f x) {y : fixedPoints f} (h : x ≤ y) : f.nextFixed x hx ≤ y :=
  Subtype.coe_le_coe.1 <| lfp_le _ <| sup_le h y.2.le

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

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

Разделы

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

Аффилиация

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