English
Continuation of the bound for LI families within an infinite basis.
Русский
Следствие ограничения размера LI семейства внутри бесконечной базы.
LaTeX
$$$\text{If } b \text{ is infinite, then for LI } v,\ |\kappa| \le |\iota|$.$$
Lean4
theorem linearIndependent_le_span_aux' {ι : Type*} [Fintype ι] (v : ι → M) (i : LinearIndependent R v) (w : Set M)
[Fintype w] (s : range v ≤ span R w) : Fintype.card ι ≤ Fintype.card w := by
-- We construct an injective linear map `(ι → R) →ₗ[R] (w → R)`,
-- by thinking of `f : ι → R` as a linear combination of the finite family `v`,
-- and expressing that (using the axiom of choice) as a linear combination over `w`.
-- We can do this linearly by constructing the map on a basis.
fapply card_le_of_injective' R
· apply Finsupp.linearCombination
exact fun i => Span.repr R w ⟨v i, s (mem_range_self i)⟩
· intro f g h
apply_fun linearCombination R ((↑) : w → M) at h
simp only [linearCombination_linearCombination, Span.finsupp_linearCombination_repr] at h
exact i h
