English
For a linear map f: V → V', and a finite set of indices η, for every Finset s ⊆ η, the rank of the sum of maps over s is bounded by the sum of the ranks of the maps over s.
Русский
Для линейного отображения f: V → V' и конечного множества индексов η, для любого конечного множества s ⊆ η верно, что ранг суммы отображений по s не превышает суммы рангов отображений по s.
LaTeX
$$$\operatorname{rank}\left(\sum_{d \in s} f(d)\right) \le \sum_{d \in s} \operatorname{rank}(f(d))$$$
Lean4
theorem le_rank_iff_exists_linearIndependent_finset {n : ℕ} {f : V →ₗ[K] V'} :
↑n ≤ rank f ↔ ∃ s : Finset V, s.card = n ∧ LinearIndependent K fun x : (s : Set V) => f x :=
by
simp only [le_rank_iff_exists_linearIndependent, Cardinal.lift_natCast, Cardinal.lift_eq_nat_iff,
Cardinal.mk_set_eq_nat_iff_finset]
constructor
· rintro ⟨s, ⟨t, rfl, rfl⟩, si⟩
exact ⟨t, rfl, si⟩
· rintro ⟨s, rfl, si⟩
exact ⟨s, ⟨s, rfl, rfl⟩, si⟩
