English
For a linear map f, and a cardinal c, c ≤ rank f if and only if there exists a subset s of V whose image under f is linearly independent and whose cardinality matches c.
Русский
Для линейного отображения f и кардинала c верно: c ≤ rank f тогда и только тогда, существует подмножество s ⊆ V такое, что образ f(s) линейно независимо и |s| = c.
LaTeX
$$$c \le \operatorname{rank} f \iff \exists s \subseteq V, \; \operatorname{lift}(|s|) = \operatorname{lift}(c) \land \operatorname{LinearIndepOn} K f s$$$
Lean4
theorem rank_finset_sum_le {η} (s : Finset η) (f : η → V →ₗ[K] V') : rank (∑ d ∈ s, f d) ≤ ∑ d ∈ s, rank (f d) :=
@Finset.sum_hom_rel _ _ _ _ _ (fun a b => rank a ≤ b) f (fun d => rank (f d)) s (le_of_eq rank_zero) fun _ _ _ h =>
le_trans (rank_add_le _ _) (add_le_add_left h _)
