English
If s is order-connected in an ordered module and every element of s is comparable with x∈s, then s is star-convex at x.
Русский
Если s – упорядоченное связное множество в упорядоченном модуле и все элементы s сравнимы с x ∈ s, то s звёздочно выпукло относительно x.
LaTeX
$$$\\text{Set.OrdConnected}.starConvex( s, x)$ при условии: s OrdConnected, x∈s и ∀ y∈s, x ≤ y или y ≤ x$$
Lean4
/-- If `s` is an order-connected set in an ordered module over an ordered semiring
and all elements of `s` are comparable with `x ∈ s`, then `s` is `StarConvex` at `x`. -/
theorem starConvex [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [PartialOrder E] [IsOrderedAddMonoid E] [Module 𝕜 E]
[PosSMulMono 𝕜 E] {x : E} {s : Set E} (hs : s.OrdConnected) (hx : x ∈ s) (h : ∀ y ∈ s, x ≤ y ∨ y ≤ x) :
StarConvex 𝕜 x s := by
intro y hy a b ha hb hab
obtain hxy | hyx := h _ hy
· refine hs.out hx hy (mem_Icc.2 ⟨?_, ?_⟩)
·
calc
x = a • x + b • x := (Convex.combo_self hab _).symm
_ ≤ a • x + b • y := by gcongr
calc
a • x + b • y ≤ a • y + b • y := by gcongr
_ = y := Convex.combo_self hab _
· refine hs.out hy hx (mem_Icc.2 ⟨?_, ?_⟩)
·
calc
y = a • y + b • y := (Convex.combo_self hab _).symm
_ ≤ a • x + b • y := by gcongr
calc
a • x + b • y ≤ a • x + b • x := by gcongr
_ = x := Convex.combo_self hab _
