convex_iff_add_mem — Mathlib

English

A set is convex iff for all x,y ∈ s and all a,b ≥ 0 with a+b=1, the point a·x + b·y lies in s.

Русский

Множество выпукло эквивалентно тому, что для любых x,y ∈ s и неотрицательных a,b с a+b=1, сумма a·x + b·y ∈ s.

LaTeX

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

Lean4

theorem convex_iff_add_mem :
    Convex 𝕜 s ↔ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s := by
  simp_rw [convex_iff_segment_subset, segment_subset_iff]

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