mathlib documentation

data.int.order

ℤ forms a conditionally complete linear order #

The integers form a conditionally complete linear order.

source
@[protected, instance]
noncomputable def int.conditionally_complete_linear_order  :
conditionally_complete_linear_order ℤ
Equations
source
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) :
Sup s = ↑(b.greatest_of_bdd Hb Hinh)
source
@[simp]
theorem int.cSup_empty  :
Sup ∅ = 0
source
theorem int.cSup_of_not_bdd_above {s : set ℤ} (h : ¬bdd_above s) :
Sup s = 0
source
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) :
Inf s = ↑(b.least_of_bdd Hb Hinh)
source
@[simp]
theorem int.cInf_empty  :
Inf ∅ = 0
source
theorem int.cInf_of_not_bdd_below {s : set ℤ} (h : ¬bdd_below s) :
Inf s = 0
source
theorem int.cSup_mem {s : set ℤ} (h1 : s.nonempty) (h2 : bdd_above s) :
Sup s ∈ s
source
theorem int.cInf_mem {s : set ℤ} (h1 : s.nonempty) (h2 : bdd_below s) :
Inf s ∈ s