English
The image of an affine subspace under an affine map is an affine subspace with carrier f''s and the smul-vsub-vadd property preserved.
Русский
Образ афинного подпространства под аффинным отображением — это афинное подпространство с носителем \(f''s\) и сохранённым свойством smul-vsub-vadd.
LaTeX
$$$(s.map f)$ is the affine subspace with carrier $f''s$ and smul_vsub_vadd_mem preserved.$$
Lean4
/-- The image of an affine subspace under an affine map as an affine subspace. -/
def map (s : AffineSubspace k P₁) : AffineSubspace k P₂
where
carrier := f '' s
smul_vsub_vadd_mem := by
rintro t - - - ⟨p₁, h₁, rfl⟩ ⟨p₂, h₂, rfl⟩ ⟨p₃, h₃, rfl⟩
use t • (p₁ -ᵥ p₂) +ᵥ p₃
suffices t • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ s by {
simp only [SetLike.mem_coe, true_and, this]
rw [AffineMap.map_vadd, map_smul, AffineMap.linearMap_vsub]
}
exact s.smul_vsub_vadd_mem t h₁ h₂ h₃
