pow_monotone

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

English

For fixed n, the map f ↦ f^n is monotone with respect to the pointwise order on CircleDeg1Lift.

Русский

Для фиксированного n отображение f ↦ f^n монотонно по точечному порядку CircleDeg1Lift.

LaTeX

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

Lean4

theorem pow_monotone (n : ℕ) : Monotone fun f : CircleDeg1Lift => f ^ n := fun _ _ h => pow_mono h n

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

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

Разделы

Аффилиация

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