antitone_iterate_of_le_id

Mathlib.Order.Iterate

URI: https://scilib.ai/kg/mathlib#Function.antitone_iterate_of_le_id

English

If id ≤ f, then the sequence m ↦ f^[m] is antitone in m.

Русский

Если id ≤ f, тогда последовательность m ↦ f^[m] убывающая по m.

LaTeX

$$$\\text{If } id \\le f, \\; \\text{then } m \\mapsto f^{[m]} \\text{ is antitone.}$$$

Lean4

theorem antitone_iterate_of_le_id (h : f ≤ id) : Antitone fun m => f^[m] := fun m n hmn =>
  @monotone_iterate_of_id_le αᵒᵈ _ f h m n hmn

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

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

Разделы

Аффилиация

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