singleton_repr

Mathlib.Analysis.InnerProductSpace.PiL2

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

English

The repr of the singleton basis extracts the coordinate value corresponding to the index i.

Русский

Представление единичного базиса извлекает координатное значение для индекса i.

LaTeX

$$$(OrthonormalBasis.singleton ι 𝕜).repr x i = x$$$

Lean4

@[simp]
theorem singleton_repr (x i) : (OrthonormalBasis.singleton ι 𝕜).repr x i = x :=
  Basis.singleton_repr _ _ _ _

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

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

Разделы

Аффилиация

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