norm_nonneg

Mathlib.Analysis.CStarAlgebra.Module.Defs

URI: https://scilib.ai/kg/mathlib#CStarModule.norm_nonneg

English

For all x ∈ E, 0 ≤ ||x||.

Русский

Для всех x ∈ E выполняется 0 ≤ ||x||.

LaTeX

$$$0 \\leq \\\\|x\\\\|$$$

Lean4

protected theorem norm_nonneg {x : E} : 0 ≤ ‖x‖ := by simp [norm_eq_sqrt_norm_inner_self (A := A)]

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

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

Разделы

Аффилиация

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