English
Let 𝕜 be a linearly ordered field. If x ∈ s and s is star-convex at x, then s is order-connected (OrdConnected).
Русский
Пусть 𝕜 — линейно упорядоченное поле. Если x ∈ s и s звездообразно выпукла относительно x, то s является OrdConnected (упорядочно связно).
LaTeX
$$$$\text{If } x \in s \text{ and } StarConvex_{\mathbb{K}}(x,s) \text{, then } s \text{ is OrdConnected.}$$$$
Lean4
/-- Star-convexity of sets. `s` is star-convex at `x` if every segment from `x` to a point in `s` is
contained in `s`. -/
def StarConvex (𝕜 : Type*) {E : Type*} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (x : E) (s : Set E) :
Prop :=
∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
