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.

source

@[protected, instance]

noncomputable def int.conditionally_complete_linear_order :

conditionally_complete_linear_order ℤ

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 := _}

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) :

has_Sup.Sup s = ↑(b.greatest_of_bdd Hb Hinh)

source

@[simp]

theorem int.cSup_empty :

has_Sup.Sup ∅ = 0

source

theorem int.cSup_of_not_bdd_above {s : set ℤ} (h : ¬bdd_above s) :

has_Sup.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) :

has_Inf.Inf s = ↑(b.least_of_bdd Hb Hinh)

source

@[simp]

theorem int.cInf_empty :

has_Inf.Inf ∅ = 0

source

theorem int.cInf_of_not_bdd_below {s : set ℤ} (h : ¬bdd_below s) :

has_Inf.Inf s = 0

source

theorem int.cSup_mem {s : set ℤ} (h1 : s.nonempty) (h2 : bdd_above s) :

has_Sup.Sup s ∈ s

source

theorem int.cInf_mem {s : set ℤ} (h1 : s.nonempty) (h2 : bdd_below s) :

has_Inf.Inf s ∈ s

ℤ forms a conditionally complete linear order #

`ℤ` forms a conditionally complete linear order #