affineIndependent_iff — Mathlib

English

Under affine independence, extending affine combinations through embeddings yields equality of indicators.

Русский

При аффинной независимости продолжение аффинных комбинаций через вложения дает равенство индикаторов.

LaTeX

$$$\\operatorname{AffineIndependent} k p \\rightarrow \\forall e,\\; \\text{indicator equality holds for extension}$$$

Lean4

/-- Injective affine maps preserve affine independence. -/
theorem affineIndependent_iff {p : ι → P} (f : P →ᵃ[k] P₂) (hf : Function.Injective f) :
    AffineIndependent k (f ∘ p) ↔ AffineIndependent k p :=
  ⟨AffineIndependent.of_comp f, fun hai => AffineIndependent.map' hai f hf⟩

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