English
For a subset s ⊆ M, there exists a finite subset t ⊆ s such that span_K t = span_K s, t ⊆ s, |t| = finrank_K(span_K s), and t is linearly independent over K.
Русский
Для подмножества s ⊆ M существует конечное подмножество t ⊆ s такое, что span_K t = span_K s, t ⊆ s, |t| = finrank_K(span_K s), и t линейно независимо над K.
LaTeX
$$$\\exists t : Finset M, \\; t \\subseteq s \\land t.card = \\operatorname{finrank}_K(\\operatorname{span}_K s) \land \\operatorname{span}_K t = \\operatorname{span}_K s \\land \\operatorname{LinearIndepOn} K\\; id\\; (t : Set M)$$$
Lean4
/-- This is a version of `exists_linearIndependent`
with an upper estimate on the size of the finite set we choose. -/
theorem exists_finset_span_eq_linearIndepOn :
∃ t : Finset M, ↑t ⊆ s ∧ t.card = finrank K (span K s) ∧ span K t = span K s ∧ LinearIndepOn K id (t : Set M) :=
by
rcases exists_linearIndependent K s with ⟨t, ht_sub, ht_span, ht_indep⟩
obtain ⟨t, rfl, ht_card⟩ : ∃ u : Finset M, ↑u = t ∧ u.card = finrank K (span K s) := by
rw [← Cardinal.mk_set_eq_nat_iff_finset, finrank_eq_rank, ← ht_span, rank_span_set ht_indep]
exact ⟨t, ht_sub, ht_card, ht_span, ht_indep⟩
