Least upper bound and greatest lower bound properties for integers #

In this file we prove that a bounded above nonempty set of integers has the greatest element, and a counterpart of this statement for the least element.

Main definitions #

int.least_of_bdd: if P : ℤ → Prop is a decidable predicate, b is a lower bound of the set {m | P m}, and there exists m : ℤ such that P m (this time, no witness is required), then int.least_of_bdd returns the least number m such that P m, together with proofs of P m and of the minimality. This definition is computable and does not rely on the axiom of choice.
int.greatest_of_bdd: a similar definition with all inequalities reversed.

Main statements #

int.exists_least_of_bdd: if P : ℤ → Prop is a predicate such that the set {m : P m} is bounded below and nonempty, then this set has the least element. This lemma uses classical logic to avoid assumption [decidable_pred P]. See int.least_of_bdd for a constructive counterpart.
int.coe_least_of_bdd_eq: (int.least_of_bdd b Hb Hinh : ℤ) does not depend on b.
int.exists_greatest_of_bdd, int.coe_greatest_of_bdd_eq: versions of the above lemmas with all inequalities reversed.

Tags #

integer numbers, least element, greatest element

source

def int.least_of_bdd {P : ℤ → Prop} [decidable_pred P] (b : ℤ) (Hb : ∀ (z : ℤ), P z → b ≤ z) (Hinh : ∃ (z : ℤ), P z) :

{lb // P lb ∧ ∀ (z : ℤ), P z → lb ≤ z}

A computable version of exists_least_of_bdd: given a decidable predicate on the integers, with an explicit lower bound and a proof that it is somewhere true, return the least value for which the predicate is true.

Equations

b.least_of_bdd Hb Hinh = have EX : ∃ (n : ℕ), P (b + ↑n), from _, ⟨b + ↑(nat.find EX), _⟩
_ = _
_ = _

source

theorem int.exists_least_of_bdd {P : ℤ → Prop} (Hbdd : ∃ (b : ℤ), ∀ (z : ℤ), P z → b ≤ z) (Hinh : ∃ (z : ℤ), P z) :

∃ (lb : ℤ), P lb ∧ ∀ (z : ℤ), P z → lb ≤ z

If P : ℤ → Prop is a predicate such that the set {m : P m} is bounded below and nonempty, then this set has the least element. This lemma uses classical logic to avoid assumption [decidable_pred P]. See int.least_of_bdd for a constructive counterpart.

source

theorem int.coe_least_of_bdd_eq {P : ℤ → Prop} [decidable_pred P] {b b' : ℤ} (Hb : ∀ (z : ℤ), P z → b ≤ z) (Hb' : ∀ (z : ℤ), P z → b' ≤ z) (Hinh : ∃ (z : ℤ), P z) :

↑(b.least_of_bdd Hb Hinh) = ↑(b'.least_of_bdd Hb' Hinh)

source

def int.greatest_of_bdd {P : ℤ → Prop} [decidable_pred P] (b : ℤ) (Hb : ∀ (z : ℤ), P z → z ≤ b) (Hinh : ∃ (z : ℤ), P z) :

{ub // P ub ∧ ∀ (z : ℤ), P z → z ≤ ub}

A computable version of exists_greatest_of_bdd: given a decidable predicate on the integers, with an explicit upper bound and a proof that it is somewhere true, return the greatest value for which the predicate is true.

Equations

b.greatest_of_bdd Hb Hinh = have Hbdd' : ∀ (z : ℤ), P (-z) → -b ≤ z, from _, have Hinh' : ∃ (z : ℤ), P (-z), from _, int.greatest_of_bdd._match_2 ((-b).least_of_bdd Hbdd' Hinh')
int.greatest_of_bdd._match_2 ⟨lb, _⟩ = ⟨-lb, _⟩
_ = _

source

theorem int.exists_greatest_of_bdd {P : ℤ → Prop} (Hbdd : ∃ (b : ℤ), ∀ (z : ℤ), P z → z ≤ b) (Hinh : ∃ (z : ℤ), P z) :

∃ (ub : ℤ), P ub ∧ ∀ (z : ℤ), P z → z ≤ ub

If P : ℤ → Prop is a predicate such that the set {m : P m} is bounded above and nonempty, then this set has the greatest element. This lemma uses classical logic to avoid assumption [decidable_pred P]. See int.greatest_of_bdd for a constructive counterpart.

source

theorem int.coe_greatest_of_bdd_eq {P : ℤ → Prop} [decidable_pred P] {b b' : ℤ} (Hb : ∀ (z : ℤ), P z → z ≤ b) (Hb' : ∀ (z : ℤ), P z → z ≤ b') (Hinh : ∃ (z : ℤ), P z) :

↑(b.greatest_of_bdd Hb Hinh) = ↑(b'.greatest_of_bdd Hb' Hinh)