semiconj_of_bijective_of_translationNumber_eq

English

If two lifts of circle homeomorphisms are bijective and share the same translation number, they are semiconjugate by a CircleDeg1Lift.

Русский

Если два подъёма окружностей являются биективными и имеют одинаковое число трансляции, они полусопряжены одним подъёмом CircleDeg1Lift.

LaTeX

$$$\forall f_1,f_2 : CircleDeg1Lift\,\, (Bijective\, f_1) \to (Bijective\, 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 `bijective f₁` and
`bijective f₂` to assume that `f₁` and `f₂` are homeomorphisms. -/
theorem semiconj_of_bijective_of_translationNumber_eq {f₁ f₂ : CircleDeg1Lift} (h₁ : Bijective f₁) (h₂ : Bijective f₂)
    (h : τ f₁ = τ f₂) : ∃ F : CircleDeg1Lift, Semiconj F f₁ f₂ :=
  semiconj_of_isUnit_of_translationNumber_eq (isUnit_iff_bijective.2 h₁) (isUnit_iff_bijective.2 h₂) h

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