add — Mathlib

English

If t is star-convex at x and u is star-convex at y, then their sum is star-convex at x+y with the sum set.

Русский

Если t звездо-конвексно в точке x и u звездо-конвексно в точке y, то их сумма звездо-конвексна в точке x+y на множествах s+t.

LaTeX

$$$$ \text{If } \text{StarConvex}(x,s) \text{ and } \text{StarConvex}(y,t), \text{ then } \text{StarConvex}(x+y, s+t). $$$$

Lean4

theorem add {t : Set E} (hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 y t) : StarConvex 𝕜 (x + y) (s + t) :=
  by
  rw [← add_image_prod]
  exact (hs.prod ht).is_linear_image IsLinearMap.isLinearMap_add

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