English
For the span basis, its value on i gives the original vector v_i.
Русский
Для базиса, задаваемого через span, значение на i даёт вектор v_i.
LaTeX
$$$(Basis.span hli i : M) = v_i$$$
Lean4
/-- A linear independent family of vectors is a basis for their span. -/
protected noncomputable def span : Basis ι R (span R (range v)) :=
Basis.mk (linearIndependent_span hli) <| by
intro x _
have : ∀ i, v i ∈ span R (range v) := fun i ↦ subset_span (Set.mem_range_self _)
have h₁ : (((↑) : span R (range v) → M) '' range fun i => ⟨v i, this i⟩) = range v :=
by
simp only [← Set.range_comp]
rfl
have h₂ : map (Submodule.subtype (span R (range v))) (span R (range fun i => ⟨v i, this i⟩)) = span R (range v) :=
by rw [← span_image, Submodule.coe_subtype, h₁]
have h₃ :
(x : M) ∈ map (Submodule.subtype (span R (range v))) (span R (Set.range fun i => Subtype.mk (v i) (this i))) :=
by
rw [h₂]
apply Subtype.mem x
rcases mem_map.1 h₃ with ⟨y, hy₁, hy₂⟩
have h_x_eq_y : x = y := by
rw [Subtype.ext_iff, ← hy₂]
simp
rwa [h_x_eq_y]
