convex_iff_forall_pos — Mathlib

English

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

Русский

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

LaTeX

$$$\Convex 𝕜 s \iff \forall x \in s, \forall y \in s, \forall a,b \,(0 < a) \to (0 < b) \to a+b=1 \to a \cdot x + b \cdot y \in s$$$

Lean4

theorem convex_iff_forall_pos :
    Convex 𝕜 s ↔ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s :=
  forall₂_congr fun _ => starConvex_iff_forall_pos

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