vectorSpan_eq_top_of_card_eq_finrank_add_one

English

If the index set has cardinality one more than the ambient space dimension, the vector span of the range is the whole space (top).

Русский

Если кардинал множества индексов равен размерности пространства плюс один, то векторное span образа равняется всему пространству.

LaTeX

$$$\operatorname{vectorSpan}_k(\operatorname{SetRange}(p)) = \top$$$

Lean4

/-- The `vectorSpan` of a finite affinely independent family whose
cardinality is one more than that of the finite-dimensional space is
`⊤`. -/
theorem vectorSpan_eq_top_of_card_eq_finrank_add_one [FiniteDimensional k V] [Fintype ι] {p : ι → P}
    (hi : AffineIndependent k p) (hc : Fintype.card ι = finrank k V + 1) : vectorSpan k (Set.range p) = ⊤ :=
  Submodule.eq_top_of_finrank_eq <| hi.finrank_vectorSpan hc

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