convex_iff_pointwise_add_subset — Mathlib

English

A set is convex iff for all a,b ≥ 0 with a+b=1, a·s + b·s ⊆ s.

Русский

Множество выпукло тогда и только тогда, когда для любых a,b ≥ 0 с a+b=1 выполняется a·s + b·s ⊆ s.

LaTeX

$$$\mathrm{Convex } 𝕜 s \iff ∀ a,b≥0,\ a+b=1 \Rightarrow a·s + b·s \subseteq s$$$

Lean4

/-- Alternative definition of set convexity, in terms of pointwise set operations. -/
theorem convex_iff_pointwise_add_subset : Convex 𝕜 s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s :=
  Iff.intro
    (by
      rintro hA a b ha hb hab w ⟨au, ⟨u, hu, rfl⟩, bv, ⟨v, hv, rfl⟩, rfl⟩
      exact hA hu hv ha hb hab)
    fun h _ hx _ hy _ _ ha hb hab => (h ha hb hab) (Set.add_mem_add ⟨_, hx, rfl⟩ ⟨_, hy, rfl⟩)

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