ℤ forms a conditionally complete linear order

The integers form a conditionally complete linear order.

@[instance_reducible]

noncomputable instance Int.instConditionallyCompleteLinearOrder : ConditionallyCompleteLinearOrder ℤ

Equations

• One or more equations did not get rendered due to their size.

theorem Int.csSup_eq_greatestOfBdd {s : Set ℤ} [DecidablePred fun (x : ℤ) => x ∈ s] (b : ℤ) (Hb : ∀ z ∈ s, z ≤ b) (Hinh : ∃ (z : ℤ), z ∈ s) : sSup s = ↑(b.greatestOfBdd Hb Hinh)

@[simp]

theorem Int.csSup_empty : sSup ∅ = 0

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

theorem Int.csInf_eq_leastOfBdd {s : Set ℤ} [DecidablePred fun (x : ℤ) => x ∈ s] (b : ℤ) (Hb : ∀ z ∈ s, b ≤ z) (Hinh : ∃ (z : ℤ), z ∈ s) : sInf s = ↑(b.leastOfBdd Hb Hinh)

@[simp]

theorem Int.csInf_empty : sInf ∅ = 0

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

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

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