coe_ofSpan

Mathlib.LinearAlgebra.Basis.VectorSpace

URI: https://scilib.ai/kg/mathlib#Module.Basis.coe_ofSpan

English

The underlying map of Basis.ofSpan is the inclusion map from the index set into V.

Русский

Базис Basis.ofSpan действует как включение индекса в пространство V.

LaTeX

$$$\\text{coe\_ofSpan} : (\\mathrm{Basis.ofSpan}\\; hs) = \\text{incl}$$$

Lean4

@[simp]
theorem coe_ofSpan (hs : ⊤ ≤ span K s) : ⇑(ofSpan hs) = ((↑) : _ → _) :=
  funext (ofSpan_apply_self hs)

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

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

Разделы

Аффилиация

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