English
Push forward an affine simplex under an injective affine map by applying the map to all its vertices and transporting its affine independence accordingly.
Русский
Перемещаем аффиндвойной симплекс по инъективному аффинному отображению, применяя отображение ко всем вершинам и соответствующе сохраняя аффинное независимое множество.
LaTeX
$$$\\text{map}: \\text{Affine.Simplex } k P n \\to \\text{Affine.Simplex } k P_2 n,\\quad (s.map\\ f\\ hf).points := f \\circ s.points,\\; (s.map\\ f hf).independent := s.independent.map' f hf$$$
Lean4
/-- Push forward an affine simplex under an injective affine map. -/
@[simps -fullyApplied]
def map {n : ℕ} (s : Affine.Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective f) : Affine.Simplex k P₂ n
where
points := f ∘ s.points
independent := s.independent.map' f hf
