supinf_1.miz



    begin

    definition

      mode R_eal is Element of ExtREAL ;

    end

    definition

      :: original: +infty

      redefine

      func +infty -> R_eal ;

      coherence by XXREAL_0:def 1;

      :: original: -infty

      redefine

      func -infty -> R_eal ;

      coherence by XXREAL_0:def 1;

    end

    definition

      let X be ext-real-membered set;

      :: SUPINF_1:def1

      func SetMajorant (X) -> ext-real-membered set means

      : Def1: for x be ExtReal holds x in it iff x is UpperBound of X;

      existence

      proof

        defpred P[ ExtReal] means $1 is UpperBound of X;

        consider Y be ext-real-membered set such that

         A1: for x be ExtReal holds x in Y iff P[x] from MEMBERED:sch 2;

        take Y;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let Y1,Y2 be ext-real-membered set such that

         A2: for x be ExtReal holds x in Y1 iff x is UpperBound of X and

         A3: for x be ExtReal holds x in Y2 iff x is UpperBound of X;

        let x be ExtReal;

        x in Y1 iff x is UpperBound of X by A2;

        hence thesis by A3;

      end;

    end

    registration

      let X be ext-real-membered set;

      cluster ( SetMajorant X) -> non empty;

      coherence

      proof

        set x = the UpperBound of X;

        x in ( SetMajorant X) by Def1;

        hence thesis;

      end;

    end

    theorem :: SUPINF_1:1

    for X,Y be ext-real-membered set st X c= Y holds for x be ExtReal holds x in ( SetMajorant Y) implies x in ( SetMajorant X)

    proof

      let X,Y be ext-real-membered set;

      assume

       A1: X c= Y;

      let x be ExtReal;

      assume x in ( SetMajorant Y);

      then x is UpperBound of Y by Def1;

      then x is UpperBound of X by A1, XXREAL_2: 6;

      hence thesis by Def1;

    end;

    definition

      let X be ext-real-membered set;

      :: SUPINF_1:def2

      func SetMinorant (X) -> ext-real-membered set means

      : Def2: for x be ExtReal holds x in it iff x is LowerBound of X;

      existence

      proof

        defpred P[ ExtReal] means $1 is LowerBound of X;

        consider Y be ext-real-membered set such that

         A1: for x be ExtReal holds x in Y iff P[x] from MEMBERED:sch 2;

        take Y;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let Y1,Y2 be ext-real-membered set such that

         A2: for x be ExtReal holds x in Y1 iff x is LowerBound of X and

         A3: for x be ExtReal holds x in Y2 iff x is LowerBound of X;

        let x be ExtReal;

        x in Y1 iff x is LowerBound of X by A2;

        hence thesis by A3;

      end;

    end

    registration

      let X be ext-real-membered set;

      cluster ( SetMinorant X) -> non empty;

      coherence

      proof

        set x = the LowerBound of X;

        x in ( SetMinorant X) by Def2;

        hence thesis;

      end;

    end

    theorem :: SUPINF_1:2

    for X,Y be ext-real-membered set st X c= Y holds for x be ExtReal holds x in ( SetMinorant Y) implies x in ( SetMinorant X)

    proof

      let X,Y be ext-real-membered set;

      assume

       A1: X c= Y;

      let x be ExtReal;

      assume x in ( SetMinorant Y);

      then x is LowerBound of Y by Def2;

      then x is LowerBound of X by A1, XXREAL_2: 5;

      hence thesis by Def2;

    end;

    theorem :: SUPINF_1:3

    for X be 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;

      for y be ExtReal st y in ( SetMajorant X) holds ( sup X) <= y

      proof

        let y be ExtReal;

        assume y in ( SetMajorant X);

        then y is UpperBound of X by Def1;

        hence thesis by XXREAL_2:def 3;

      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 be ExtReal st y in ( SetMinorant X) holds y <= ( inf X)

      proof

        let y be ExtReal;

        assume y in ( SetMinorant X);

        then y is LowerBound of X by Def2;

        hence thesis by XXREAL_2:def 4;

      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 thesis by A1, A2, A3, XXREAL_2: 55, XXREAL_2: 56;

    end;

    registration

      let X be non empty set;

      cluster non empty with_non-empty_elements for Subset-Family of X;

      existence

      proof

        take {( [#] X)};

        thus {( [#] X)} is non empty;

        assume {} in {( [#] X)};

        hence contradiction by TARSKI:def 1;

      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 ;

      :: SUPINF_1:def3

      func SUP (F) -> ext-real-membered set means

      : Def3: for a be ExtReal holds a in it iff ex A be non empty ext-real-membered set st A in F & a = ( sup A);

      existence

      proof

        defpred P[ ExtReal] means ex A be non empty ext-real-membered set st A in F & $1 = ( sup A);

        consider S be ext-real-membered set such that

         A1: for a be ExtReal holds a in S iff P[a] from MEMBERED:sch 2;

        reconsider S as ext-real-membered set;

        take S;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let S1,S2 be ext-real-membered set such that

         A2: for a be ExtReal holds a in S1 iff ex A be non empty ext-real-membered set st A in F & a = ( sup A) and

         A3: for a be ExtReal holds a in S2 iff ex A be non empty ext-real-membered set st A in F & a = ( sup A);

        let a be ExtReal;

        hereby

          assume a in S1;

          then ex A be non empty ext-real-membered set st A in F & a = ( sup A) by A2;

          hence a in S2 by A3;

        end;

        assume a in S2;

        then ex A be non empty ext-real-membered set st A in F & a = ( sup A) by A3;

        hence thesis by A2;

      end;

    end

    registration

      let F be bool_DOMAIN of ExtREAL ;

      cluster ( SUP F) -> non empty;

      coherence

      proof

        set A = the Element of F;

        reconsider A as non empty ext-real-membered set by SETFAM_1:def 8;

        ( sup A) = ( sup A);

        hence thesis by Def3;

      end;

    end

    theorem :: SUPINF_1:4

    

     Th4: for F be bool_DOMAIN of ExtREAL , S be 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 , S be non empty ext-real-membered set;

      assume

       A1: S = ( union F);

      for x be ExtReal st x in ( SUP F) holds x <= ( sup S)

      proof

        let x be ExtReal;

        assume x in ( SUP F);

        then

        consider A be non empty ext-real-membered set such that

         A2: A in F and

         A3: x = ( sup A) by Def3;

        A c= S by A1, A2, TARSKI:def 4;

        hence thesis by A3, XXREAL_2: 59;

      end;

      hence thesis by XXREAL_2:def 1;

    end;

    theorem :: SUPINF_1:5

    

     Th5: for F be bool_DOMAIN of ExtREAL , S be ext-real-membered set st S = ( union F) holds ( sup ( SUP F)) is UpperBound of S

    proof

      let F be bool_DOMAIN of ExtREAL , S be ext-real-membered set;

      assume

       A1: S = ( union F);

      for x be ExtReal st x in S holds x <= ( sup ( SUP F))

      proof

        let x be ExtReal;

        assume x in S;

        then

        consider Z be set such that

         A2: x in Z and

         A3: Z in F by A1, TARSKI:def 4;

        reconsider Z as non empty ext-real-membered set by A2, A3;

        set a = ( sup Z);

        ( sup Z) is UpperBound of Z & a in ( SUP F) by A3, Def3, XXREAL_2:def 3;

        hence thesis by A2, XXREAL_2: 61, XXREAL_2:def 1;

      end;

      hence thesis by XXREAL_2:def 1;

    end;

    theorem :: SUPINF_1:6

    for F be bool_DOMAIN of ExtREAL , S be non empty ext-real-membered set st S = ( union F) holds ( sup S) = ( sup ( SUP F))

    proof

      let F be bool_DOMAIN of ExtREAL , S be non empty ext-real-membered set;

      set a = ( sup S);

      set b = ( sup ( SUP F));

      assume

       A1: S = ( union F);

      then ( sup S) is UpperBound of ( SUP F) by Th4;

      then

       A2: b <= a by XXREAL_2:def 3;

      ( sup ( SUP F)) is UpperBound of S by A1, Th5;

      then a <= b by XXREAL_2:def 3;

      hence thesis by A2, XXREAL_0: 1;

    end;

    definition

      let F be bool_DOMAIN of ExtREAL ;

      :: SUPINF_1:def4

      func INF F -> ext-real-membered set means

      : Def4: for a be ExtReal holds a in it iff ex A be non empty ext-real-membered set st A in F & a = ( inf A);

      existence

      proof

        set A = the Element of F;

        defpred P[ ExtReal] means ex A be non empty ext-real-membered set st A in F & $1 = ( inf A);

        reconsider A as non empty ext-real-membered set by SETFAM_1:def 8;

        consider S be ext-real-membered set such that

         A1: for a be ExtReal holds a in S iff P[a] from MEMBERED:sch 2;

        ( inf A) = ( inf A);

        then

        reconsider S as non empty ext-real-membered set by A1;

        take S;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let S1,S2 be ext-real-membered set such that

         A2: for a be ExtReal holds a in S1 iff ex A be non empty ext-real-membered set st A in F & a = ( inf A) and

         A3: for a be ExtReal holds a in S2 iff ex A be non empty ext-real-membered set st A in F & a = ( inf A);

        for a be object holds a in S1 iff a in S2

        proof

          let a be object;

          hereby

            assume

             A4: a in S1;

            then

            reconsider a9 = a as ExtReal;

            ex A be non empty ext-real-membered set st A in F & a9 = ( inf A) by A2, A4;

            hence a in S2 by A3;

          end;

          assume

           A5: a in S2;

          then

          reconsider a as ExtReal;

          ex A be non empty ext-real-membered set st A in F & a = ( inf A) by A3, A5;

          hence thesis by A2;

        end;

        hence thesis;

      end;

    end

    registration

      let F be bool_DOMAIN of ExtREAL ;

      cluster ( INF F) -> non empty;

      coherence

      proof

        set A = the Element of F;

        reconsider A as non empty ext-real-membered set by SETFAM_1:def 8;

        ( inf A) = ( inf A);

        hence thesis by Def4;

      end;

    end

    theorem :: SUPINF_1:7

    

     Th7: for F be bool_DOMAIN of ExtREAL , S be 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 , S be non empty ext-real-membered set;

      assume

       A1: S = ( union F);

      for x be ExtReal st x in ( INF F) holds ( inf S) <= x

      proof

        let x be ExtReal;

        assume x in ( INF F);

        then

        consider A be non empty ext-real-membered set such that

         A2: A in F and

         A3: x = ( inf A) by Def4;

        A c= S by A1, A2, TARSKI:def 4;

        hence thesis by A3, XXREAL_2: 60;

      end;

      hence thesis by XXREAL_2:def 2;

    end;

    theorem :: SUPINF_1:8

    

     Th8: for F be bool_DOMAIN of ExtREAL , S be ext-real-membered set st S = ( union F) holds ( inf ( INF F)) is LowerBound of S

    proof

      let F be bool_DOMAIN of ExtREAL , S be ext-real-membered set;

      assume

       A1: S = ( union F);

      for x be ExtReal st x in S holds ( inf ( INF F)) <= x

      proof

        let x be ExtReal;

        assume x in S;

        then

        consider Z be set such that

         A2: x in Z and

         A3: Z in F by A1, TARSKI:def 4;

        reconsider Z as non empty ext-real-membered set by A2, A3;

        set a = ( inf Z);

        ( inf Z) is LowerBound of Z & a in ( INF F) by A3, Def4, XXREAL_2:def 4;

        hence thesis by A2, XXREAL_2: 62, XXREAL_2:def 2;

      end;

      hence thesis by XXREAL_2:def 2;

    end;

    theorem :: SUPINF_1:9

    for F be bool_DOMAIN of ExtREAL , S be non empty ext-real-membered set st S = ( union F) holds ( inf S) = ( inf ( INF F))

    proof

      let F be bool_DOMAIN of ExtREAL , S be non empty ext-real-membered set;

      set a = ( inf S);

      set b = ( inf ( INF F));

      assume

       A1: S = ( union F);

      then ( inf S) is LowerBound of ( INF F) by Th7;

      then

       A2: a <= b by XXREAL_2:def 4;

      ( inf ( INF F)) is LowerBound of S by A1, Th8;

      then b <= a by XXREAL_2:def 4;

      hence thesis by A2, XXREAL_0: 1;

    end;