map_linePolynomial — Mathlib

English

The line through two mapped points is the map of the line through the original points.

Русский

Прямая через изображённые точки является образом прямой через исходные точки.

LaTeX

$$$ linePolynomial (f x) (f y) (f \ell) = (linePolynomial x y \ell).map f $$$

Lean4

theorem map_linePolynomial : linePolynomial (f x) (f y) (f ℓ) = (linePolynomial x y ℓ).map f :=
  by
  simp only [linePolynomial]
  map_simp

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