ofVectorSpace — Mathlib

English

Every vector space has a basis; in particular, there exists a basis indexed by ofVectorSpaceIndex K V.

Русский

Каждое векторное пространство имеет базис; в частности, существует базис V, индексированный множестом ofVectorSpaceIndex K V.

LaTeX

$$$\exists B: Basis (ofVectorSpaceIndex(K,V))$$$

Lean4

/-- Each vector space has a basis. -/
noncomputable def ofVectorSpace : Basis (ofVectorSpaceIndex K V) K V :=
  Basis.extend (linearIndependent_empty K V)

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