Documentation

Mathlib.Data.Int.ConditionallyCompleteOrder

forms a conditionally complete linear order #

The integers form a conditionally complete linear order.

theorem Int.csSup_eq_greatest_of_bdd {s : Set } [DecidablePred fun x => x s] (b : ) (Hb : ∀ (z : ), z sz b) (Hinh : z, z s) :
sSup s = ↑(Int.greatestOfBdd b Hb Hinh)
@[simp]
theorem Int.csInf_eq_least_of_bdd {s : Set } [DecidablePred fun x => x s] (b : ) (Hb : ∀ (z : ), z sb z) (Hinh : z, z s) :
sInf s = ↑(Int.leastOfBdd b Hb Hinh)
@[simp]
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