add — Mathlib

English

Convex if and only if the pairwise positive combination property holds.

Русский

Выпуклость эквивалентна парной положительной комбинации.

LaTeX

$$$\Convex 𝕜 s \iff s.\text{Pairwise} (\lambda x y, \forall a,b>0, a x + b y \in s)$$$

Lean4

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

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