exists_set_linearIndependent_of_lt_rank

English

If n is less than the rank of M, there exists a subset s of M with cardinality n that is linearly independent on M.

Русский

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

LaTeX

$$$\forall n\, (hn : n < \operatorname{rank}_R(M))\; \exists s \subseteq M, \lvert s\rvert = n \land \operatorname{LinearIndepOn} R (\mathrm{id}) s$$$

Lean4

theorem exists_set_linearIndependent_of_lt_rank {n : Cardinal} (hn : n < Module.rank R M) :
    ∃ s : Set M, #s = n ∧ LinearIndepOn R id s :=
  by
  obtain ⟨⟨s, hs⟩, hs'⟩ := exists_lt_of_lt_ciSup' (hn.trans_eq (Module.rank_def R M))
  obtain ⟨t, ht, ht'⟩ := le_mk_iff_exists_subset.mp hs'.le
  exact ⟨t, ht', hs.mono ht⟩

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