English
Under strong rank condition, if there exists an injective linear map from finsupp α to finsupp β, then |α| ≤ |β|.
Русский
При сильном ранге, если существует инъективное линейное отображение Finsupp α → Finsupp β, тогда |α| ≤ |β|.
LaTeX
$$$\#\alpha \le \#\beta$ given an injective linear map $(\alpha \to \mathbb{R}) \to (\beta \to \mathbb{R})$.$$
Lean4
/-- An auxiliary lemma for `linearIndependent_le_basis`:
we handle the case where the basis `b` is infinite.
-/
theorem linearIndependent_le_infinite_basis {ι : Type w} (b : Basis ι R M) [Infinite ι] {κ : Type w} (v : κ → M)
(i : LinearIndependent R v) : #κ ≤ #ι := by
classical
by_contra h
rw [not_le, ← Cardinal.mk_finset_of_infinite ι] at h
let Φ := fun k : κ => (b.repr (v k)).support
obtain ⟨s, w : Infinite ↑(Φ ⁻¹' { s })⟩ := Cardinal.exists_infinite_fiber Φ h (by infer_instance)
let v' := fun k : Φ ⁻¹' { s } => v k
have i' : LinearIndependent R v' := i.comp _ Subtype.val_injective
have w' : Finite (Φ ⁻¹' { s }) := by
apply i'.finite_of_le_span_finite v' (s.image b)
rintro m ⟨⟨p, ⟨rfl⟩⟩, rfl⟩
simp only [SetLike.mem_coe, Finset.coe_image]
apply Basis.mem_span_repr_support
exact w.false
