pointwiseVAdd — Mathlib

English

If v is a vector and p is a point with p ∈ s, then v + p ∈ v + s; conversely, membership is preserved under this translation.

Русский

Если v — вектор и p — точка, принадлежащая s, то v + p принадлежит переносимой области v + s; обратно принадлежность сохраняется под такой трансляцией.

LaTeX

$$$v + p \in v + s \iff p \in s.$$$

Lean4

/-- The additive action on an affine subspace corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale. -/
protected def pointwiseVAdd : VAdd V (AffineSubspace k P) where vadd x s := s.map (AffineEquiv.constVAdd k P x)

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