convex_iff_pairwise_pos — Mathlib

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

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