English
For Module.Free K V, for any c, c ≤ rank K V iff there exists a set s with cardinality c that is linearly independent.
Русский
Для Module.Free K V и любого кардинального c, c ≤ rank K V эквивалентно существованию множества s размера c, линейно независимого.
LaTeX
$$$$ c \\le Module.rank\\,K\\,V \\iff \\exists s:\\text{ Set }V,\\; #s = c \\land LinearIndepOn K id s $$$$
Lean4
theorem le_rank_iff_exists_linearIndependent [Module.Free K V] {c : Cardinal} :
c ≤ Module.rank K V ↔ ∃ s : Set V, #s = c ∧ LinearIndepOn K id s :=
by
haveI := nontrivial_of_invariantBasisNumber K
constructor
· intro h
obtain ⟨κ, t'⟩ := Module.Free.exists_basis (R := K) (M := V)
let t := t'.reindexRange
have : LinearIndepOn K id (Set.range t') :=
by
convert t.linearIndependent.linearIndepOn_id
ext
simp [t]
rw [← t.mk_eq_rank'', le_mk_iff_exists_subset] at h
rcases h with ⟨s, hst, hsc⟩
exact ⟨s, hsc, this.mono hst⟩
· rintro ⟨s, rfl, si⟩
exact si.cardinal_le_rank
