Documentation

Mathlib.Data.Int.LeastGreatest

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 #

Main statements #

Tags #

integer numbers, least element, greatest element

def Int.leastOfBdd {P : Prop} [DecidablePred 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 = b + (Nat.find ),
Instances For
    theorem Int.exists_least_of_bdd {P : Prop} (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 : Prop} [DecidablePred 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 : Prop} [DecidablePred 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 = match (-b).leastOfBdd with | lb, => -lb,
    Instances For
      theorem Int.exists_greatest_of_bdd {P : Prop} (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 : Prop} [DecidablePred 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)