of_isEmpty

Mathlib.Analysis.InnerProductSpace.Orthonormal

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

English

If the index type is empty, any function v: ι → E is orthonormal.

Русский

Если множество индексов пусто, любая функция v: ι → E является ортонормированным семейством.

LaTeX

$$[IsEmpty ι] ⇒ Orthonormal 𝕜 v$$

Lean4

@[simp]
theorem of_isEmpty [IsEmpty ι] (v : ι → E) : Orthonormal 𝕜 v :=
  ⟨IsEmpty.elim ‹_›, Subsingleton.pairwise⟩

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

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

Разделы

Аффилиация

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