English
For any n ≤ rank R M, there exists a finite subset s of M with cardinality n such that s is linearly independent on M.
Русский
Для любого n ≤ ранг M существует конечное подмножество s ⊆ M такого, что |s| = n и s линейно независимо на M.
LaTeX
$$$\forall n\, (hn : n ≤ \operatorname{rank}_R(M))\; \exists s : \text{Finset } M, s.card = n ∧ \operatorname{LinearIndepOn} R id s$$$
Lean4
theorem exists_finset_linearIndependent_of_le_rank {n : ℕ} (hn : n ≤ Module.rank R M) :
∃ s : Finset M, s.card = n ∧ LinearIndepOn R id (s : Set M) :=
by
rcases hn.eq_or_lt with h | h
· obtain ⟨⟨s, hs⟩, hs'⟩ :=
Cardinal.exists_eq_natCast_of_iSup_eq _ (Cardinal.bddAbove_range _) _ (h.trans (Module.rank_def R M)).symm
have : Finite s := lt_aleph0_iff_finite.mp (hs' ▸ nat_lt_aleph0 n)
cases nonempty_fintype s
refine ⟨s.toFinset, by simpa using hs', by simpa⟩
· obtain ⟨s, hs, hs'⟩ := exists_set_linearIndependent_of_lt_rank h
have : Finite s := lt_aleph0_iff_finite.mp (hs ▸ nat_lt_aleph0 n)
cases nonempty_fintype s
exact ⟨s.toFinset, by simpa using hs, by simpa⟩
