affineIndependent_set_of_eq_iff — Mathlib

English

The image of a family under an injective affine map remains affinely independent.

Русский

Образ семейства под инъективным аффинным отображением сохраняет аффинную независимость.

LaTeX

$$$\\forall p\\,\\forall f\\;\\operatorname{AffineIndependent} k p \\rightarrow \\operatorname{AffineIndependent} k (f \\circ p)$$$

Lean4

/-- Affine equivalences preserve affine independence of subsets. -/
theorem affineIndependent_set_of_eq_iff {s : Set P} (e : P ≃ᵃ[k] P₂) :
    AffineIndependent k ((↑) : e '' s → P₂) ↔ AffineIndependent k ((↑) : s → P) :=
  by
  have : e ∘ ((↑) : s → P) = ((↑) : e '' s → P₂) ∘ (e : P ≃ P₂).image s := rfl
  erw [← e.affineIndependent_iff, this, affineIndependent_equiv]

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