map_le_lfp

Mathlib.Order.FixedPoints

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

English

If a ≤ f.lfp then f a ≤ f.lfp; the map preserves the fixed-point bound.

Русский

Если a ≤ f.lfp, то f(a) ≤ f.lfp; отображение сохраняет предел фиксированной точки.

LaTeX

$$$a \le f.lfp \;\Rightarrow\; f(a) \le f.lfp$$$

Lean4

theorem map_le_lfp {a : α} (ha : a ≤ f.lfp) : f a ≤ f.lfp :=
  f.le_lfp fun _ hb => (f.mono <| le_sInf_iff.1 ha _ hb).trans hb

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

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

Разделы

Аффилиация

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