English
If the image of a family under an affine transformation is affinely independent, so is the original family.
Русский
Если образ семейства точек под аффинным отображением аффинно независим, то и исходное семейство аффинно независимо.
LaTeX
$$$\\forall p\\;\\, (f: P\\to^a_k P_2)\\;\\text{injection} \\Rightarrow \\operatorname{AffineIndependent} k (f\\circ p) \\rightarrow \\operatorname{AffineIndependent} k p$$$
Lean4
/-- If the image of a family of points in affine space under an affine transformation is affine-
independent, then the original family of points is also affine-independent. -/
theorem of_comp {p : ι → P} (f : P →ᵃ[k] P₂) (hai : AffineIndependent k (f ∘ p)) : AffineIndependent k p :=
by
rcases isEmpty_or_nonempty ι with h | h
· apply affineIndependent_of_subsingleton
obtain ⟨i⟩ := h
rw [affineIndependent_iff_linearIndependent_vsub k p i]
simp_rw [affineIndependent_iff_linearIndependent_vsub k (f ∘ p) i, Function.comp_apply, ← f.linearMap_vsub] at hai
exact LinearIndependent.of_comp f.linear hai
