tendsto_translation_number₀

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

URI: https://scilib.ai/kg/mathlib#CircleDeg1Lift.tendsto_translation_number₀

← MathLib Explorer

English

The translation number function is monotone: if f ≤ g then τ(f) ≤ τ(g).

Русский

Функция числа трансляции монотонна: если f ≤ g, то τ(f) ≤ τ(g).

LaTeX

$$$ \text{Monotone}(τ) $$$

Lean4

theorem tendsto_translation_number₀ : Tendsto (fun n : ℕ => (f ^ n) 0 / n) atTop (𝓝 <| τ f) :=
  (tendsto_add_atTop_iff_nat 1).1 (mod_cast f.tendsto_translation_number₀')

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

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

Разделы

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

Аффилиация

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