pointwise_vadd_eq_map — Mathlib

English

Translation by a vector equals applying the corresponding affine equivalence to the subspace.

Русский

Перенос на вектор равен применению соответствующего аффинного эквивалента к подпространству.

LaTeX

$$$v +\!\!\! s = s.map (\mathrm{AffineEquiv}.constVAdd k P v).$$$

Lean4

theorem pointwise_vadd_eq_map (v : V) (s : AffineSubspace k P) : v +ᵥ s = s.map (AffineEquiv.constVAdd k P v) :=
  rfl

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