translationNumber_eq_of_tendsto_aux

English

Let f be a CircleDeg1Lift. If its auxiliary translation-number sequence tends to a real τ' as n goes to infinity, then the translation number of f equals τ'.

Русский

Пусть f — CircleDeg1Lift. Если последовательность сопряжённых чисел трансляции f.transnumAuxSeq сходится к вещественному τ' при n → ∞, то τ(f) = τ'.

LaTeX

$$$ \forall f \in CircleDeg1Lift, \forall τ' \in \mathbb{R}, \operatorname{Tendsto} (f.transnumAuxSeq)_{atTop} (\mathcal{N}(τ')) \Rightarrow τ(f) = τ'. $$$

Lean4

theorem translationNumber_eq_of_tendsto_aux {τ' : ℝ} (h : Tendsto f.transnumAuxSeq atTop (𝓝 τ')) : τ f = τ' :=
  h.limUnder_eq

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