English
Injective affine transformations preserve affine independence.
Русский
Инъективные аффинные преобразования сохраняют аффинную независимость.
LaTeX
$$$\\forall p\\,\\forall f\\; (\\operatorname{Injective} f) \\Rightarrow \\operatorname{AffineIndependent} k p \\Rightarrow \\operatorname{AffineIndependent} k (f\\circ p)$$$
Lean4
/-- The image of a family of points in affine space, under an injective affine transformation, is
affine-independent. -/
theorem map' {p : ι → P} (hai : AffineIndependent k p) (f : P →ᵃ[k] P₂) (hf : Function.Injective f) :
AffineIndependent k (f ∘ p) := by
rcases isEmpty_or_nonempty ι with h | h
· apply affineIndependent_of_subsingleton
obtain ⟨i⟩ := h
rw [affineIndependent_iff_linearIndependent_vsub k p i] at hai
simp_rw [affineIndependent_iff_linearIndependent_vsub k (f ∘ p) i, Function.comp_apply, ← f.linearMap_vsub]
have hf' : LinearMap.ker f.linear = ⊥ := by rwa [LinearMap.ker_eq_bot, f.linear_injective_iff]
exact LinearIndependent.map' hai f.linear hf'
