# List of theorems

List of theorems in peano_new/arithmetic/reals/supremum.gh:

supremumeu # <context> # This theorem is part of a series of proofs about the properties of the supremum # given the <a href="/edit/peano_new/arithmetic/reals/supremum-ax.ghi/ax-sup"> completeness axiom</a>. # for real numbers. All numbers are assumed to be real. # </context> # <title> Existence of a unique supremum </title>
(-> (/\ (-. (=_ S ({/}))) (E. x (upperbound x S))) (E! y (supremum y S)))
df-sup # <title> Def. Supremum of a Set </title> # <summary> # Define the supremum of a set. This is different from # <a href="../supremum-def.gh/df-supremum">df-supremum </a> which is a boolean expression # stating whether or not a number is the supremum of a set. This takes a set and gives you # the supremum if it exists. # </summary>
(= (sup S) (iota ({|} x (supremum x S))))
(= A B)(<-> (supremum A S) (supremum B S))
(-> ph (= A B))(-> ph (<-> (supremum A S) (supremum B S)))
(=_ S T)(<-> (supremum A S) (supremum A T))
(-> ph (=_ S T))(-> ph (<-> (supremum A S) (supremum A T)))
supremumeq12 # <title> Equivalence for supremum </title>
(-> (/\ (= A B) (=_ S T)) (<-> (supremum A S) (supremum B T)))
(-> ph (= A B)) , (-> ph (=_ S T))(-> ph (<-> (supremum A S) (supremum B T)))
EqReplaceImp1El0 # <title> Substitution </title> # <table> # (-> ph (e. [ A ] ] ] S)) # (= [ A ] [ B ] ) # (-> ph (e. [ [ [ B ] S)) # </table>
(-> ph (e. A S)) , (= A B)(-> ph (e. B S))
supsupremum # <title> sup is the supremum when one exists </title> # <summary> # The definition df-sup works as expected when the supremum exists. # </summary>
(-> (/\ (-. (=_ S ({/}))) (E. y (upperbound y S))) (supremum (sup S) S))
belowSup # <title> Numbers in set below the supremum </title> # <summary> # If the supremum exists, there is a number in the set that is below the supremum # </summary>
(-> (/\ (> ep (0)) (/\ (-. (=_ S ({/}))) (E. x (upperbound x S)))) (E. y (/\ (e. y S) (> y (- (sup S) ep)))))
BiReplaceBi1Al1 # <title> Substitution </title> # <table> # (<-> ph (A. x [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (<-> ph (A. x [ [ [ ch ] )) # </table>
(<-> ph (A. x ps)) , (<-> ps ch)(<-> ph (A. x ch))
BiReplaceBi1Al1Imp0 # <title> Substitution </title> # <table> # (<-> ph (A. x (-> [ ps ] ] ] th))) # (<-> [ ps ] [ ch ] ) # (<-> ph (A. x (-> [ [ [ ch ] th))) # </table>
(<-> ph (A. x (-> ps th))) , (<-> ps ch)(<-> ph (A. x (-> ch th)))
upperboundlt # <title> Upper Bound for Numbers Below a Value </title> # <summary> # A is an upper bound to the set of numbers less than or equal to A. # </summary>
(upperbound A ({|} x (<= x A)))
ImpReplaceImp1Al1 # <title> Substitution </title> # <table> # (-> ph (A. x [ ps ] ] ] )) # (-> [ ps ] [ ch ] ) # (-> ph (A. x [ [ [ ch ] )) # </table>
(-> ph (A. x ps)) , (-> ps ch)(-> ph (A. x ch))
BiReplaceImp1Al1 # <title> Substitution </title> # <table> # (-> ph (A. x [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (A. x [ [ [ ch ] )) # </table>
(-> ph (A. x ps)) , (<-> ps ch)(-> ph (A. x ch))
upperboundss # <title> Upperbound of a subset </title>
(-> (/\ (C_ S T) (upperbound A T)) (upperbound A S))
ImpReplaceBi1 # <title> Substitution </title> # <table> # (<-> ph [ ps ] ] ] ) # (-> [ ps ] [ ch ] ) # (<-> ph [ [ [ ch ] ) # </table>
(<-> ph ps) , (-> ps ch)(-> ph ch)
ImpReplaceImp1Ex1 # <title> Substitution </title> # <table> # (-> ph (E. x [ ps ] ] ] )) # (-> [ ps ] [ ch ] ) # (-> ph (E. x [ [ [ ch ] )) # </table>
(-> ph (E. x ps)) , (-> ps ch)(-> ph (E. x ch))
ImpReplaceImp1Ex1An0 # <title> Substitution </title> # <table> # (-> ph (E. x (/\ [ ps ] ] ] th))) # (-> [ ps ] [ ch ] ) # (-> ph (E. x (/\ [ [ [ ch ] th))) # </table>
(-> ph (E. x (/\ ps th))) , (-> ps ch)(-> ph (E. x (/\ ch th)))
archimedean # <title> Archimedean Property </title> # <summary> An unfinished proof of the Arichmedean property </title>
(-> (/\ (>= A (0)) (E. y (upperbound y ({|} x (/\ (e. x (N)) (<= x A)))))) (E. z (/\ (<= z A) (> z (- (sup ({|} x (/\ (e. x (N)) (<= x A)))) (1))))))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)