eventually_norm_pow_le — Mathlib

English

There exists a threshold after which the power inequality holds for all larger exponents.

Русский

Существует порог, после которого неравенство норм для степеней выполняется для всех больших степеней.

LaTeX

$$$\forall a, \exists N, \forall n \ge N, \|a^n\| ≤ \|a\|^n.$$$

Lean4

theorem eventually_norm_pow_le (a : α) : ∀ᶠ n : ℕ in atTop, ‖a ^ n‖ ≤ ‖a‖ ^ n :=
  eventually_atTop.mpr ⟨1, fun _b h => norm_pow_le' a (Nat.succ_le_iff.mp h)⟩

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