nnnorm_pow_le' — Mathlib

English

For a ∈ α, and n > 0, ‖a^n‖₊ ≤ ‖a‖₊^n.

Русский

Для a в α и n>0, ‖a^n‖₊ ≤ ‖a‖₊^n.

LaTeX

$$$\|a^n\|_{+} \le \|a\|_{+}^{n} \quad (n>0).$$$

Lean4

/-- If `α` is a seminormed ring, then `‖a ^ n‖₊ ≤ ‖a‖₊ ^ n` for `n > 0`.
See also `nnnorm_pow_le`. -/
theorem nnnorm_pow_le' (a : α) : ∀ {n : ℕ}, 0 < n → ‖a ^ n‖₊ ≤ ‖a‖₊ ^ n
  | 1, _ => by simp only [pow_one, le_rfl]
  | n + 2, _ => by
    simpa only [pow_succ' _ (n + 1)] using
      le_trans (nnnorm_mul_le _ _) (mul_le_mul_left' (nnnorm_pow_le' a n.succ_pos) _)

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