constVAdd_zero — Mathlib

English

Let P be an affine space modeled on a normed vector space V over a field 𝕜. Translating every point of P by the zero vector, i.e. applying constVAdd 𝕜 P (0 : V), yields the identity transformation on P.

Русский

Пусть P — аффинное пространство, моделируемое нормированным векторным пространством V над полем 𝕜. Сдвиг всех точек на нулевой вектор, то есть constVAdd 𝕜 P (0 : V), дает тождественное отображение на P.

LaTeX

$$$\mathrm{constVAdd}_{\mathbb{k}}(P,0) = \mathrm{id}_P$$$

Lean4

@[simp]
theorem constVAdd_zero : constVAdd 𝕜 P (0 : V) = refl 𝕜 P :=
  ext <| zero_vadd V

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