coe_toBasis

Mathlib.Analysis.InnerProductSpace.PiL2

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

English

The coercion from the orthonormal basis toBasis coincides with the canonical basis mapping.

Русский

Переход от OrthonormalBasis к базису toBasis совпадает с каноническим отображением базиса.

LaTeX

$$b.toBasis = b$$

Lean4

@[simp]
protected theorem coe_toBasis (b : OrthonormalBasis ι 𝕜 E) : (⇑b.toBasis : ι → E) = ⇑b :=
  rfl

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

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

Разделы

Аффилиация

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