English
If a family v is linearly independent and lies in the span of a subspace w, then the size of v is bounded by the size of w.
Русский
Если семейство линейно независимо и лежит в области порожденной w, то размер v ограничен размером w.
LaTeX
$$$\text{If } v: ι \to M \text{ is LI and } \operatorname{range}(v) \subseteq \operatorname{span}(w), \ |ι| \le |w|.$$$
Lean4
/-- If `R` satisfies the strong rank condition,
then for any linearly independent family `v : ι → M`
contained in the span of some finite `w : Set M`,
the cardinality of `ι` is bounded by the cardinality of `w`.
-/
theorem linearIndependent_le_span' {ι : Type*} (v : ι → M) (i : LinearIndependent R v) (w : Set M) [Fintype w]
(s : range v ≤ span R w) : #ι ≤ Fintype.card w :=
by
haveI : Finite ι := i.finite_of_le_span_finite v w s
letI := Fintype.ofFinite ι
rw [Cardinal.mk_fintype]
simp only [Nat.cast_le]
exact linearIndependent_le_span_aux' v i w s
