ℤ
forms a conditionally complete linear order #
The integers form a conditionally complete linear order.
Equations
- One or more equations did not get rendered due to their size.
theorem
Int.csupₛ_eq_greatest_of_bdd
{s : Set ℤ}
[inst : DecidablePred fun x => x ∈ s]
(b : ℤ)
(Hb : ∀ (z : ℤ), z ∈ s → z ≤ b)
(Hinh : ∃ z, z ∈ s)
:
supₛ s = ↑(Int.greatestOfBdd b Hb Hinh)
theorem
Int.cinfₛ_eq_least_of_bdd
{s : Set ℤ}
[inst : DecidablePred fun x => x ∈ s]
(b : ℤ)
(Hb : ∀ (z : ℤ), z ∈ s → b ≤ z)
(Hinh : ∃ z, z ∈ s)
:
infₛ s = ↑(Int.leastOfBdd b Hb Hinh)