coe_finsetBasisOfLinearIndependentOfCardEqFinrank

English

For a finite set s with a linear independent embedding of s into V, and card s = finrank K V, the underlying function of finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq is the inclusion map from s to V.

Русский

Для конечного множества s с линейно независимым вложением в V и card(s) = finrank_K V функция-основа равна включению s в V.

LaTeX

$$$\\bigl(\\text{finsetBasisOfLinearIndependentOfCardEqFinrank }\\; hs \\; lin\\_ind \\; card\\_eq\\bigr) = (\\uparrow): s \\to V$.$$

Lean4

@[simp]
theorem coe_finsetBasisOfLinearIndependentOfCardEqFinrank {s : Finset V} (hs : s.Nonempty)
    (lin_ind : LinearIndependent K ((↑) : s → V)) (card_eq : s.card = finrank K V) :
    ⇑(finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq) = ((↑) : s → V) := by
  simp [finsetBasisOfLinearIndependentOfCardEqFinrank]

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