le_rank_iff_exists_linearIndependent_finset

English

For Module.Free K V, c ≤ rank K V is equivalent to the existence of a Finset of size c that is linearly independent.

Русский

Для Module.Free K V, c ≤ rank K V эквивалентно существованию конечного множества Finset размера c, линейно независимого.

LaTeX

$$$$ c \\le Module.rank\\,K\\,V \\iff \\exists s:\\mathrm{Finset}(V), s. card = c \\land LinearIndependent K ((↑) : (s:Set V)→V) $$$$

Lean4

theorem le_rank_iff_exists_linearIndependent_finset [Module.Free K V] {n : ℕ} :
    ↑n ≤ Module.rank K V ↔ ∃ s : Finset V, s.card = n ∧ LinearIndependent K ((↑) : ↥(s : Set V) → V) :=
  by
  simp only [le_rank_iff_exists_linearIndependent, mk_set_eq_nat_iff_finset]
  constructor
  · rintro ⟨s, ⟨t, rfl, rfl⟩, si⟩
    exact ⟨t, rfl, si⟩
  · rintro ⟨s, rfl, si⟩
    exact ⟨s, ⟨s, rfl, rfl⟩, si⟩

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