ℤ forms a conditionally complete linear order

The integers form a conditionally complete linear order.

ink

instance instConditionallyCompleteLinearOrderInt : ConditionallyCompleteLinearOrder ℤ

Equations

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

ink

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)

ink

@[simp]

theorem Int.csupₛ_empty : supₛ ∅ = 0

ink

theorem Int.csupₛ_of_not_bdd_above {s : Set ℤ} (h : ¬BddAbove s) : supₛ s = 0

ink

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)

ink

@[simp]

theorem Int.cinfₛ_empty : infₛ ∅ = 0

ink

theorem Int.cinfₛ_of_not_bdd_below {s : Set ℤ} (h : ¬BddBelow s) : infₛ s = 0

ink

theorem Int.csupₛ_mem {s : Set ℤ} (h1 : Set.Nonempty s) (h2 : BddAbove s) : supₛ s ∈ s

ink

theorem Int.cinfₛ_mem {s : Set ℤ} (h1 : Set.Nonempty s) (h2 : BddBelow s) : infₛ s ∈ s