finsetBasisOfTopLeSpanOfCardEqFinrank

English

The coercion from a basis instance to the underlying function equals the original function.

Русский

Сведение из экземпляра базиса к базовой функции равняется исходной функции.

LaTeX

$$$\mathrm{coe}(\mathrm{basisOfTopLeSpanOfCardEqFinrank}\; b\; \ldots) = b$$$

Lean4

/-- A finset of `finrank K V` vectors forms a basis if they span the whole space. -/
@[simps! repr_apply]
noncomputable def finsetBasisOfTopLeSpanOfCardEqFinrank {s : Finset V} (le_span : ⊤ ≤ span K (s : Set V))
    (card_eq : s.card = finrank K V) : Basis { x // x ∈ s } K V :=
  basisOfTopLeSpanOfCardEqFinrank ((↑) : ↥(s : Set V) → V)
    ((@Subtype.range_coe_subtype _ fun x => x ∈ s).symm ▸ le_span) (_root_.trans (Fintype.card_coe _) card_eq)

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