# 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))))))