zero_pow_eventuallyEq — Mathlib

English

For any MonoidWithZero, the sequence n ↦ 0^n is eventually constantly 0 along atTop.

Русский

Для любого моноида с нулем последовательность n ↦ 0^n становится постоянно равной 0 на бесконечности.

LaTeX

$$$ (0)^{n} \to 0 \quad \text{eventually along } n \to +\infty,$ i.e. $\exists N \forall n \ge N, 0^{n}=0 $.$$

Lean4

theorem zero_pow_eventuallyEq [MonoidWithZero α] : (fun n : ℕ => (0 : α) ^ n) =ᶠ[atTop] fun _ => 0 :=
  eventually_atTop.2 ⟨1, fun _n hn ↦ zero_pow <| Nat.one_le_iff_ne_zero.1 hn⟩

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