# Documentation

Mathlib.Data.Int.ConditionallyCompleteOrder

## ℤ 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 : } [inst : DecidablePred fun x => x s] (b : ) (Hb : ∀ (z : ), z sz b) (Hinh : z, z s) :
supₛ s = ↑(Int.greatestOfBdd b Hb Hinh)
@[simp]
theorem Int.csupₛ_empty :
= 0
theorem Int.cinfₛ_eq_least_of_bdd {s : } [inst : DecidablePred fun x => x s] (b : ) (Hb : ∀ (z : ), z sb z) (Hinh : z, z s) :
infₛ s = ↑(Int.leastOfBdd b Hb Hinh)
@[simp]
theorem Int.cinfₛ_empty :
= 0
theorem Int.csupₛ_mem {s : } (h1 : ) (h2 : ) :
theorem Int.cinfₛ_mem {s : } (h1 : ) (h2 : ) :