norm_pow_le_mul_norm — Mathlib

English

For any natural exponent n, the norm of a^n is at most n times the norm of a.

Русский

Для натурального показателя n нормa a^n не превышает n раз нормы a.

LaTeX

$$$\\forall n \\in \\mathbb{N},\\: \\|a^n\\| \\le n \\cdot \\|a\\|$$$

Lean4

@[to_additive norm_nsmul_le]
theorem norm_pow_le_mul_norm : ∀ {n : ℕ}, ‖a ^ n‖ ≤ n * ‖a‖
  | 0 => by simp
  | n + 1 => by simpa [pow_succ, add_mul] using norm_mul_le_of_le' norm_pow_le_mul_norm le_rfl

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