enorm_eq_one

Mathlib.Analysis.InnerProductSpace.Orthonormal

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

English

If v is orthonormal, then the ENNReal norm of each vector v_i equals 1: ‖v_i‖ₑ = 1.

Русский

Если v ортонормированно, то для каждого i ‖v_i‖ₑ = 1.

LaTeX

$$$\operatorname{Orthonormal} 𝕜 v \rightarrow \forall i, \|v i\|_{e} = 1$$$

Lean4

theorem enorm_eq_one {v : ι → E} (h : Orthonormal 𝕜 v) (i : ι) : ‖v i‖ₑ = 1 := by rw [← ofReal_norm];
  simp [h.norm_eq_one]

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

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

Разделы

Аффилиация

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