Subset_of_Linearly_Independent_Set_is_Linearly_Independent
Provedlinear-algebralinear-independenceproofwiki
A subset of a linearly independent set is also linearly independent.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Subset_of_Linearly_Independent_Set_is_Linearly_Independent {R : Type _} [Ring R] {M : Type _} [AddCommGroup M] [Module R M] {S T : Set M} (hST : S ⊆ T) (hT : LinearIndependent R (fun (x : T) => (x : M))) : LinearIndependent R (fun (x : S) => (x : M)) := by sorrySource