English
A finite family is linearly independent if and only if its cardinality equals the finrank of its span.
Русский
Конечное семейство линейно независимо тогда и только тогда, когда размерность его порожденного пространства равна размерам индекса.
LaTeX
$$$\operatorname{LinearIndependent}_K b \iff |ι| = (\operatorname{Set.range} b).\operatorname{finrank}_K$$$
Lean4
/-- A finite family of vectors is linearly independent if and only if
its cardinality equals the dimension of its span. -/
theorem linearIndependent_iff_card_eq_finrank_span {ι : Type*} [Fintype ι] {b : ι → V} :
LinearIndependent K b ↔ Fintype.card ι = (Set.range b).finrank K :=
by
constructor
· intro h
exact (finrank_span_eq_card h).symm
· intro hc
let f := Submodule.subtype (span K (Set.range b))
let b' : ι → span K (Set.range b) := fun i => ⟨b i, mem_span.2 fun p hp => hp (Set.mem_range_self _)⟩
have hs : ⊤ ≤ span K (Set.range b') := by
intro x
have h : span K (f '' Set.range b') = map f (span K (Set.range b')) := span_image f
have hf : f '' Set.range b' = Set.range b := by
ext x
simp [f, b', Set.mem_image, Set.mem_range]
rw [hf] at h
have hx : (x : V) ∈ span K (Set.range b) := x.property
simp_rw [h] at hx
simpa [f, mem_map] using hx
have hi : LinearMap.ker f = ⊥ := ker_subtype _
convert (linearIndependent_of_top_le_span_of_card_eq_finrank hs hc).map' _ hi
