English
Star-convexity of a set is equivalent to a particular pointwise-addition condition using a and b with a+b=1 and a,b≥0.
Русский
Звездообразность множества эквивалентна условию на точечное сложение: при a,b≥0 и a+b=1 множество сохраняет подмножество s при a·{x}+b·s.
LaTeX
$$$$StarConvex_{\mathbb{K}}(x,s) \iff \forall a,b\ge 0,\ a+b=1 \Rightarrow a\cdot\{x\} + b\cdot s \subseteq s.$$$$
Lean4
/-- Alternative definition of star-convexity, in terms of pointwise set operations. -/
theorem starConvex_iff_pointwise_add_subset :
StarConvex 𝕜 x s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • { x } + b • s ⊆ s :=
by
refine ⟨?_, fun h y hy a b ha hb hab => h ha hb hab (add_mem_add (smul_mem_smul_set <| mem_singleton _) ⟨_, hy, rfl⟩)⟩
rintro hA a b ha hb hab w ⟨au, ⟨u, rfl : u = x, rfl⟩, bv, ⟨v, hv, rfl⟩, rfl⟩
exact hA hv ha hb hab
