translationNumber_eq_of_semiconjBy

English

If g1 and g2 are semiconjugate by f, then τ g1 = τ g2.

Русский

Если g1 и g2 связаны полуподстановлением через f, то τ(g1) = τ(g2).

LaTeX

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

Lean4

theorem translationNumber_eq_of_semiconjBy {f g₁ g₂ : CircleDeg1Lift} (H : SemiconjBy f g₁ g₂) : τ g₁ = τ g₂ :=
  translationNumber_eq_of_dist_bounded 2 fun n => le_of_lt <| dist_map_zero_lt_of_semiconjBy <| H.pow_right n

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