English
Let I be a nonempty subset of N that is bounded above. Then I = [sInf I, sSup I] if and only if for all x ∈ I and y ∈ I, Disjoint(Ioo x y, I) implies y ≤ x + 1.
Русский
Пусть I ⊆ ℕ не пусто и ограничено сверху. Тогда I = [sInf(I), sSup(I)] тогда и только тогда, когда для любых x ∈ I и y ∈ I выполняется: если Ioo(x,y) не содержит элементов из I, то y ≤ x + 1.
LaTeX
$$$ I \neq \varnothing \Rightarrow BddAbove(I) \Rightarrow ( I = Icc (sInf I) (sSup I) \iff \forall x \in I \forall y \in I ( \operatorname{Disjoint}(Ioo x y, I) \Rightarrow y \le x+1 ) ) $$$
Lean4
theorem eq_Icc_iff_nat {I : Set ℕ} (h₀ : I.Nonempty) (h₂ : BddAbove I) :
I = Icc (sInf I) (sSup I) ↔ ∀ᵉ (x ∈ I) (y ∈ I), Disjoint (Ioo x y) I → y ≤ x + 1 := by
simp [← h₀.ordConnected_iff_of_bdd (OrderBot.bddBelow I) h₂, ordConnected_iff_disjoint_Ioo_empty]
