starConvex_iff_div — Mathlib

English

Star-convexity is equivalent to a division-based criterion: for all y∈s, a,b≥0 with a+b>0, the convex combination (a/(a+b))x+(b/(a+b))y lies in s.

Русский

Звёздочная выпуклость равносильна критерию через деление: для всех y∈s и a,b≥0, a+b>0, выражение (a/(a+b))x+(b/(a+b))y принадлежит s.

LaTeX

$$$\\text{StarConvex}_{\\mathbb{K}}(x,s) \\iff \\forall y\\in s, \\forall a,b≥0, 0

Lean4

/-- Alternative definition of star-convexity, using division. -/
theorem starConvex_iff_div :
    StarConvex 𝕜 x s ↔
      ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s :=
  ⟨fun h y hy a b ha hb hab => by
    apply h hy
    · positivity
    · positivity
    · rw [← add_div]
      exact div_self hab.ne', fun h y hy a b ha hb hab =>
    by
    have h' := h hy ha hb
    rw [hab, div_one, div_one] at h'
    exact h' zero_lt_one⟩

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