map_mkOfPoint — Mathlib

English

Pushing forward a 0-simplex mkOfPoint along an injective affine map f simply maps the underlying point accordingly.

Русский

Перемещая нулевую грань mkOfPoint по инъективному аффинному отображению f, вершина остается соответствовать изображению точки.

LaTeX

$$$(mkOfPoint\\ k p).map f hf = mkOfPoint\\ k (f p)$$$

Lean4

@[simp]
theorem map_mkOfPoint (f : P →ᵃ[k] P₂) (hf : Function.Injective f) (p : P) :
    (mkOfPoint k p).map f hf = mkOfPoint k (f p) :=
  rfl

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