English
If x ∈ s, StarConvex 𝕜 x s is equivalent to the statement involving all y ∈ s with y ≠ x and all a,b > 0 with a+b = 1, that a x + b y ∈ s.
Русский
Если x ∈ s, тогда StarConvex 𝕜 x s эквивалентно условию: для каждого y ∈ s, y ≠ x, и для всех a,b > 0 с a+b=1 то a x + b y ∈ s.
LaTeX
$$$$\starConvex_{\mathbb{K}}(x,s) \iff \forall y \in s,\ x \neq y \Rightarrow \forall a,b>0,\ a+b=1 \Rightarrow a\cdot x + b\cdot y \in s.$$$$
Lean4
theorem starConvex_iff_forall_ne_pos (hx : x ∈ s) :
StarConvex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s :=
by
refine ⟨fun h y hy _ a b ha hb hab => h hy ha.le hb.le hab, ?_⟩
intro h y hy a b ha hb hab
obtain rfl | ha' := ha.eq_or_lt
· rw [zero_add] at hab
rwa [hab, zero_smul, one_smul, zero_add]
obtain rfl | hb' := hb.eq_or_lt
· rw [add_zero] at hab
rwa [hab, zero_smul, one_smul, add_zero]
obtain rfl | hxy := eq_or_ne x y
· rwa [Convex.combo_self hab]
exact h hy hxy ha' hb' hab
