English
If a set S is OrdConnected and is a chain with respect to the usual order, then S is convex: between any two points of S, the whole segment lies in S.
Русский
Если множество S упорядочно-соединено и образует цепочку по обычному порядку, то S выпукло: между любыми двумя точками S лежит весь отрезок внутри S.
LaTeX
$$$S\text{ is OrdConnected and IsChain}(\le, S) \Rightarrow \operatorname{Convex}_{\mathbb{K}}(S).$$$
Lean4
theorem convex_of_chain [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [PartialOrder E] [IsOrderedAddMonoid E]
[Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} (hs : s.OrdConnected) (h : IsChain (· ≤ ·) s) : Convex 𝕜 s :=
by
refine convex_iff_segment_subset.mpr fun x hx y hy => ?_
obtain hxy | hyx := h.total hx hy
· exact (segment_subset_Icc hxy).trans (hs.out hx hy)
· rw [segment_symm]
exact (segment_subset_Icc hyx).trans (hs.out hy hx)
