nnnorm_pow_le

Mathlib.Analysis.Normed.Group.Ultra

URI: https://scilib.ai/kg/mathlib#IsUltrametricDist.nnnorm_pow_le

← MathLib Explorer

English

For x in a normed group and n ∈ ℕ, ‖x^n‖₊ ≤ ‖x‖₊.

Русский

Для x в нормированной группе и для натурального n, ‖x^n‖₊ ≤ ‖x‖₊.

LaTeX

$$$\\|x^n\\|_{+} \\leq \\|x\\|_{+}$$$

Lean4

@[to_additive]
theorem nnnorm_pow_le (x : S) (n : ℕ) : ‖x ^ n‖₊ ≤ ‖x‖₊ := by
  induction n with
  | zero => simp
  | succ n hn => simpa [pow_add, hn] using nnnorm_mul_le_max (x ^ n) x

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru