exists_finset_linearIndependent_of_le_finrank

English

If n ≤ finrank_R M, there exists a Finset s ⊆ M with card n and LinearIndepOn R id s.

Русский

Если n ≤ finrank_R M, существует конечное подмножество s ⊆ M такого, что s линейно независимо по R.

LaTeX

$$$\forall n\, (hn : n ≤ \operatorname{finrank}_R(M))\; \exists s : \mathrm{Finset} M, s.card = n ∧ \operatorname{LinearIndepOn} R id s.toSet$$

Lean4

theorem exists_finset_linearIndependent_of_le_finrank {n : ℕ} (hn : n ≤ finrank R M) :
    ∃ s : Finset M, s.card = n ∧ LinearIndependent R ((↑) : s → M) :=
  by
  by_cases h : finrank R M = 0
  · rw [le_zero_iff.mp (hn.trans_eq h)]
    exact ⟨∅, rfl, by convert linearIndependent_empty R M using 2 <;> aesop⟩
  exact
    exists_finset_linearIndependent_of_le_rank
      ((Nat.cast_le.mpr hn).trans_eq (cast_toNat_of_lt_aleph0 (toNat_ne_zero.mp h).2))

Похожие утверждения