ℤ forms a conditionally complete linear order

The integers form a conditionally complete linear order.

@[implicit_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)

@[deprecated Int.csSup_eq_greatestOfBdd (since := "2025-12-24")]

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

Alias of Int.csSup_eq_greatestOfBdd.

@[simp]

theorem Int.csSup_empty : sSup ∅ = 0

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

@[deprecated Int.csSup_of_not_bddAbove (since := "2025-12-24")]

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

Alias of Int.csSup_of_not_bddAbove.

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)

@[deprecated Int.csInf_eq_leastOfBdd (since := "2025-12-24")]

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

Alias of Int.csInf_eq_leastOfBdd.

@[simp]

theorem Int.csInf_empty : sInf ∅ = 0

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

@[deprecated Int.csInf_of_not_bddBelow (since := "2025-12-24")]

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

Alias of Int.csInf_of_not_bddBelow.

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