norm_eq_zero

Mathlib.Topology.Algebra.Valued.NormedValued

URI: https://scilib.ai/kg/mathlib#Valued.norm_eq_zero

English

If the norm of x is zero, then x is zero.

Русский

Если норма x равна нулю, то x равен нулю.

LaTeX

$$$$ \text{If } \|x\| = 0 \text{ then } x = 0. $$$$

Lean4

theorem norm_eq_zero {x : L} (hx : norm x = 0) : x = 0 := by
  simpa [norm, NNReal.coe_eq_zero, RankOne.hom_eq_zero_iff, zero_iff] using hx

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

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

Разделы

Аффилиация

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