:: SUPINF_1 semantic presentation begin definition mode R_eal is Element of ExtREAL ; end; definition :: original: +infty redefine func +infty -> R_eal; coherence +infty is R_eal by XXREAL_0:def_1; :: original: -infty redefine func -infty -> R_eal; coherence -infty is R_eal by XXREAL_0:def_1; end; definition let X be ext-real-membered set ; func SetMajorant X -> ext-real-membered set means :Def1: :: SUPINF_1:def 1 for x being ext-real number holds ( x in it iff x is UpperBound of X ); existence ex b1 being ext-real-membered set st for x being ext-real number holds ( x in b1 iff x is UpperBound of X ) proof defpred S1[ ext-real number ] means \$1 is UpperBound of X; consider Y being ext-real-membered set such that A1: for x being ext-real number holds ( x in Y iff S1[x] ) from MEMBERED:sch_2(); take Y ; ::_thesis: for x being ext-real number holds ( x in Y iff x is UpperBound of X ) thus for x being ext-real number holds ( x in Y iff x is UpperBound of X ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being ext-real-membered set st ( for x being ext-real number holds ( x in b1 iff x is UpperBound of X ) ) & ( for x being ext-real number holds ( x in b2 iff x is UpperBound of X ) ) holds b1 = b2 proof let Y1, Y2 be ext-real-membered set ; ::_thesis: ( ( for x being ext-real number holds ( x in Y1 iff x is UpperBound of X ) ) & ( for x being ext-real number holds ( x in Y2 iff x is UpperBound of X ) ) implies Y1 = Y2 ) assume that A2: for x being ext-real number holds ( x in Y1 iff x is UpperBound of X ) and A3: for x being ext-real number holds ( x in Y2 iff x is UpperBound of X ) ; ::_thesis: Y1 = Y2 let x be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not x in Y1 or x in Y2 ) & ( not x in Y2 or x in Y1 ) ) ( x in Y1 iff x is UpperBound of X ) by A2; hence ( ( not x in Y1 or x in Y2 ) & ( not x in Y2 or x in Y1 ) ) by A3; ::_thesis: verum end; end; :: deftheorem Def1 defines SetMajorant SUPINF_1:def_1_:_ for X, b2 being ext-real-membered set holds ( b2 = SetMajorant X iff for x being ext-real number holds ( x in b2 iff x is UpperBound of X ) ); registration let X be ext-real-membered set ; cluster SetMajorant X -> non empty ext-real-membered ; coherence not SetMajorant X is empty proof set x = the UpperBound of X; the UpperBound of X in SetMajorant X by Def1; hence not SetMajorant X is empty ; ::_thesis: verum end; end; theorem :: SUPINF_1:1 for X, Y being ext-real-membered set st X c= Y holds for x being ext-real number st x in SetMajorant Y holds x in SetMajorant X proof let X, Y be ext-real-membered set ; ::_thesis: ( X c= Y implies for x being ext-real number st x in SetMajorant Y holds x in SetMajorant X ) assume A1: X c= Y ; ::_thesis: for x being ext-real number st x in SetMajorant Y holds x in SetMajorant X let x be ext-real number ; ::_thesis: ( x in SetMajorant Y implies x in SetMajorant X ) assume x in SetMajorant Y ; ::_thesis: x in SetMajorant X then x is UpperBound of Y by Def1; then x is UpperBound of X by A1, XXREAL_2:6; hence x in SetMajorant X by Def1; ::_thesis: verum end; definition let X be ext-real-membered set ; func SetMinorant X -> ext-real-membered set means :Def2: :: SUPINF_1:def 2 for x being ext-real number holds ( x in it iff x is LowerBound of X ); existence ex b1 being ext-real-membered set st for x being ext-real number holds ( x in b1 iff x is LowerBound of X ) proof defpred S1[ ext-real number ] means \$1 is LowerBound of X; consider Y being ext-real-membered set such that A1: for x being ext-real number holds ( x in Y iff S1[x] ) from MEMBERED:sch_2(); take Y ; ::_thesis: for x being ext-real number holds ( x in Y iff x is LowerBound of X ) thus for x being ext-real number holds ( x in Y iff x is LowerBound of X ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being ext-real-membered set st ( for x being ext-real number holds ( x in b1 iff x is LowerBound of X ) ) & ( for x being ext-real number holds ( x in b2 iff x is LowerBound of X ) ) holds b1 = b2 proof let Y1, Y2 be ext-real-membered set ; ::_thesis: ( ( for x being ext-real number holds ( x in Y1 iff x is LowerBound of X ) ) & ( for x being ext-real number holds ( x in Y2 iff x is LowerBound of X ) ) implies Y1 = Y2 ) assume that A2: for x being ext-real number holds ( x in Y1 iff x is LowerBound of X ) and A3: for x being ext-real number holds ( x in Y2 iff x is LowerBound of X ) ; ::_thesis: Y1 = Y2 let x be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not x in Y1 or x in Y2 ) & ( not x in Y2 or x in Y1 ) ) ( x in Y1 iff x is LowerBound of X ) by A2; hence ( ( not x in Y1 or x in Y2 ) & ( not x in Y2 or x in Y1 ) ) by A3; ::_thesis: verum end; end; :: deftheorem Def2 defines SetMinorant SUPINF_1:def_2_:_ for X, b2 being ext-real-membered set holds ( b2 = SetMinorant X iff for x being ext-real number holds ( x in b2 iff x is LowerBound of X ) ); registration let X be ext-real-membered set ; cluster SetMinorant X -> non empty ext-real-membered ; coherence not SetMinorant X is empty proof set x = the LowerBound of X; the LowerBound of X in SetMinorant X by Def2; hence not SetMinorant X is empty ; ::_thesis: verum end; end; theorem :: SUPINF_1:2 for X, Y being ext-real-membered set st X c= Y holds for x being ext-real number st x in SetMinorant Y holds x in SetMinorant X proof let X, Y be ext-real-membered set ; ::_thesis: ( X c= Y implies for x being ext-real number st x in SetMinorant Y holds x in SetMinorant X ) assume A1: X c= Y ; ::_thesis: for x being ext-real number st x in SetMinorant Y holds x in SetMinorant X let x be ext-real number ; ::_thesis: ( x in SetMinorant Y implies x in SetMinorant X ) assume x in SetMinorant Y ; ::_thesis: x in SetMinorant X then x is LowerBound of Y by Def2; then x is LowerBound of X by A1, XXREAL_2:5; hence x in SetMinorant X by Def2; ::_thesis: verum end; theorem :: SUPINF_1:3 for X being non empty ext-real-membered set holds ( sup X = inf (SetMajorant X) & inf X = sup (SetMinorant X) ) proof let X be non empty ext-real-membered set ; ::_thesis: ( sup X = inf (SetMajorant X) & inf X = sup (SetMinorant X) ) for y being ext-real number st y in SetMajorant X holds sup X <= y proof let y be ext-real number ; ::_thesis: ( y in SetMajorant X implies sup X <= y ) assume y in SetMajorant X ; ::_thesis: sup X <= y then y is UpperBound of X by Def1; hence sup X <= y by XXREAL_2:def_3; ::_thesis: verum end; then A1: sup X is LowerBound of SetMajorant X by XXREAL_2:def_2; inf X is LowerBound of X by XXREAL_2:def_4; then A2: inf X in SetMinorant X by Def2; for y being ext-real number st y in SetMinorant X holds y <= inf X proof let y be ext-real number ; ::_thesis: ( y in SetMinorant X implies y <= inf X ) assume y in SetMinorant X ; ::_thesis: y <= inf X then y is LowerBound of X by Def2; hence y <= inf X by XXREAL_2:def_4; ::_thesis: verum end; then A3: inf X is UpperBound of SetMinorant X by XXREAL_2:def_1; sup X is UpperBound of X by XXREAL_2:def_3; then sup X in SetMajorant X by Def1; hence ( sup X = inf (SetMajorant X) & inf X = sup (SetMinorant X) ) by A1, A2, A3, XXREAL_2:55, XXREAL_2:56; ::_thesis: verum end; registration let X be non empty set ; cluster non empty with_non-empty_elements for Element of K6(K6(X)); existence ex b1 being Subset-Family of X st ( not b1 is empty & b1 is with_non-empty_elements ) proof take {([#] X)} ; ::_thesis: ( not {([#] X)} is empty & {([#] X)} is with_non-empty_elements ) thus not {([#] X)} is empty ; ::_thesis: {([#] X)} is with_non-empty_elements assume {} in {([#] X)} ; :: according to SETFAM_1:def_8 ::_thesis: contradiction hence contradiction by TARSKI:def_1; ::_thesis: verum end; end; definition let X be non empty set ; mode bool_DOMAIN of X is non empty with_non-empty_elements Subset-Family of X; end; definition let F be bool_DOMAIN of ExtREAL; func SUP F -> ext-real-membered set means :Def3: :: SUPINF_1:def 3 for a being ext-real number holds ( a in it iff ex A being non empty ext-real-membered set st ( A in F & a = sup A ) ); existence ex b1 being ext-real-membered set st for a being ext-real number holds ( a in b1 iff ex A being non empty ext-real-membered set st ( A in F & a = sup A ) ) proof defpred S1[ ext-real number ] means ex A being non empty ext-real-membered set st ( A in F & \$1 = sup A ); consider S being ext-real-membered set such that A1: for a being ext-real number holds ( a in S iff S1[a] ) from MEMBERED:sch_2(); reconsider S = S as ext-real-membered set ; take S ; ::_thesis: for a being ext-real number holds ( a in S iff ex A being non empty ext-real-membered set st ( A in F & a = sup A ) ) thus for a being ext-real number holds ( a in S iff ex A being non empty ext-real-membered set st ( A in F & a = sup A ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being ext-real-membered set st ( for a being ext-real number holds ( a in b1 iff ex A being non empty ext-real-membered set st ( A in F & a = sup A ) ) ) & ( for a being ext-real number holds ( a in b2 iff ex A being non empty ext-real-membered set st ( A in F & a = sup A ) ) ) holds b1 = b2 proof let S1, S2 be ext-real-membered set ; ::_thesis: ( ( for a being ext-real number holds ( a in S1 iff ex A being non empty ext-real-membered set st ( A in F & a = sup A ) ) ) & ( for a being ext-real number holds ( a in S2 iff ex A being non empty ext-real-membered set st ( A in F & a = sup A ) ) ) implies S1 = S2 ) assume that A2: for a being ext-real number holds ( a in S1 iff ex A being non empty ext-real-membered set st ( A in F & a = sup A ) ) and A3: for a being ext-real number holds ( a in S2 iff ex A being non empty ext-real-membered set st ( A in F & a = sup A ) ) ; ::_thesis: S1 = S2 let a be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not a in S1 or a in S2 ) & ( not a in S2 or a in S1 ) ) hereby ::_thesis: ( not a in S2 or a in S1 ) assume a in S1 ; ::_thesis: a in S2 then ex A being non empty ext-real-membered set st ( A in F & a = sup A ) by A2; hence a in S2 by A3; ::_thesis: verum end; assume a in S2 ; ::_thesis: a in S1 then ex A being non empty ext-real-membered set st ( A in F & a = sup A ) by A3; hence a in S1 by A2; ::_thesis: verum end; end; :: deftheorem Def3 defines SUP SUPINF_1:def_3_:_ for F being bool_DOMAIN of ExtREAL for b2 being ext-real-membered set holds ( b2 = SUP F iff for a being ext-real number holds ( a in b2 iff ex A being non empty ext-real-membered set st ( A in F & a = sup A ) ) ); registration let F be bool_DOMAIN of ExtREAL; cluster SUP F -> non empty ext-real-membered ; coherence not SUP F is empty proof set A = the Element of F; reconsider A = the Element of F as non empty ext-real-membered set by SETFAM_1:def_8; sup A = sup A ; hence not SUP F is empty by Def3; ::_thesis: verum end; end; theorem Th4: :: SUPINF_1:4 for F being bool_DOMAIN of ExtREAL for S being non empty ext-real-membered number st S = union F holds sup S is UpperBound of SUP F proof let F be bool_DOMAIN of ExtREAL; ::_thesis: for S being non empty ext-real-membered number st S = union F holds sup S is UpperBound of SUP F let S be non empty ext-real-membered set ; ::_thesis: ( S = union F implies sup S is UpperBound of SUP F ) assume A1: S = union F ; ::_thesis: sup S is UpperBound of SUP F for x being ext-real number st x in SUP F holds x <= sup S proof let x be ext-real number ; ::_thesis: ( x in SUP F implies x <= sup S ) assume x in SUP F ; ::_thesis: x <= sup S then consider A being non empty ext-real-membered set such that A2: A in F and A3: x = sup A by Def3; A c= S proof let a be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not a in A or a in S ) assume a in A ; ::_thesis: a in S hence a in S by A1, A2, TARSKI:def_4; ::_thesis: verum end; hence x <= sup S by A3, XXREAL_2:59; ::_thesis: verum end; hence sup S is UpperBound of SUP F by XXREAL_2:def_1; ::_thesis: verum end; theorem Th5: :: SUPINF_1:5 for F being bool_DOMAIN of ExtREAL for S being ext-real-membered set st S = union F holds sup (SUP F) is UpperBound of S proof let F be bool_DOMAIN of ExtREAL; ::_thesis: for S being ext-real-membered set st S = union F holds sup (SUP F) is UpperBound of S let S be ext-real-membered set ; ::_thesis: ( S = union F implies sup (SUP F) is UpperBound of S ) assume A1: S = union F ; ::_thesis: sup (SUP F) is UpperBound of S for x being ext-real number st x in S holds x <= sup (SUP F) proof let x be ext-real number ; ::_thesis: ( x in S implies x <= sup (SUP F) ) assume x in S ; ::_thesis: x <= sup (SUP F) then consider Z being set such that A2: x in Z and A3: Z in F by A1, TARSKI:def_4; reconsider Z = Z as non empty ext-real-membered set by A2, A3; consider a being set such that A4: a = sup Z ; reconsider a = a as ext-real number by A4; ( sup Z is UpperBound of Z & a in SUP F ) by A3, A4, Def3, XXREAL_2:def_3; hence x <= sup (SUP F) by A2, A4, XXREAL_2:61, XXREAL_2:def_1; ::_thesis: verum end; hence sup (SUP F) is UpperBound of S by XXREAL_2:def_1; ::_thesis: verum end; theorem :: SUPINF_1:6 for F being bool_DOMAIN of ExtREAL for S being non empty ext-real-membered set st S = union F holds sup S = sup (SUP F) proof let F be bool_DOMAIN of ExtREAL; ::_thesis: for S being non empty ext-real-membered set st S = union F holds sup S = sup (SUP F) let S be non empty ext-real-membered set ; ::_thesis: ( S = union F implies sup S = sup (SUP F) ) set a = sup S; set b = sup (SUP F); assume A1: S = union F ; ::_thesis: sup S = sup (SUP F) then sup S is UpperBound of SUP F by Th4; then A2: sup (SUP F) <= sup S by XXREAL_2:def_3; sup (SUP F) is UpperBound of S by A1, Th5; then sup S <= sup (SUP F) by XXREAL_2:def_3; hence sup S = sup (SUP F) by A2, XXREAL_0:1; ::_thesis: verum end; definition let F be bool_DOMAIN of ExtREAL; func INF F -> ext-real-membered set means :Def4: :: SUPINF_1:def 4 for a being ext-real number holds ( a in it iff ex A being non empty ext-real-membered set st ( A in F & a = inf A ) ); existence ex b1 being ext-real-membered set st for a being ext-real number holds ( a in b1 iff ex A being non empty ext-real-membered set st ( A in F & a = inf A ) ) proof set A = the Element of F; defpred S1[ ext-real number ] means ex A being non empty ext-real-membered set st ( A in F & \$1 = inf A ); reconsider A = the Element of F as non empty ext-real-membered set by SETFAM_1:def_8; consider S being ext-real-membered set such that A1: for a being ext-real number holds ( a in S iff S1[a] ) from MEMBERED:sch_2(); inf A = inf A ; then reconsider S = S as non empty ext-real-membered set by A1; take S ; ::_thesis: for a being ext-real number holds ( a in S iff ex A being non empty ext-real-membered set st ( A in F & a = inf A ) ) thus for a being ext-real number holds ( a in S iff ex A being non empty ext-real-membered set st ( A in F & a = inf A ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being ext-real-membered set st ( for a being ext-real number holds ( a in b1 iff ex A being non empty ext-real-membered set st ( A in F & a = inf A ) ) ) & ( for a being ext-real number holds ( a in b2 iff ex A being non empty ext-real-membered set st ( A in F & a = inf A ) ) ) holds b1 = b2 proof let S1, S2 be ext-real-membered set ; ::_thesis: ( ( for a being ext-real number holds ( a in S1 iff ex A being non empty ext-real-membered set st ( A in F & a = inf A ) ) ) & ( for a being ext-real number holds ( a in S2 iff ex A being non empty ext-real-membered set st ( A in F & a = inf A ) ) ) implies S1 = S2 ) assume that A2: for a being ext-real number holds ( a in S1 iff ex A being non empty ext-real-membered set st ( A in F & a = inf A ) ) and A3: for a being ext-real number holds ( a in S2 iff ex A being non empty ext-real-membered set st ( A in F & a = inf A ) ) ; ::_thesis: S1 = S2 for a being set holds ( a in S1 iff a in S2 ) proof let a be set ; ::_thesis: ( a in S1 iff a in S2 ) hereby ::_thesis: ( a in S2 implies a in S1 ) assume A4: a in S1 ; ::_thesis: a in S2 then reconsider a9 = a as ext-real number ; ex A being non empty ext-real-membered set st ( A in F & a9 = inf A ) by A2, A4; hence a in S2 by A3; ::_thesis: verum end; assume A5: a in S2 ; ::_thesis: a in S1 then reconsider a = a as ext-real number ; ex A being non empty ext-real-membered set st ( A in F & a = inf A ) by A3, A5; hence a in S1 by A2; ::_thesis: verum end; hence S1 = S2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def4 defines INF SUPINF_1:def_4_:_ for F being bool_DOMAIN of ExtREAL for b2 being ext-real-membered set holds ( b2 = INF F iff for a being ext-real number holds ( a in b2 iff ex A being non empty ext-real-membered set st ( A in F & a = inf A ) ) ); registration let F be bool_DOMAIN of ExtREAL; cluster INF F -> non empty ext-real-membered ; coherence not INF F is empty proof set A = the Element of F; reconsider A = the Element of F as non empty ext-real-membered set by SETFAM_1:def_8; inf A = inf A ; hence not INF F is empty by Def4; ::_thesis: verum end; end; theorem Th7: :: SUPINF_1:7 for F being bool_DOMAIN of ExtREAL for S being non empty ext-real-membered set st S = union F holds inf S is LowerBound of INF F proof let F be bool_DOMAIN of ExtREAL; ::_thesis: for S being non empty ext-real-membered set st S = union F holds inf S is LowerBound of INF F let S be non empty ext-real-membered set ; ::_thesis: ( S = union F implies inf S is LowerBound of INF F ) assume A1: S = union F ; ::_thesis: inf S is LowerBound of INF F for x being ext-real number st x in INF F holds inf S <= x proof let x be ext-real number ; ::_thesis: ( x in INF F implies inf S <= x ) assume x in INF F ; ::_thesis: inf S <= x then consider A being non empty ext-real-membered set such that A2: A in F and A3: x = inf A by Def4; A c= S proof let a be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not a in A or a in S ) assume a in A ; ::_thesis: a in S hence a in S by A1, A2, TARSKI:def_4; ::_thesis: verum end; hence inf S <= x by A3, XXREAL_2:60; ::_thesis: verum end; hence inf S is LowerBound of INF F by XXREAL_2:def_2; ::_thesis: verum end; theorem Th8: :: SUPINF_1:8 for F being bool_DOMAIN of ExtREAL for S being ext-real-membered set st S = union F holds inf (INF F) is LowerBound of S proof let F be bool_DOMAIN of ExtREAL; ::_thesis: for S being ext-real-membered set st S = union F holds inf (INF F) is LowerBound of S let S be ext-real-membered set ; ::_thesis: ( S = union F implies inf (INF F) is LowerBound of S ) assume A1: S = union F ; ::_thesis: inf (INF F) is LowerBound of S for x being ext-real number st x in S holds inf (INF F) <= x proof let x be ext-real number ; ::_thesis: ( x in S implies inf (INF F) <= x ) assume x in S ; ::_thesis: inf (INF F) <= x then consider Z being set such that A2: x in Z and A3: Z in F by A1, TARSKI:def_4; reconsider Z = Z as non empty ext-real-membered set by A2, A3; consider a being set such that A4: a = inf Z ; reconsider a = a as ext-real number by A4; ( inf Z is LowerBound of Z & a in INF F ) by A3, A4, Def4, XXREAL_2:def_4; hence inf (INF F) <= x by A2, A4, XXREAL_2:62, XXREAL_2:def_2; ::_thesis: verum end; hence inf (INF F) is LowerBound of S by XXREAL_2:def_2; ::_thesis: verum end; theorem :: SUPINF_1:9 for F being bool_DOMAIN of ExtREAL for S being non empty ext-real-membered set st S = union F holds inf S = inf (INF F) proof let F be bool_DOMAIN of ExtREAL; ::_thesis: for S being non empty ext-real-membered set st S = union F holds inf S = inf (INF F) let S be non empty ext-real-membered set ; ::_thesis: ( S = union F implies inf S = inf (INF F) ) set a = inf S; set b = inf (INF F); assume A1: S = union F ; ::_thesis: inf S = inf (INF F) then inf S is LowerBound of INF F by Th7; then A2: inf S <= inf (INF F) by XXREAL_2:def_4; inf (INF F) is LowerBound of S by A1, Th8; then inf (INF F) <= inf S by XXREAL_2:def_4; hence inf S = inf (INF F) by A2, XXREAL_0:1; ::_thesis: verum end;