convex_iff_div — Mathlib

English

Under mild field/order assumptions, the midpoint of x and y belongs to a convex set given x,y ∈ s.

Русский

При умеренных условиях поля/порядка середина x и y принадлежит выпуклому множеству, если x,y ∈ s.

LaTeX

$$$$ \\text{midpoint}_{\\mathbb{K}}(x,y) \\in s $$$$

Lean4

/-- Alternative definition of set convexity, using division. -/
theorem convex_iff_div :
    Convex 𝕜 s ↔
      ∀ ⦃x⦄,
        x ∈ s → ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s :=
  forall₂_congr fun _ _ => starConvex_iff_div

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