ne_zero

Mathlib.Analysis.InnerProductSpace.Orthonormal

URI: https://scilib.ai/kg/mathlib#Orthonormal.ne_zero

English

In an orthonormal family, each vector is nonzero.

Русский

В ортонормированной семье каждый вектор ненулевой.

LaTeX

$$$v_i \\neq 0$ for every index $i$ in the index set.$$

Lean4

theorem ne_zero {v : ι → E} (hv : Orthonormal 𝕜 v) (i : ι) : v i ≠ 0 :=
  by
  refine ne_of_apply_ne norm ?_
  rw [hv.1 i, norm_zero]
  simp

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

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

Разделы

Аффилиация

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