iterate_monotone

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

URI: https://scilib.ai/kg/mathlib#CircleDeg1Lift.iterate_monotone

English

For each natural number n, the map f ↦ f^[n] is monotone with respect to the pointwise order.

Русский

Для каждого натурального n отображение f ↦ f^{[n]} монотонно по точечному порядку.

LaTeX

$$$ \forall n \in \mathbb{N}, \; \text{Monotone}(f \mapsto f^{[n]}). $$$

Lean4

theorem iterate_monotone (n : ℕ) : Monotone fun f : CircleDeg1Lift => f^[n] := fun f _ h =>
  f.monotone.iterate_le_of_le h _

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

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

Разделы

Аффилиация

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