exists_linearIndependent_of_le_rank

English

If the rank of a finite-dimensional space M over K is at least n, then there exists a function f: Fin n → M whose values form a linearly independent set.

Русский

Если ранг пространства M над полем K достаточен, существует отображение f: Fin n → M такое, что образующие его значения являются линейно независимыми.

LaTeX

$$$ \\exists f : Fin\\!\\ n \\to M,\\; \\mathrm{LinearIndependent}_K f $$$

Lean4

theorem exists_linearIndependent_of_le_rank {n : ℕ} (hn : n ≤ Module.rank R M) :
    ∃ f : Fin n → M, LinearIndependent R f :=
  have ⟨_, hs, hs'⟩ := exists_finset_linearIndependent_of_le_rank hn
  ⟨_, (linearIndependent_equiv (Finset.equivFinOfCardEq hs).symm).mpr hs'⟩

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