singleton_apply

Mathlib.Analysis.InnerProductSpace.PiL2

URI: https://scilib.ai/kg/mathlib#OrthonormalBasis.singleton_apply

English

If there is a unique index type, the singleton basis yields a trivial basis with a single vector.

Русский

Если имеется единственный индекс, единичный базис порождает тривиальный базис с одним вектором.

LaTeX

$$Definition: OrthonormalBasis.singleton ι 𝕜$$

Lean4

@[simp]
theorem singleton_apply (i) : OrthonormalBasis.singleton ι 𝕜 i = 1 :=
  Basis.singleton_apply _ _ _

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

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

Разделы

Аффилиация

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