norm_pow_le' — Mathlib

English

For a with h>0, ‖a^n‖ ≤ ‖a‖^n in NNReal sense.

Русский

Для a с положительным n, неравенство в NNReal: ‖a^n‖ ≤ ‖a‖^n.

LaTeX

$$$\text{If } h>0,\; \mathrm{nnnorm}(a^n) ≤ \mathrm{nnnorm}(a)^n.$$$

Lean4

/-- If `α` is a seminormed ring, then `‖a ^ n‖ ≤ ‖a‖ ^ n` for `n > 0`. See also `norm_pow_le`. -/
theorem norm_pow_le' (a : α) {n : ℕ} (h : 0 < n) : ‖a ^ n‖ ≤ ‖a‖ ^ n := by
  simpa only [NNReal.coe_pow, coe_nnnorm] using NNReal.coe_mono (nnnorm_pow_le' a h)

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