convexHull_sub — Mathlib

English

The convex hull operation is compatible with subtraction of sets: conv(R, s - t) = conv(R, s) - conv(R, t).

Русский

Выпуклая оболочка совместима с вычитанием множеств: conv(R, s − t) = conv(R, s) − conv(R, t).

LaTeX

$$$\operatorname{conv}(R, s - t) = \operatorname{conv}(R, s) - \operatorname{conv}(R, t)$$$

Lean4

theorem convexHull_sub (s t : Set E) : convexHull R (s - t) = convexHull R s - convexHull R t := by
  simp_rw [sub_eq_add_neg, convexHull_add, ← convexHull_neg]

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