norm_pos

Mathlib.Analysis.CStarAlgebra.Module.Defs

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

← MathLib Explorer

English

If x ≠ 0 then 0 < ||x||.

Русский

Если x ≠ 0, то 0 < ||x||.

LaTeX

$$$x \\neq 0 \\Rightarrow 0 < \\\\|x\\\\|$$$

Lean4

protected theorem norm_pos {x : E} (hx : x ≠ 0) : 0 < ‖x‖ :=
  by
  simp only [norm_eq_sqrt_norm_inner_self (A := A), Real.sqrt_pos, norm_pos_iff]
  intro H
  rw [inner_self] at H
  exact hx H

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

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

Разделы

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

Аффилиация

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