nnnorm_zpow_le_mul_norm — Mathlib

English

For any a in a normed group and any integer n, ∥a^n∥₊ ≤ ∥n∥₊ · ∥a∥₊.

Русский

Для любого a в нормированной группе и целого n верно ∥a^n∥₊ ≤ ∥n∥₊ · ∥a∥₊.

LaTeX

$$$\|a^{n}\|_{+} \le \|n\|_{+} \cdot \|a\|_{+}$$$

Lean4

@[to_additive nnnorm_zsmul_le]
theorem nnnorm_zpow_le_mul_norm (n : ℤ) (a : α) : ‖a ^ n‖₊ ≤ ‖n‖₊ * ‖a‖₊ := by
  simpa only [← NNReal.coe_le_coe, NNReal.coe_mul] using norm_zpow_le_mul_norm n a

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