mathlib documentation

data.int.order

forms a conditionally complete linear order #

The integers form a conditionally complete linear order.

@[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) :
Sup s = (b.greatest_of_bdd Hb Hinh)
@[simp]
theorem int.cSup_empty  :
theorem int.cSup_of_not_bdd_above {s : set } (h : ¬bdd_above s) :
Sup s = 0
theorem int.cInf_eq_least_of_bdd {s : set } [decidable_pred (λ (_x : ), _x s)] (b : ) (Hb : ∀ (z : ), z sb z) (Hinh : ∃ (z : ), z s) :
Inf s = (b.least_of_bdd Hb Hinh)
@[simp]
theorem int.cInf_empty  :
theorem int.cInf_of_not_bdd_below {s : set } (h : ¬bdd_below s) :
Inf s = 0
theorem int.cSup_mem {s : set } (h1 : s.nonempty) (h2 : bdd_above s) :
Sup s s
theorem int.cInf_mem {s : set } (h1 : s.nonempty) (h2 : bdd_below s) :
Inf s s