ℤ forms a conditionally complete linear order #
The integers form a conditionally complete linear order.
@[protected, instance]
Equations
- int.conditionally_complete_linear_order = {sup := lattice.sup linear_order.to_lattice, le := linear_order.le int.linear_order, lt := linear_order.lt int.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := int.conditionally_complete_linear_order._proof_1, le_sup_right := int.conditionally_complete_linear_order._proof_2, sup_le := int.conditionally_complete_linear_order._proof_3, inf := lattice.inf linear_order.to_lattice, inf_le_left := int.conditionally_complete_linear_order._proof_4, inf_le_right := int.conditionally_complete_linear_order._proof_5, le_inf := int.conditionally_complete_linear_order._proof_6, Sup := λ (s : set ℤ), dite (s.nonempty ∧ bdd_above s) (λ (h : s.nonempty ∧ bdd_above s), ↑((classical.some _).greatest_of_bdd _ _)) (λ (h : ¬(s.nonempty ∧ bdd_above s)), 0), Inf := λ (s : set ℤ), dite (s.nonempty ∧ bdd_below s) (λ (h : s.nonempty ∧ bdd_below s), ↑((classical.some _).least_of_bdd _ _)) (λ (h : ¬(s.nonempty ∧ bdd_below s)), 0), le_cSup := int.conditionally_complete_linear_order._proof_13, cSup_le := int.conditionally_complete_linear_order._proof_14, cInf_le := int.conditionally_complete_linear_order._proof_15, le_cInf := int.conditionally_complete_linear_order._proof_16, le_total := _, decidable_le := linear_order.decidable_le int.linear_order, decidable_eq := linear_order.decidable_eq int.linear_order, decidable_lt := linear_order.decidable_lt int.linear_order, max_def := _, min_def := _}
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) :
has_Sup.Sup s = ↑(b.greatest_of_bdd Hb Hinh)
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) :
has_Inf.Inf s = ↑(b.least_of_bdd Hb Hinh)