translationNumber_eq_of_semiconj

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

← MathLib Explorer

English

If f semiconjugates g1 to g2, then τ g1 = τ g2.

Русский

Если f полуподстановляет g1 к g2, тогда τ g1 = τ g2.

LaTeX

$$$ \forall f,g_1,g_2, \text{Semiconj}(f,g_1,g_2) \Rightarrow τ(g_1) = τ(g_2). $$$

Lean4

theorem translationNumber_eq_of_semiconj {f g₁ g₂ : CircleDeg1Lift} (H : Function.Semiconj f g₁ g₂) : τ g₁ = τ g₂ :=
  translationNumber_eq_of_semiconjBy <| semiconjBy_iff_semiconj.2 H

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

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

Разделы

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

Аффилиация

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