translationNumber_mono

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

← MathLib Explorer

English

Reiterating monotone property: τ is monotone.

Русский

Повторное утверждение монотонности: τ монотонна.

LaTeX

$$$ \text{Monotone } τ $$$

Lean4

theorem translationNumber_mono : Monotone τ := fun f g h =>
  le_of_tendsto_of_tendsto' f.tendsto_translation_number₀ g.tendsto_translation_number₀ fun n => by gcongr;
    exact pow_mono h _ _

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

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

Разделы

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

Аффилиация

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