mono — Mathlib

English

From an affine independent family, the corresponding range set is affine independent.

Русский

Из аффинной независимой семьи следует, что диапазон независим.

LaTeX

$$AffineIndependent k p → AffineIndependent k fun x => x : Set.range p → P$$

Lean4

/-- If a set of points is affinely independent, so is any subset. -/
protected theorem mono {s t : Set P} (ha : AffineIndependent k (fun x => x : t → P)) (hs : s ⊆ t) :
    AffineIndependent k (fun x => x : s → P) :=
  ha.comp_embedding (s.embeddingOfSubset t hs)

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