English
Let I ⊆ Z be nonempty with both a lower and upper bound. 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 (in integers).
Русский
Пусть I ⊆ ℤ непусто и ограничено снизу и сверху. Тогда I = [sInf I, sSup I], эквивалентно условию: для любых x,y ∈ I, Disjoint(Ioo x y, I) ⇒ y ≤ x + 1.
LaTeX
$$$ I \neq \varnothing \Rightarrow BddBelow(I) \land 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_int {I : Set ℤ} (h₀ : I.Nonempty) (h₁ : BddBelow I) (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 h₁ h₂, ordConnected_iff_disjoint_Ioo_empty, Int.succ]
