English
A set s is convex iff it is pairwise with the property that certain positive convex combinations lie in s.
Русский
Множество s выпукло тогда, когда оно попарно обладает свойством, что положительные выпуклые комбинации точек принадлежат s.
LaTeX
$$$\Convex 𝕜 s \iff s.Peerwise (\lambda x y, \forall a,b>0, a x + b y \in s)$$$
Lean4
theorem convex_iff_pairwise_pos :
Convex 𝕜 s ↔ s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s :=
by
refine convex_iff_forall_pos.trans ⟨fun h x hx y hy _ => h hx hy, ?_⟩
intro h x hx y hy a b ha hb hab
obtain rfl | hxy := eq_or_ne x y
· rwa [Convex.combo_self hab]
· exact h hx hy hxy ha hb hab