units_semiconj_of_translationNumber_eq

English

If a natural n satisfies n < τ(f), then for all x, x + n < f(x).

Русский

Если натуральное n удовлетворяет n < τ(f), тогда для всех x выполняется x + n < f(x).

LaTeX

$$$$ \\forall f, \\forall n \\in \\mathbb{N}, \\ n < \\tau f \\Rightarrow \\forall x \\in \\mathbb{R}, \\ x + n < f(x). $$$$

Lean4

/-- If two lifts of circle homeomorphisms have the same translation number, then they are
semiconjugate by a `CircleDeg1Lift`. This version uses arguments `f₁ f₂ : CircleDeg1Liftˣ`
to assume that `f₁` and `f₂` are homeomorphisms. -/
theorem units_semiconj_of_translationNumber_eq {f₁ f₂ : CircleDeg1Liftˣ} (h : τ f₁ = τ f₂) :
    ∃ F : CircleDeg1Lift, Semiconj F f₁ f₂ :=
  have :
    ∀ n : Multiplicative ℤ,
      τ ((Units.coeHom _).comp (zpowersHom _ f₁) n) = τ ((Units.coeHom _).comp (zpowersHom _ f₂) n) :=
    fun n ↦ by simp [h]
  (semiconj_of_group_action_of_forall_translationNumber_eq _ _ this).imp fun F hF => by
    simpa using hF (Multiplicative.ofAdd 1)

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