English
Let I be a nonempty subset of a ConditionallyCompleteLinearOrder with a top and bottom and LocallyFiniteOrder. Then I is order-connected if and only if I equals the closed interval between its infimum and supremum, i.e. I = [sInf(I), sSup(I)].
Русский
Пусть I ⊆ α, где α — упорядоченное линейное множество с условной полнотой, с нижней и верхней границами и локально конечным порядком. Тогда I является ордированной связностью (ord-connected) тогда и только тогда, когда I совпадает с замкнутым интервалом между наименьшей нижней границей и наибольшей верхней границей I, то есть I = [sInf(I), sSup(I)].
LaTeX
$$$ I \neq \varnothing \Rightarrow ( \operatorname{OrdConnected}(I) \iff I = Icc (sInf I) (sSup I) ) $$$
Lean4
/-- A version of `Set.Nonempty.ordConnected_iff_of_bdd` for complete linear orders, such as `Fin n`,
in which the explicit boundedness hypotheses are not necessary. -/
theorem ordConnected_iff_of_bdd' [ConditionallyCompleteLinearOrder α] [OrderTop α] [OrderBot α] [LocallyFiniteOrder α]
(h₀ : I.Nonempty) : I.OrdConnected ↔ I = Icc (sInf I) (sSup I) :=
h₀.ordConnected_iff_of_bdd (OrderBot.bddBelow I)
(OrderTop.bddAbove I)
/- TODO The `LocallyFiniteOrder` assumption here is probably too strong (e.g., it rules out `ℝ`
for which this result holds). However at the time of writing it is not clear what weaker
assumption(s) should replace it. -/
