inner_self_eq_zero

Mathlib.Analysis.InnerProductSpace.Basic

URI: https://scilib.ai/kg/mathlib#inner_self_eq_zero

English

For x ∈ E, ⟪x, x⟫ = 0 if and only if x = 0.

Русский

Для x ∈ E выполняется: ⟪x, x⟫ = 0 эквивалентно x = 0.

LaTeX

$$$\langle x, x\rangle = 0 \;\Longleftrightarrow\; x = 0$$$

Lean4

@[simp]
theorem inner_self_eq_zero {x : E} : ⟪x, x⟫ = 0 ↔ x = 0 := by
  rw [inner_self_eq_norm_sq_to_K, sq_eq_zero_iff, ofReal_eq_zero, norm_eq_zero]

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

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

Разделы

Аффилиация

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