AffineIndependent — Mathlib

English

If h: card ι = finrank k V + 1, then there exists an affine basis ι k P.

Русский

Если выполнено равенство размера индекса и размерности, существует аффинная база.

LaTeX

$$Nonempty (AffineBasis ι k P)$$

Lean4

/-- An indexed family is said to be affinely independent if no
nontrivial weighted subtractions (where the sum of weights is 0) are
0. -/
def AffineIndependent (p : ι → P) : Prop :=
  ∀ (s : Finset ι) (w : ι → k), ∑ i ∈ s, w i = 0 → s.weightedVSub p w = (0 : V) → ∀ i ∈ s, w i = 0

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