span_apply

Mathlib.LinearAlgebra.Basis.Basic

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

English

See Span behavior: the i-th value of span recovers v_i.

Русский

См. поведение span: i-й элемент равен v_i.

LaTeX

$$$(Basis.span hli i : M) = v_i$$$

Lean4

protected theorem span_apply (i : ι) : (Basis.span hli i : M) = v i :=
  congr_arg ((↑) : span R (range v) → M) <| Basis.mk_apply _ _ _

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

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

Разделы

Аффилиация

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