mathlib3 documentation

data.int.conditionally_complete_order

forms a conditionally complete linear order #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 s z b) (Hinh : (z : ), z s) :
@[simp]
theorem int.cInf_eq_least_of_bdd {s : set } [decidable_pred (λ (_x : ), _x s)] (b : ) (Hb : (z : ), z s b 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) :