linearIndependent — Mathlib

English

The range of the basis Basis.ofVectorSpace equals the index set for the vector space.

Русский

Диапазон базиса Basis.ofVectorSpace совпадает с индексным множеством пространства.

LaTeX

$$$\operatorname{range}(\mathrm{Basis.ofVectorSpace}(K,V)) = \mathrm{ofVectorSpaceIndex}(K,V)$$$

Lean4

theorem linearIndependent : LinearIndependent K ((↑) : ofVectorSpaceIndex K V → V) :=
  by
  convert (ofVectorSpace K V).linearIndependent
  ext x
  rw [ofVectorSpace_apply_self]

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