exists_fun_fin_finrank_span_eq — Mathlib

English

For a subset s of M over K, there exists a finite t with t ⊆ s such that span_K t = span_K s and t is linearly independent over K.

Русский

Для подмножества s ⊆ M над полем K существует конечное t ⊆ s такое, что span_K t = span_K s и t линейно независимо над K.

LaTeX

$$$\\exists t : Finset M, \\; t \\subseteq s \\land t.card = finrank K (span K s) \\land span K t = span K s \\land LinearIndepOn K id (t : Set M)$$$

Lean4

theorem exists_fun_fin_finrank_span_eq :
    ∃ f : Fin (finrank K (span K s)) → M, (∀ i, f i ∈ s) ∧ span K (range f) = span K s ∧ LinearIndependent K f :=
  by
  rcases exists_finset_span_eq_linearIndepOn K s with ⟨t, hts, ht_card, ht_span, ht_indep⟩
  set e := (Finset.equivFinOfCardEq ht_card).symm
  exact ⟨(↑) ∘ e, fun i ↦ hts (e i).2, by simpa, ht_indep.comp _ e.injective⟩

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