convexHull_vadd — Mathlib

English

The convex hull is invariant under translation: translating a set by a fixed vector commutes with taking its convex hull.

Русский

Выпуклая оболочка инвариантна относительно переноса: перенос множества на фиксированный вектор коммутирует с взятием выпуклой оболочки.

LaTeX

$$$\\operatorname{convHull}_{\\mathbb{k}}(x + S) = x + \\operatorname{convHull}_{\\mathbb{k}}(S),$$$

Lean4

theorem convexHull_vadd (x : E) (s : Set E) : convexHull 𝕜 (x +ᵥ s) = x +ᵥ convexHull 𝕜 s :=
  (AffineEquiv.constVAdd 𝕜 _ x).toAffineMap.image_convexHull s |>.symm

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