sumExtendIndex — Mathlib

English

For a linearly independent family v, sumExtendIndex hs is a set of vectors to be added to v in order to form a basis of the ambient space.

Русский

Для линейно независимой семейства v множество sumExtendIndex hs задаёт дополнительные векторы, которые следует добавить к v, чтобы получить базис окружающего пространства.

LaTeX

$$$\\text{sumExtendIndex}(hs) = \\text{LinearIndepOn.extend}(hs) \\setminus \\mathrm{range}(v)$$$

Lean4

/-- Auxiliary definition: the index for the new basis vectors in `Basis.sumExtend`.

The specific value of this definition should be considered an implementation detail. -/
def sumExtendIndex (hs : LinearIndependent K v) : Set V :=
  LinearIndepOn.extend hs.linearIndepOn_id (subset_univ _) \ range v

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