range_finsetBasis — Mathlib

English

The set of vectors produced by the finite basis map is exactly the standard basis index Basis.ofVectorSpaceIndex K V.

Русский

Множество векторов, получаемых отображением конечного базиса, ровно соответствует стандартному индексу базиса Basis.ofVectorSpaceIndex K V.

LaTeX

$$$ \\mathrm{Set.range}(\\mathrm{finsetBasis}\\,K\\,V) = \\mathrm{Basis.ofVectorSpaceIndex}\\,K\\,V $$$

Lean4

@[simp]
theorem range_finsetBasis [IsNoetherian K V] : Set.range (finsetBasis K V) = Basis.ofVectorSpaceIndex K V := by
  rw [finsetBasis, Basis.range_reindex, Basis.range_ofVectorSpace]

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