ℤ forms a conditionally complete linear order

The integers form a conditionally complete linear order.

instance instConditionallyCompleteLinearOrderInt : ConditionallyCompleteLinearOrder ℤ

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)

@[simp]

theorem Int.csSup_empty : sSup ∅ = 0

theorem Int.csSup_of_not_bdd_above {s : Set ℤ} (h : ¬BddAbove s) : sSup s = 0

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)

@[simp]

theorem Int.csInf_empty : sInf ∅ = 0

theorem Int.csInf_of_not_bdd_below {s : Set ℤ} (h : ¬BddBelow s) : sInf s = 0

theorem Int.csSup_mem {s : Set ℤ} (h1 : Set.Nonempty s) (h2 : BddAbove s) : sSup s ∈ s

theorem Int.csInf_mem {s : Set ℤ} (h1 : Set.Nonempty s) (h2 : BddBelow s) : sInf s ∈ s