ℤ
forms a conditionally complete linear order #
The integers form a conditionally complete linear order.
theorem
Int.csSup_eq_greatest_of_bdd
{s : Set ℤ}
[DecidablePred fun x => x ∈ s]
(b : ℤ)
(Hb : ∀ (z : ℤ), z ∈ s → z ≤ b)
(Hinh : ∃ z, z ∈ s)
:
sSup s = ↑(Int.greatestOfBdd b Hb Hinh)
theorem
Int.csInf_eq_least_of_bdd
{s : Set ℤ}
[DecidablePred fun x => x ∈ s]
(b : ℤ)
(Hb : ∀ (z : ℤ), z ∈ s → b ≤ z)
(Hinh : ∃ z, z ∈ s)
:
sInf s = ↑(Int.leastOfBdd b Hb Hinh)