English
Another variant of the infinite-basis bound for LI families contained in span of the basis.
Русский
Другой вариант границы для бесконечной базы и линейно независимых семей внутри их области.
LaTeX
$$$|\kappa| \le |\iota|$ under the infinite-basis setting.$$
Lean4
/-- If `R` satisfies the strong rank condition,
then any linearly independent family `v : ι → M`
contained in the span of some finite `w : Set M`,
is itself finite.
-/
theorem finite_of_le_span_finite {ι : Type*} (v : ι → M) (i : LinearIndependent R v) (w : Set M) [Finite w]
(s : range v ≤ span R w) : Finite ι :=
letI := Fintype.ofFinite w
Fintype.finite <|
fintypeOfFinsetCardLe (Fintype.card w) fun t =>
by
let v' := fun x : (t : Set ι) => v x
have i' : LinearIndependent R v' := i.comp _ Subtype.val_injective
have s' : range v' ≤ span R w := (range_comp_subset_range _ _).trans s
simpa using linearIndependent_le_span_aux' v' i' w s'
