comp_lineMap — Mathlib

English

Composition of affine map with a line map yields another line map with transformed endpoints.

Русский

Сложение аффинного отображения с lineMap даёт новую lineMap с преобразованными концами.

LaTeX

$$$ (f \circ \text{lineMap}(p_0,p_1)) = \text{lineMap}(f p_0, f p_1) $$$

Lean4

@[simp]
theorem comp_lineMap (f : P1 →ᵃ[k] P2) (p₀ p₁ : P1) : f.comp (lineMap p₀ p₁) = lineMap (f p₀) (f p₁) :=
  ext <| f.apply_lineMap p₀ p₁

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