le_iterate_of_le

Mathlib.Order.Iterate

URI: https://scilib.ai/kg/mathlib#Monotone.le_iterate_of_le

← MathLib Explorer

English

If id ≤ f, then id ≤ f^[n] for every n.

Русский

Если тождество ≤ f, тогда идент. ≤ f^[n] для любого n.

LaTeX

$$$\\mathrm{id} \\le f \\Rightarrow \\forall n, \\mathrm{id} \\le f^{[n]}.$$$

Lean4

/-- If `f ≤ g` and `g` is monotone, then `f^[n] ≤ g^[n]`. -/
theorem le_iterate_of_le {g : α → α} (hg : Monotone g) (h : f ≤ g) (n : ℕ) : f^[n] ≤ g^[n] :=
  hg.dual.iterate_le_of_le h n

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

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

Разделы

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

Аффилиация

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