coe_setBasisOfLinearIndependentOfCardEqFinrank

English

Let s be a set with Nonempty s and Finite s, and lin_ind be LinearIndependent K ((↑) : s → V) with card_eq : s.toFinset.card = finrank K V. Then the coe of setBasisOfLinearIndependentOfCardEqFinrank equals the inclusion map from s to V.

Русский

Пусть s ненулево и конечно, линейно независимое отображение из s в V; тогда основание setBasisOfLinearIndependentOfCardEqFinrank коe совпадает с включением s в V.

LaTeX

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

Lean4

@[simp]
theorem coe_setBasisOfLinearIndependentOfCardEqFinrank {s : Set V} [Nonempty s] [Fintype s]
    (lin_ind : LinearIndependent K ((↑) : s → V)) (card_eq : s.toFinset.card = finrank K V) :
    ⇑(setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq) = ((↑) : s → V) := by
  simp [setBasisOfLinearIndependentOfCardEqFinrank]

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