Documentation

Mathlib.Data.Int.ConditionallyCompleteOrder

forms a conditionally complete linear order #

The integers form a conditionally complete linear order.

Equations
  • One or more equations did not get rendered due to their size.
theorem Int.csSup_eq_greatest_of_bdd {s : Set } [DecidablePred fun (x : ) => x s] (b : ) (Hb : zs, z b) (Hinh : ∃ (z : ), z s) :
sSup s = (b.greatestOfBdd Hb Hinh)
@[simp]
theorem Int.csInf_eq_least_of_bdd {s : Set } [DecidablePred fun (x : ) => x s] (b : ) (Hb : zs, b z) (Hinh : ∃ (z : ), z s) :
sInf s = (b.leastOfBdd Hb Hinh)
@[simp]
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