mathlib documentation

data.int.order

forms a conditionally complete linear order #

The integers form a conditionally complete linear order.

@[protected, instance]
Equations
theorem int.cSup_eq_greatest_of_bdd {s : set } [decidable_pred (λ (_x : ), _x s)] (b : ) (Hb : ∀ (z : ), z sz b) (Hinh : ∃ (z : ), z s) :
@[simp]
theorem int.cInf_eq_least_of_bdd {s : set } [decidable_pred (λ (_x : ), _x s)] (b : ) (Hb : ∀ (z : ), z sb z) (Hinh : ∃ (z : ), z s) :
@[simp]
theorem int.cSup_mem {s : set } (h1 : s.nonempty) (h2 : bdd_above s) :
theorem int.cInf_mem {s : set } (h1 : s.nonempty) (h2 : bdd_below s) :