map_vadd — Mathlib

English

An affine isometry maps a translated point v + p to the translated image by the linear part: e(v + p) = e.linearIsometryEquiv(v) + e(p).

Русский

Аффинная изометрия переводит точку v + p в изображение, полученное переносом через линейную часть: e(v + p) = e.linearIsometryEquiv(v) + e(p).

LaTeX

$$$e(v +\u22A5 p) = e.linearIsometryEquiv(v) +\u22A5 e(p)$$$

Lean4

@[simp]
theorem map_vadd (p : P) (v : V) : e (v +ᵥ p) = e.linearIsometryEquiv v +ᵥ e p :=
  e.toAffineIsometry.map_vadd p v

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