tendsto_eval_one_sub_pow — Mathlib

English

For a fixed κ, the forward difference tends to zero under the given conditions.

Русский

Для фиксированного κ переходный предел стремится к нулю при выполнении условий.

LaTeX

$$Tendsto (fun n ↦ (κ 1 − 1)^n) atTop (nhds 0)$$

Lean4

theorem tendsto_eval_one_sub_pow {κ : AddChar ℤ_[p] R} (hκ : Continuous κ) :
    Tendsto (fun n ↦ (κ 1 - 1) ^ n) atTop (𝓝 0) :=
  by
  refine (PadicInt.fwdDiff_tendsto_zero ⟨κ, hκ⟩).congr fun n ↦ ?_
  simpa only [AddChar.map_zero_eq_one, mul_one] using fwdDiff_addChar_eq κ 0 1 n

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