subtype — Mathlib

English

If p is affinely independent, then restricting to a subtype of indices preserves affine independence.

Русский

Если p аффинно независимa, то ограничение к подтипу индексов сохраняет независимость.

LaTeX

$$AffineIndependent k p → AffineIndependent k (λ i, p i.val)$$

Lean4

/-- If a family is affinely independent, so is any subfamily indexed
by a subtype of the index type. -/
protected theorem subtype {p : ι → P} (ha : AffineIndependent k p) (s : Set ι) : AffineIndependent k fun i : s => p i :=
  ha.comp_embedding (Embedding.subtype _)

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