English
Let 𝕜 be a field with a linear order and a strict ordering property. If x ∈ s, then s is star-shaped with center x if and only if s is order-connected.
Русский
Пусть 𝕜 является полем с линейным порядком и строгой упорядоченностью. При условии x ∈ s множество s звездообразно относительно центра x тогда и только тогда, когда s упорядочно связно.
LaTeX
$$$x \in s \;\Longrightarrow\; \mathrm{StarConvex}_{\mathbb{K}}(x,s) \iff s\ \text{is order-connected}$$$
Lean4
theorem starConvex_iff_ordConnected [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) :
StarConvex 𝕜 x s ↔ s.OrdConnected := by
simp_rw [ordConnected_iff_uIcc_subset_left hx, starConvex_iff_segment_subset, segment_eq_uIcc]
