nnnorm_def

Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

URI: https://scilib.ai/kg/mathlib#TrivSqZeroExt.nnnorm_def

English

The nnnorm (nonnegative norm) on tsze equals the sum of the nnnorms of the components.

Русский

Норма_NN на tsze равна сумме норм_NN компонент.

LaTeX

$$$\\|x\\|_{+} = \\|\\mathrm{fst}(x)\\|_{+} + \\|\\mathrm{snd}(x)\\|_{+}$$$

Lean4

theorem nnnorm_def (x : tsze R M) : ‖x‖₊ = ‖fst x‖₊ + ‖snd x‖₊ := by ext; simp [norm_def]

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

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

Разделы

Аффилиация

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