translationNumber_eq_of_tendsto₀'

English

If Tendsto (f^[n + 1] 0 / (n + 1)) atTop (nhds τ') then τ f = τ'.

Русский

Если Tendsto (f^[n + 1] 0 / (n + 1)) до τ' в atTop, то τ(f) = τ'.

LaTeX

$$$ \forall f \in CircleDeg1Lift, \forall τ' \in \mathbb{R}, \operatorname{Tendsto} (n \mapsto f^[n + 1] 0 / (n + 1))_{atTop} (\mathcal{N}(τ')) \Rightarrow τ(f) = τ'. $$$

Lean4

theorem translationNumber_eq_of_tendsto₀' {τ' : ℝ} (h : Tendsto (fun n : ℕ => f^[n + 1] 0 / (n + 1)) atTop (𝓝 τ')) :
    τ f = τ' :=
  f.translationNumber_eq_of_tendsto₀ <| (tendsto_add_atTop_iff_nat 1).1 (mod_cast h)

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