linearMap_vsub — Mathlib

English

The linear part of an affine map acts linearly on the difference of two points: f.linear (p1 -ᵥ p2) = f p1 -ᵥ f p2.

Русский

Линейная часть аффинного отображения действует линейно на разность двух точек: f.linear(p1 -ᵥ p2) = f p1 -ᵥ f p2.

LaTeX

$$$f.linear (p_1 -_v p_2) = f p_1 -_v f p_2$$$

Lean4

/-- The linear map on the result of subtracting two points is the
result of subtracting the result of the affine map on those two
points. -/
@[simp]
theorem linearMap_vsub (f : P1 →ᵃ[k] P2) (p1 p2 : P1) : f.linear (p1 -ᵥ p2) = f p1 -ᵥ f p2 := by
  conv_rhs => rw [← vsub_vadd p1 p2, map_vadd, vadd_vsub]

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