English
If two lifts of circle homeomorphisms have the same translation number and both are bijective, then they are semiconjugate by some CircleDeg1Lift.
Русский
Пусть два подъёма окружностей, являющиеся биективными отображениями, имеют одинаковое число трансляции. Тогда существует подъём F типа CircleDeg1Lift, такой что F полуобразует один подъём в другой.
LaTeX
$$$\forall f_1,f_2 : CircleDeg1Lift\,\, (IsUnit\, f_1) \to (IsUnit\, f_2) \to (\tau f_1 = \tau f_2) \to \exists F:\ CircleDeg1Lift, \ Semiconj\ F\ f_1\ f_2$$$
Lean4
/-- If two lifts of circle homeomorphisms have the same translation number, then they are
semiconjugate by a `CircleDeg1Lift`. This version uses assumptions `IsUnit f₁` and `IsUnit f₂`
to assume that `f₁` and `f₂` are homeomorphisms. -/
theorem semiconj_of_isUnit_of_translationNumber_eq {f₁ f₂ : CircleDeg1Lift} (h₁ : IsUnit f₁) (h₂ : IsUnit f₂)
(h : τ f₁ = τ f₂) : ∃ F : CircleDeg1Lift, Semiconj F f₁ f₂ :=
by
rcases h₁, h₂ with ⟨⟨f₁, rfl⟩, ⟨f₂, rfl⟩⟩
exact units_semiconj_of_translationNumber_eq h
