ofVectorSpaceIndex — Mathlib

English

ofVectorSpaceIndex is defined as the extension of the empty independent set inside the universal set.

Русский

ofVectorSpaceIndex определяется как расширение пустого линейно независимого множества внутри всего пространства.

LaTeX

$$$\\mathrm{ofVectorSpaceIndex} = (\\mathrm{linearIndepOn\_empty} K id).extend(\\mathrm{subset\\_univ} V)$$$

Lean4

/-- A set used to index `Basis.ofVectorSpace`. -/
noncomputable def ofVectorSpaceIndex : Set V :=
  (linearIndepOn_empty K id).extend (subset_univ _)

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