measure5.miz



    begin

    reserve a,b for R_eal;

    scheme :: MEASURE5:sch1

    RSetEq { P[ set] } :

for X1,X2 be Subset of REAL st (for x be R_eal holds x in X1 iff P[x]) & (for x be R_eal holds x in X2 iff P[x]) holds X1 = X2;

      let A1,A2 be Subset of REAL such that

       A1: for x be R_eal holds x in A1 iff P[x] and

       A2: for x be R_eal holds x in A2 iff P[x];

      thus A1 c= A2

      proof

        let x be Real;

        assume

         A3: x in A1;

        then x in REAL ;

        then

        reconsider x as R_eal by NUMBERS: 31;

        P[x] by A1, A3;

        hence thesis by A2;

      end;

      let x be Real;

      assume

       A4: x in A2;

      then x in REAL ;

      then

      reconsider x as R_eal by NUMBERS: 31;

      P[x] by A2, A4;

      hence thesis by A1;

    end;

    definition

      let a,b be R_eal;

      :: original: ].

      redefine

      :: MEASURE5:def1

      func ].a,b.[ -> Subset of REAL means for x be R_eal holds x in it iff a < x & x < b;

      coherence

      proof

        for x be set st x in ].a, b.[ holds x in REAL ;

        hence thesis;

      end;

      compatibility

      proof

        let X be Subset of REAL ;

        thus X = ].a, b.[ implies for x be R_eal holds x in X iff a < x & x < b by XXREAL_1: 4;

        assume

         A1: for x be R_eal holds x in X iff a < x & x < b;

        thus X c= ].a, b.[

        proof

          let x be Real;

          assume

           A2: x in X;

          then x in REAL ;

          then

          reconsider t = x as R_eal by NUMBERS: 31;

          a < t & t < b by A1, A2;

          hence thesis;

        end;

        let x be Real;

        reconsider t = x as R_eal by XXREAL_0:def 1;

        assume x in ].a, b.[;

        then a < t & t < b by XXREAL_1: 4;

        hence thesis by A1;

      end;

    end

    definition

      let IT be Subset of REAL ;

      :: MEASURE5:def2

      attr IT is open_interval means ex a,b be R_eal st IT = ].a, b.[;

      :: MEASURE5:def3

      attr IT is closed_interval means ex a,b be Real st IT = [.a, b.];

    end

    registration

      cluster non empty open_interval for Subset of REAL ;

      existence

      proof

        take ]. -infty , +infty .[;

        ( In ( 0 , REAL )) in ]. -infty , +infty .[ by XXREAL_1: 224;

        hence ]. -infty , +infty .[ is non empty;

        take -infty , +infty ;

        thus thesis;

      end;

      cluster non empty closed_interval for Subset of REAL ;

      existence

      proof

        take [. 0 , 1.];

        thus [. 0 , 1.] is non empty by XXREAL_1: 30;

        take 0 , 1;

        thus thesis;

      end;

    end

    definition

      let IT be Subset of REAL ;

      :: MEASURE5:def4

      attr IT is right_open_interval means ex a be Real, b be R_eal st IT = [.a, b.[;

    end

    notation

      let IT be Subset of REAL ;

      synonym IT is left_closed_interval for IT is right_open_interval;

    end

    definition

      let IT be Subset of REAL ;

      :: MEASURE5:def5

      attr IT is left_open_interval means ex a be R_eal, b be Real st IT = ].a, b.];

    end

    notation

      let IT be Subset of REAL ;

      synonym IT is right_closed_interval for IT is left_open_interval;

    end

    registration

      cluster non empty right_open_interval for Subset of REAL ;

      existence

      proof

        take [. 0 , +infty .[;

         0 in [. 0 , +infty .[ by XXREAL_1: 236;

        hence [. 0 , +infty .[ is non empty;

        take 0 , +infty ;

        thus thesis;

      end;

      cluster non empty left_open_interval for Subset of REAL ;

      existence

      proof

        take ]. -infty , 1.];

        1 in ]. -infty , 1.] by XXREAL_1: 234;

        hence ]. -infty , 1.] is non empty;

        take -infty , 1;

        thus thesis;

      end;

    end

    definition

      mode Interval is interval Subset of REAL ;

    end

    reserve A,B for Interval;

    registration

      cluster open_interval -> interval for Subset of REAL ;

      coherence ;

      cluster closed_interval -> interval for Subset of REAL ;

      coherence ;

      cluster right_open_interval -> interval for Subset of REAL ;

      coherence ;

      cluster left_open_interval -> interval for Subset of REAL ;

      coherence ;

    end

    theorem :: MEASURE5:1

    for I be interval Subset of REAL holds I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval

    proof

      let I be interval Subset of REAL ;

      per cases ;

        suppose

         A1: I is left_end right_end;

        reconsider a = ( inf I), b = ( sup I) as R_eal;

        

         A2: a in I & I = [.a, b.] by A1, XXREAL_2: 75, XXREAL_2:def 5;

        thus thesis by A1, A2;

      end;

        suppose

         A3: I is non left_end right_end;

        set a = ( inf I), b = ( sup I);

        

         A4: I = ].a, b.] by A3, XXREAL_2: 76;

        

         A5: b in I by A3, XXREAL_2:def 6;

        thus thesis by A5, A4;

      end;

        suppose

         A6: I is left_end non right_end;

        set a = ( inf I), b = ( sup I);

        

         A7: I = [.a, b.[ by A6, XXREAL_2: 77;

        

         A8: a in I by A6, XXREAL_2:def 5;

        thus thesis by A8, A7;

      end;

        suppose I is non left_end non right_end;

        then

        consider a,b be ExtReal such that

         A9: a <= b and

         A10: I = ].a, b.[ by XXREAL_2: 79;

        reconsider a, b as R_eal by XXREAL_0:def 1;

        a <= b by A9;

        hence thesis by A10;

      end;

    end;

    theorem :: MEASURE5:2

    

     Th2: for a,b be R_eal st a < b holds ex x be R_eal st a < x & x < b & x in REAL

    proof

      let a,b be R_eal;

      

       A1: a in REAL or a in { -infty , +infty } by XBOOLE_0:def 3, XXREAL_0:def 4;

      

       A2: b in REAL or b in { -infty , +infty } by XBOOLE_0:def 3, XXREAL_0:def 4;

      assume

       A3: a < b;

      then

       A4: ( not a = +infty ) & not b = -infty by XXREAL_0: 4, XXREAL_0: 6;

      per cases by A1, A2, A4, TARSKI:def 2;

        suppose a in REAL & b in REAL ;

        then

        consider x,y be Real such that

         A5: x = a & y = b and x <= y by A3;

        consider z be Real such that

         A6: x < z & z < y by A3, A5, XREAL_1: 5;

        reconsider z as Element of REAL by XREAL_0:def 1;

        reconsider o = z as R_eal by XXREAL_0:def 1;

        take o;

        thus thesis by A5, A6;

      end;

        suppose

         A7: a in REAL & b = +infty ;

        then

        reconsider x = a as Real;

        consider z be Real such that

         A8: x < z by XREAL_1: 1;

        reconsider z as Element of REAL by XREAL_0:def 1;

        reconsider o = z as R_eal by XXREAL_0:def 1;

        take o;

        thus thesis by A7, A8, XXREAL_0: 9;

      end;

        suppose

         A9: a = -infty & b in REAL ;

        then

        reconsider y = b as Real;

        consider z be Real such that

         A10: z < y by XREAL_1: 2;

        reconsider z as Element of REAL by XREAL_0:def 1;

        reconsider o = z as R_eal by XXREAL_0:def 1;

        take o;

        thus thesis by A9, A10, XXREAL_0: 12;

      end;

        suppose

         A11: a = -infty & b = +infty ;

        take 0. ;

         0. = ( In ( 0 , REAL ));

        hence thesis by A11;

      end;

    end;

    theorem :: MEASURE5:3

    for a,b,c be R_eal st a < b & a < c holds ex x be R_eal st a < x & x < b & x < c & x in REAL

    proof

      let a,b,c be R_eal;

      

       A1: ( min (b,c)) = ( min {b, c}) by XXREAL_2: 14;

      ex o be R_eal st o in {b, c} & o <= c

      proof

        take c;

        thus thesis by TARSKI:def 2;

      end;

      then

       A2: ( min (b,c)) <= c by A1, XXREAL_2: 62;

      reconsider m = ( min (b,c)) as R_eal by XXREAL_0:def 1;

      assume a < b & a < c;

      then a < ( min (b,c)) by XXREAL_0:def 9;

      then

      consider x be R_eal such that

       A3: a < x & x < m & x in REAL by Th2;

      take x;

      ex o be R_eal st o in {b, c} & o <= b

      proof

        take b;

        thus thesis by TARSKI:def 2;

      end;

      then ( min (b,c)) <= b by A1, XXREAL_2: 62;

      hence thesis by A3, A2, XXREAL_0: 2;

    end;

    theorem :: MEASURE5:4

    for a,b,c be R_eal st a < c & b < c holds ex x be R_eal st a < x & b < x & x < c & x in REAL

    proof

      let a,b,c be R_eal;

      reconsider m = ( max (a,b)) as R_eal by XXREAL_0:def 1;

      

       A1: b in {a, b} by TARSKI:def 2;

      assume a < c & b < c;

      then ( max (a,b)) < c by XXREAL_0:def 10;

      then

      consider x be R_eal such that

       A2: m < x & x < c & x in REAL by Th2;

      take x;

      ( max (a,b)) = ( max {a, b}) & a in {a, b} by TARSKI:def 2, XXREAL_2: 12;

      hence thesis by A2, A1, XXREAL_2: 61;

    end;

    definition

      let A be ext-real-membered set;

      :: MEASURE5:def6

      func diameter A -> R_eal equals

      : Def6: (( sup A) - ( inf A)) if A <> {}

      otherwise 0. ;

      coherence ;

      consistency ;

    end

    theorem :: MEASURE5:5

    for a,b be R_eal holds (a < b implies ( diameter ].a, b.[) = (b - a)) & (b <= a implies ( diameter ].a, b.[) = 0. )

    proof

      let a,b be R_eal;

      hereby

        assume

         A1: a < b;

        then

         A2: ( sup ].a, b.[) = b by XXREAL_2: 32;

         ].a, b.[ <> {} & ( inf ].a, b.[) = a by A1, XXREAL_1: 33, XXREAL_2: 28;

        hence ( diameter ].a, b.[) = (b - a) by A2, Def6;

      end;

      assume b <= a;

      then ].a, b.[ = {} by XXREAL_1: 28;

      hence thesis by Def6;

    end;

    theorem :: MEASURE5:6

    for a,b be R_eal holds (a <= b implies ( diameter [.a, b.]) = (b - a)) & (b < a implies ( diameter [.a, b.]) = 0. )

    proof

      let a,b be R_eal;

      hereby

        assume

         A1: a <= b;

        then

         A2: ( sup [.a, b.]) = b by XXREAL_2: 29;

         [.a, b.] <> {} & ( inf [.a, b.]) = a by A1, XXREAL_1: 30, XXREAL_2: 25;

        hence ( diameter [.a, b.]) = (b - a) by A2, Def6;

      end;

      assume b < a;

      then [.a, b.] = {} by XXREAL_1: 29;

      hence thesis by Def6;

    end;

    theorem :: MEASURE5:7

    for a,b be R_eal holds (a < b implies ( diameter [.a, b.[) = (b - a)) & (b <= a implies ( diameter [.a, b.[) = 0. )

    proof

      let a,b be R_eal;

      hereby

        assume

         A1: a < b;

        then

         A2: ( sup [.a, b.[) = b by XXREAL_2: 31;

         [.a, b.[ <> {} & ( inf [.a, b.[) = a by A1, XXREAL_1: 31, XXREAL_2: 26;

        hence ( diameter [.a, b.[) = (b - a) by A2, Def6;

      end;

      assume b <= a;

      then [.a, b.[ = {} by XXREAL_1: 27;

      hence thesis by Def6;

    end;

    theorem :: MEASURE5:8

    for a,b be R_eal holds (a < b implies ( diameter ].a, b.]) = (b - a)) & (b <= a implies ( diameter ].a, b.]) = 0. )

    proof

      let a,b be R_eal;

      hereby

        assume

         A1: a < b;

        then

         A2: ( sup ].a, b.]) = b by XXREAL_2: 30;

         ].a, b.] <> {} & ( inf ].a, b.]) = a by A1, XXREAL_1: 32, XXREAL_2: 27;

        hence ( diameter ].a, b.]) = (b - a) by A2, Def6;

      end;

      assume b <= a;

      then ].a, b.] = {} by XXREAL_1: 26;

      hence thesis by Def6;

    end;

    theorem :: MEASURE5:9

    for a,b be R_eal holds a = -infty & b = +infty & (A = ].a, b.[ or A = [.a, b.] or A = [.a, b.[ or A = ].a, b.]) implies ( diameter A) = +infty

    proof

      let a,b be R_eal;

      assume that

       A1: a = -infty & b = +infty and

       A2: A = ].a, b.[ or A = [.a, b.] or A = [.a, b.[ or A = ].a, b.];

      

       A3: ( sup A) = +infty & ( inf A) = -infty by A1, A2, XXREAL_2: 25, XXREAL_2: 26, XXREAL_2: 27, XXREAL_2: 28, XXREAL_2: 29, XXREAL_2: 30, XXREAL_2: 31, XXREAL_2: 32;

      then A is non empty by XXREAL_2: 40;

      

      then ( diameter A) = (b - a) by A1, A3, Def6

      .= +infty by A1, XXREAL_3: 13;

      hence thesis;

    end;

    registration

      cluster empty -> open_interval for Subset of REAL ;

      coherence

      proof

        let S be Subset of REAL ;

        assume S is empty;

        then S = ]. 0. , 0. .[;

        hence thesis;

      end;

    end

    theorem :: MEASURE5:10

    ( diameter {} ) = 0. by Def6;

    

     Lm1: ( diameter A) >= 0

    proof

      per cases ;

        suppose A is empty;

        hence thesis by Def6;

      end;

        suppose A is non empty;

        then ( inf A) <= ( sup A) by XXREAL_2: 40;

        then (( sup A) - ( inf A)) >= 0 by XXREAL_3: 40;

        hence thesis by Def6;

      end;

    end;

    

     Lm2: A c= B implies ( diameter A) <= ( diameter B)

    proof

      assume

       A1: A c= B;

      per cases ;

        suppose A = {} ;

        then ( diameter A) = 0 by Def6;

        hence thesis by Lm1;

      end;

        suppose

         A2: A <> {} ;

        then B <> {} by A1;

        then

         A3: ( diameter B) = (( sup B) - ( inf B)) by Def6;

        

         A4: ( sup A) <= ( sup B) & ( inf B) <= ( inf A) by A1, XXREAL_2: 59, XXREAL_2: 60;

        ( diameter A) = (( sup A) - ( inf A)) by A2, Def6;

        hence thesis by A3, A4, XXREAL_3: 37;

      end;

    end;

    theorem :: MEASURE5:11

    A c= B & B = [.a, b.] & b <= a implies ( diameter A) = 0. & ( diameter B) = 0.

    proof

      assume that

       A1: A c= B and

       A2: B = [.a, b.] and

       A3: b <= a;

      per cases by A3, XXREAL_0: 1;

        suppose

         A4: a = b;

        then B = {a} by A2, XXREAL_1: 17;

        then ( inf B) = a & ( sup B) = a by XXREAL_2: 11, XXREAL_2: 13;

        

        then

         A5: ( diameter B) = (a - a) by A2, A4, Def6

        .= 0 by XXREAL_3: 7;

        then ( diameter A) <= 0 by A1, Lm2;

        hence thesis by A5, Lm1;

      end;

        suppose b < a;

        then

         A6: B = {} by A2, XXREAL_1: 29;

        then A = {} by A1;

        hence thesis by A6, Def6;

      end;

    end;

    theorem :: MEASURE5:12

    A c= B implies ( diameter A) <= ( diameter B) by Lm2;

    theorem :: MEASURE5:13

     0. <= ( diameter A) by Lm1;

    theorem :: MEASURE5:14

    for X be Subset of REAL holds X is non empty closed_interval iff ex a,b be Real st a <= b & X = [.a, b.] by XXREAL_1: 29, XXREAL_1: 30;