# Defines upper bound and supremum. Contains a theorem that there is at most one supremum.
param (PROP /peano_new/prop.ghi () "")
param (PREDICATE /peano_new/predicate/all.ghi (PROP) "")
param (REALS /peano_new/arithmetic/reals/common.ghi (PROP PREDICATE) "")
param (SET_MIN /peano_new/set_min.ghi (PROP PREDICATE) "")
tvar (wff ph ps ch th ta)
tvar (nat A B C D ep)
var (nat v w x y z)
tvar (set S T U V)
##
## redirect supremum-def.gh
##
term (wff (upperbound A S))
term (wff (supremum A S))
##
Def. Set Upper Bound
stmt (df-upperbound ((S x) (A x)) () (<-> (upperbound A S) (A. x (-> (e. x S) (<= x A)))))
## Equivalence for upperbound ##
stmt (upperboundeq1 () () (-> (= A B) (<-> (upperbound A S) (upperbound B S))))
## Equivalence for upperbound ##
stmt (upperboundseq2 () () (-> (=_ S T) (<-> (upperbound A S) (upperbound A T))))
## Supremum Definition
stmt (df-supremum ((S x)(A x)) () (<-> (supremum A S) (/\ (upperbound A S) (-. (E. x (/\ (upperbound x S) (< x A)))))))
## Equivalence for supremum ##
stmt (supremumeq1 () () (-> (= A B) (<-> (supremum A S) (supremum B S))))
## Equivalence for supremum ##
stmt (supremumseq2 () () (-> (=_ S T) (<-> (supremum A S) (supremum A T))))
## There is at most one supremum
stmt (supremummo ((S x)) () (E* x (supremum x S)))
## No upper bounds below the supremum
stmt (belowSupremum ((S y)(A y)(ep y)) () (-> (/\ (> ep (0)) (supremum A S)) (E. y (/\ (e. y S) (> y (- A ep))))))