# 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.leastOfBdd: 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.leastOfBdd 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.greatestOfBdd: 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 [DecidablePred P]. See Int.leastOfBdd for a constructive counterpart.

• Int.coe_leastOfBdd_eq: (Int.leastOfBdd 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

def Int.leastOfBdd {P : } [] (b : ) (Hb : ∀ (z : ), P zb z) (Hinh : ∃ (z : ), P z) :
{ lb : // P lb ∀ (z : ), P zlb 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.leastOfBdd Hb Hinh = let_fun EX := ; b + (Nat.find EX),
Instances For
theorem Int.exists_least_of_bdd {P : } (Hbdd : ∃ (b : ), ∀ (z : ), P zb z) (Hinh : ∃ (z : ), P z) :
∃ (lb : ), P lb ∀ (z : ), P zlb 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 [DecidablePred P]. See Int.leastOfBdd for a constructive counterpart.

theorem Int.coe_leastOfBdd_eq {P : } [] {b : } {b' : } (Hb : ∀ (z : ), P zb z) (Hb' : ∀ (z : ), P zb' z) (Hinh : ∃ (z : ), P z) :
(b.leastOfBdd Hb Hinh) = (b'.leastOfBdd Hb' Hinh)
def Int.greatestOfBdd {P : } [] (b : ) (Hb : ∀ (z : ), P zz b) (Hinh : ∃ (z : ), P z) :
{ ub : // P ub ∀ (z : ), P zz 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.greatestOfBdd Hb Hinh = let_fun Hbdd' := ; let_fun Hinh' := ; match (-b).leastOfBdd Hbdd' Hinh' with | lb, => -lb,
Instances For
theorem Int.exists_greatest_of_bdd {P : } (Hbdd : ∃ (b : ), ∀ (z : ), P zz b) (Hinh : ∃ (z : ), P z) :
∃ (ub : ), P ub ∀ (z : ), P zz 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 [DecidablePred P]. See Int.greatestOfBdd for a constructive counterpart.

theorem Int.coe_greatestOfBdd_eq {P : } [] {b : } {b' : } (Hb : ∀ (z : ), P zz b) (Hb' : ∀ (z : ), P zz b') (Hinh : ∃ (z : ), P z) :
(b.greatestOfBdd Hb Hinh) = (b'.greatestOfBdd Hb' Hinh)