vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one

English

If an affinely independent p and a finite s satisfy that vectorSpan of s.image p is ≤ sm and card s = dim(sm) + 1, then vectorSpan equals sm.

Русский

Если p аффинно независим и s конечен, и vectorSpan( s.image p ) ≤ sm и |s| = dim(sm) + 1, то vectorSpan = sm.

LaTeX

$$$\text{AffineIndependent}_k(p) \Rightarrow (\operatorname{vectorSpan}_k(\operatorname{image}(p,s)) \le sm) \Rightarrow \#s = \operatorname{finrank}_k(sm) + 1 \Rightarrow \operatorname{vectorSpan}_k(\operatorname{image}(p,s)) = sm$$$

Lean4

/-- If the `vectorSpan` of a finite subset of an affinely independent
family lies in a submodule with dimension one less than its
cardinality, it equals that submodule. -/
theorem vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one [DecidableEq P] {p : ι → P}
    (hi : AffineIndependent k p) {s : Finset ι} {sm : Submodule k V} [FiniteDimensional k sm]
    (hle : vectorSpan k (s.image p : Set P) ≤ sm) (hc : #s = finrank k sm + 1) :
    vectorSpan k (s.image p : Set P) = sm :=
  Submodule.eq_of_le_of_finrank_eq hle <| hi.finrank_vectorSpan_image_finset hc

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