English
For a LI family v and a finite set w spanning a subspace, the index cardinality is bounded by the finite set's card.
Русский
Для LI-семьи v и конечного набора w, порождающего подпространство, размер индексов ограничен кардиналом w.
LaTeX
$$$\#\iota \le w.card$ under finiteness assumptions.$$
Lean4
/-- `StrongRankCondition` implies that if there is an injective linear map `(α →₀ R) →ₗ[R] β →₀ R`,
then the cardinal of `α` is smaller than or equal to the cardinal of `β`.
-/
theorem card_le_of_injective'' {α : Type v} {β : Type v} (f : (α →₀ R) →ₗ[R] β →₀ R) (i : Injective f) : #α ≤ #β :=
by
let b : Basis β R (β →₀ R) := ⟨1⟩
apply linearIndependent_le_basis b (fun (i : α) ↦ f (Finsupp.single i 1))
rw [LinearIndependent]
have : (linearCombination R fun i ↦ f (Finsupp.single i 1)) = f := by ext a b; simp
exact this.symm ▸ i
