mathlib documentation

data.int.least_greatest

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.least_of_bdd {P : → Prop} [decidable_pred 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
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 [decidable_pred P]. See int.least_of_bdd for a constructive counterpart.

theorem int.coe_least_of_bdd_eq {P : → Prop} [decidable_pred P] {b b' : } (Hb : ∀ (z : ), P zb z) (Hb' : ∀ (z : ), P zb' z) (Hinh : ∃ (z : ), P z) :
(b.least_of_bdd Hb Hinh) = (b'.least_of_bdd Hb' Hinh)
def int.greatest_of_bdd {P : → Prop} [decidable_pred 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.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, _⟩
  • _ = _
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 [decidable_pred P]. See int.greatest_of_bdd for a constructive counterpart.

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