:: by J\'ozef Bia\las

::

:: Received February 5, 1994

:: Copyright (c) 1994-2021 Association of Mizar Users

theorem :: MEASURE6:3

for F being sequence of ExtREAL

for x being R_eal st ex n being Element of NAT st x <= F . n & F is nonnegative holds

x <= SUM F

for x being R_eal st ex n being Element of NAT st x <= F . n & F is nonnegative holds

x <= SUM F

proof end;

definition
end;

theorem :: MEASURE6:4

for eps being ExtReal st 0. < eps holds

ex F being sequence of ExtREAL st

( ( for n being Nat holds 0. < F . n ) & SUM F < eps )

ex F being sequence of ExtREAL st

( ( for n being Nat holds 0. < F . n ) & SUM F < eps )

proof end;

theorem :: MEASURE6:5

for eps being ExtReal

for X being non empty Subset of ExtREAL st 0. < eps & inf X is Real holds

ex x being ExtReal st

( x in X & x < (inf X) + eps )

for X being non empty Subset of ExtREAL st 0. < eps & inf X is Real holds

ex x being ExtReal st

( x in X & x < (inf X) + eps )

proof end;

theorem :: MEASURE6:6

for eps being ExtReal

for X being non empty Subset of ExtREAL st 0. < eps & sup X is Real holds

ex x being ExtReal st

( x in X & (sup X) - eps < x )

for X being non empty Subset of ExtREAL st 0. < eps & sup X is Real holds

ex x being ExtReal st

( x in X & (sup X) - eps < x )

proof end;

theorem :: MEASURE6:7

for F being sequence of ExtREAL st F is nonnegative & SUM F < +infty holds

for n being Element of NAT holds F . n in REAL

for n being Element of NAT holds F . n in REAL

proof end;

:: PROPERTIES OF THE INTERVALS

registration

ex b_{1} being Subset of REAL st

( not b_{1} is empty & b_{1} is interval )
end;

cluster non empty complex-membered ext-real-membered real-membered interval for Element of bool REAL;

existence ex b

( not b

proof end;

theorem :: MEASURE6:8

theorem :: MEASURE6:9

theorem :: MEASURE6:10

theorem Th11: :: MEASURE6:11

for A being non empty Interval

for a being ExtReal st ex b being ExtReal st

( a <= b & A = [.a,b.[ ) holds

a = inf A

for a being ExtReal st ex b being ExtReal st

( a <= b & A = [.a,b.[ ) holds

a = inf A

proof end;

theorem :: MEASURE6:12

theorem Th13: :: MEASURE6:13

for A being non empty Interval

for b being ExtReal st ex a being ExtReal st

( a <= b & A = ].a,b.] ) holds

b = sup A

for b being ExtReal st ex a being ExtReal st

( a <= b & A = ].a,b.] ) holds

b = sup A

proof end;

theorem :: MEASURE6:14

theorem Th15: :: MEASURE6:15

for A being non empty Interval

for b being ExtReal st ex a being ExtReal st

( a <= b & A = [.a,b.[ ) holds

b = sup A

for b being ExtReal st ex a being ExtReal st

( a <= b & A = [.a,b.[ ) holds

b = sup A

proof end;

theorem :: MEASURE6:20

for A, B being non empty Interval

for a, b being Real st a in A & b in B & sup A <= inf B holds

a <= b

for a, b being Real st a in A & b in B & sup A <= inf B holds

a <= b

proof end;

theorem :: MEASURE6:21

for A, B being real-membered set

for y being Real holds

( y in B ++ A iff ex x, z being Real st

( x in B & z in A & y = x + z ) )

for y being Real holds

( y in B ++ A iff ex x, z being Real st

( x in B & z in A & y = x + z ) )

proof end;

theorem :: MEASURE6:22

for A, B being non empty Interval st sup A = inf B & ( sup A in A or inf B in B ) holds

A \/ B is Interval by XXREAL_2:def 5, XXREAL_2:def 6, XXREAL_2:90, XXREAL_2:91;

A \/ B is Interval by XXREAL_2:def 5, XXREAL_2:def 6, XXREAL_2:90, XXREAL_2:91;

definition

let A be real-membered set ;

let x be Real;

:: original: ++

redefine func x ++ A -> Subset of REAL;

coherence

x ++ A is Subset of REAL by MEMBERED:3;

end;
let x be Real;

:: original: ++

redefine func x ++ A -> Subset of REAL;

coherence

x ++ A is Subset of REAL by MEMBERED:3;

Lm1: for A being real-membered set

for x, y being Real holds

( y in x ++ A iff ex z being Real st

( z in A & y = x + z ) )

proof end;

theorem Th28: :: MEASURE6:28

for A being Interval

for x being Real holds

( A is right_open_interval iff x ++ A is right_open_interval )

for x being Real holds

( A is right_open_interval iff x ++ A is right_open_interval )

proof end;

theorem Th29: :: MEASURE6:29

for A being Interval

for x being Real holds

( A is left_open_interval iff x ++ A is left_open_interval )

for x being Real holds

( A is left_open_interval iff x ++ A is left_open_interval )

proof end;

theorem Th31: :: MEASURE6:31

for A being real-membered set

for x being Real

for y being R_eal st x = y holds

sup (x ++ A) = y + (sup A)

for x being Real

for y being R_eal st x = y holds

sup (x ++ A) = y + (sup A)

proof end;

theorem Th32: :: MEASURE6:32

for A being real-membered set

for x being Real

for y being R_eal st x = y holds

inf (x ++ A) = y + (inf A)

for x being Real

for y being R_eal st x = y holds

inf (x ++ A) = y + (inf A)

proof end;

notation

let X be set ;

synonym without_zero X for with_non-empty_elements ;

antonym with_zero X for with_non-empty_elements ;

end;
synonym without_zero X for with_non-empty_elements ;

antonym with_zero X for with_non-empty_elements ;

definition
end;

:: deftheorem Def1 defines without_zero MEASURE6:def 2 :

for X being set holds

( X is without_zero iff not 0 in X );

for X being set holds

( X is without_zero iff not 0 in X );

registration
end;

registration

existence

ex b_{1} being set st

( not b_{1} is empty & b_{1} is without_zero )

ex b_{1} being set st

( not b_{1} is empty & b_{1} is with_zero )
by Def1;

end;
ex b

( not b

proof end;

existence ex b

( not b

registration

ex b_{1} being Subset of REAL st

( not b_{1} is empty & b_{1} is without_zero )

ex b_{1} being Subset of REAL st

( not b_{1} is empty & b_{1} is with_zero )
end;

cluster non empty complex-membered ext-real-membered real-membered without_zero for Element of bool REAL;

existence ex b

( not b

proof end;

cluster non empty complex-membered ext-real-membered real-membered with_zero for Element of bool REAL;

existence ex b

( not b

proof end;

theorem Th34: :: MEASURE6:34

for F being set st not F is empty & F is with_non-empty_elements & F is c=-linear holds

F is centered

F is centered

proof end;

registration

let F be set ;

coherence

for b_{1} being Subset-Family of F st not b_{1} is empty & b_{1} is with_non-empty_elements & b_{1} is c=-linear holds

b_{1} is centered
by Th34;

end;
coherence

for b

b

registration
end;

definition

let X, Y be set ;

let f be Function of X,Y;

ex b_{1} being Function of (bool Y),(bool X) st

for y being Subset of Y holds b_{1} . y = f " y

for b_{1}, b_{2} being Function of (bool Y),(bool X) st ( for y being Subset of Y holds b_{1} . y = f " y ) & ( for y being Subset of Y holds b_{2} . y = f " y ) holds

b_{1} = b_{2}

end;
let f be Function of X,Y;

func " f -> Function of (bool Y),(bool X) means :Def2: :: MEASURE6:def 3

for y being Subset of Y holds it . y = f " y;

existence for y being Subset of Y holds it . y = f " y;

ex b

for y being Subset of Y holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines " MEASURE6:def 3 :

for X, Y being set

for f being Function of X,Y

for b_{4} being Function of (bool Y),(bool X) holds

( b_{4} = " f iff for y being Subset of Y holds b_{4} . y = f " y );

for X, Y being set

for f being Function of X,Y

for b

( b

theorem :: MEASURE6:35

for X, Y, x being set

for S being Subset-Family of Y

for f being Function of X,Y st x in meet ((" f) .: S) holds

f . x in meet S

for S being Subset-Family of Y

for f being Function of X,Y st x in meet ((" f) .: S) holds

f . x in meet S

proof end;

theorem Th38: :: MEASURE6:38

for seq being Real_Sequence st seq is convergent & seq is non-zero & lim seq = 0 holds

not seq " is bounded

not seq " is bounded

proof end;

notation
end;

definition

let X be real-membered set ;

compatibility

( X is with_max iff ( X is bounded_above & upper_bound X in X ) )

( X is with_min iff ( X is bounded_below & lower_bound X in X ) )

end;
compatibility

( X is with_max iff ( X is bounded_above & upper_bound X in X ) )

proof end;

compatibility ( X is with_min iff ( X is bounded_below & lower_bound X in X ) )

proof end;

:: deftheorem defines with_max MEASURE6:def 4 :

for X being real-membered set holds

( X is with_max iff ( X is bounded_above & upper_bound X in X ) );

for X being real-membered set holds

( X is with_max iff ( X is bounded_above & upper_bound X in X ) );

:: deftheorem defines with_min MEASURE6:def 5 :

for X being real-membered set holds

( X is with_min iff ( X is bounded_below & lower_bound X in X ) );

for X being real-membered set holds

( X is with_min iff ( X is bounded_below & lower_bound X in X ) );

registration

ex b_{1} being Subset of REAL st

( not b_{1} is empty & b_{1} is closed & b_{1} is real-bounded )
end;

cluster non empty complex-membered ext-real-membered real-membered real-bounded closed for Element of bool REAL;

existence ex b

( not b

proof end;

:: deftheorem defines open MEASURE6:def 6 :

for R being Subset-Family of REAL holds

( R is open iff for X being Subset of REAL st X in R holds

X is open );

for R being Subset-Family of REAL holds

( R is open iff for X being Subset of REAL st X in R holds

X is open );

:: deftheorem defines closed MEASURE6:def 7 :

for R being Subset-Family of REAL holds

( R is closed iff for X being Subset of REAL st X in R holds

X is closed );

for R being Subset-Family of REAL holds

( R is closed iff for X being Subset of REAL st X in R holds

X is closed );

definition

let X be Subset of REAL;

:: original: --

redefine func -- X -> Subset of REAL;

coherence

-- X is Subset of REAL by MEMBERED:3;

end;
:: original: --

redefine func -- X -> Subset of REAL;

coherence

-- X is Subset of REAL by MEMBERED:3;

theorem :: MEASURE6:40

Lm2: for X being Subset of REAL st X is bounded_above holds

-- X is bounded_below

proof end;

Lm3: for X being Subset of REAL st X is bounded_below holds

-- X is bounded_above

proof end;

theorem Th43: :: MEASURE6:43

for X being non empty Subset of REAL st X is bounded_below holds

lower_bound X = - (upper_bound (-- X))

lower_bound X = - (upper_bound (-- X))

proof end;

theorem Th44: :: MEASURE6:44

for X being non empty Subset of REAL st X is bounded_above holds

upper_bound X = - (lower_bound (-- X))

upper_bound X = - (lower_bound (-- X))

proof end;

Lm4: for X being Subset of REAL st X is closed holds

-- X is closed

proof end;

Lm5: for X being Subset of REAL

for p being Real holds p ++ X = { (p + r3) where r3 is Real : r3 in X }

proof end;

theorem Th46: :: MEASURE6:46

for r being Real

for X being Subset of REAL

for q3 being Real holds

( r in X iff q3 + r in q3 ++ X )

for X being Subset of REAL

for q3 being Real holds

( r in X iff q3 + r in q3 ++ X )

proof end;

theorem :: MEASURE6:48

Lm6: for X being Subset of REAL

for s being Real st X is bounded_above holds

s ++ X is bounded_above

proof end;

theorem :: MEASURE6:49

for X being Subset of REAL

for q3 being Real holds

( X is bounded_above iff q3 ++ X is bounded_above )

for q3 being Real holds

( X is bounded_above iff q3 ++ X is bounded_above )

proof end;

Lm7: for X being Subset of REAL

for p being Real st X is bounded_below holds

p ++ X is bounded_below

proof end;

theorem :: MEASURE6:50

for X being Subset of REAL

for q3 being Real holds

( X is bounded_below iff q3 ++ X is bounded_below )

for q3 being Real holds

( X is bounded_below iff q3 ++ X is bounded_below )

proof end;

theorem :: MEASURE6:51

for q3 being Real

for X being non empty Subset of REAL st X is bounded_below holds

lower_bound (q3 ++ X) = q3 + (lower_bound X)

for X being non empty Subset of REAL st X is bounded_below holds

lower_bound (q3 ++ X) = q3 + (lower_bound X)

proof end;

theorem :: MEASURE6:52

for q3 being Real

for X being non empty Subset of REAL st X is bounded_above holds

upper_bound (q3 ++ X) = q3 + (upper_bound X)

for X being non empty Subset of REAL st X is bounded_above holds

upper_bound (q3 ++ X) = q3 + (upper_bound X)

proof end;

Lm8: for q3 being Real

for X being Subset of REAL st X is closed holds

q3 ++ X is closed

proof end;

definition

let X be Subset of REAL;

coherence

{ (1 / r3) where r3 is Real : r3 in X } is Subset of REAL

for b_{1}, b_{2} being Subset of REAL st b_{1} = { (1 / r3) where r3 is Real : r3 in b_{2} } holds

b_{2} = { (1 / r3) where r3 is Real : r3 in b_{1} }

end;
coherence

{ (1 / r3) where r3 is Real : r3 in X } is Subset of REAL

proof end;

involutiveness for b

b

proof end;

:: deftheorem defines Inv MEASURE6:def 8 :

for X being Subset of REAL holds Inv X = { (1 / r3) where r3 is Real : r3 in X } ;

for X being Subset of REAL holds Inv X = { (1 / r3) where r3 is Real : r3 in X } ;

definition

let X be real-membered set ;

meet { A where A is Subset of REAL : ( X c= A & A is closed ) } is Subset of REAL

for b_{1} being Subset of REAL

for b_{2} being real-membered set st b_{1} = meet { A where A is Subset of REAL : ( b_{2} c= A & A is closed ) } holds

b_{1} = meet { A where A is Subset of REAL : ( b_{1} c= A & A is closed ) }

end;
func Cl X -> Subset of REAL equals :: MEASURE6:def 9

meet { A where A is Subset of REAL : ( X c= A & A is closed ) } ;

coherence meet { A where A is Subset of REAL : ( X c= A & A is closed ) } ;

meet { A where A is Subset of REAL : ( X c= A & A is closed ) } is Subset of REAL

proof end;

projectivity for b

for b

b

proof end;

:: deftheorem defines Cl MEASURE6:def 9 :

for X being real-membered set holds Cl X = meet { A where A is Subset of REAL : ( X c= A & A is closed ) } ;

for X being real-membered set holds Cl X = meet { A where A is Subset of REAL : ( X c= A & A is closed ) } ;

registration
end;

theorem Th63: :: MEASURE6:63

for X being Subset of REAL

for r3 being Real holds

( r3 in Cl X iff for O being open Subset of REAL st r3 in O holds

not O /\ X is empty )

for r3 being Real holds

( r3 in Cl X iff for O being open Subset of REAL st r3 in O holds

not O /\ X is empty )

proof end;

theorem :: MEASURE6:64

for X being Subset of REAL

for r3 being Real st r3 in Cl X holds

ex seq being Real_Sequence st

( rng seq c= X & seq is convergent & lim seq = r3 )

for r3 being Real st r3 in Cl X holds

ex seq being Real_Sequence st

( rng seq c= X & seq is convergent & lim seq = r3 )

proof end;

definition

let X be set ;

let f be Function of X,REAL;

( f is bounded_below iff f .: X is bounded_below )

( f is bounded_above iff f .: X is bounded_above )

end;
let f be Function of X,REAL;

:: original: bounded_below

redefine attr f is bounded_below means :: MEASURE6:def 10

f .: X is bounded_below ;

compatibility redefine attr f is bounded_below means :: MEASURE6:def 10

f .: X is bounded_below ;

( f is bounded_below iff f .: X is bounded_below )

proof end;

:: original: bounded_above

redefine attr f is bounded_above means :: MEASURE6:def 11

f .: X is bounded_above ;

compatibility redefine attr f is bounded_above means :: MEASURE6:def 11

f .: X is bounded_above ;

( f is bounded_above iff f .: X is bounded_above )

proof end;

:: deftheorem defines bounded_below MEASURE6:def 10 :

for X being set

for f being Function of X,REAL holds

( f is bounded_below iff f .: X is bounded_below );

for X being set

for f being Function of X,REAL holds

( f is bounded_below iff f .: X is bounded_below );

:: deftheorem defines bounded_above MEASURE6:def 11 :

for X being set

for f being Function of X,REAL holds

( f is bounded_above iff f .: X is bounded_above );

for X being set

for f being Function of X,REAL holds

( f is bounded_above iff f .: X is bounded_above );

:: deftheorem defines with_max MEASURE6:def 12 :

for X being set

for f being Function of X,REAL holds

( f is with_max iff f .: X is with_max );

for X being set

for f being Function of X,REAL holds

( f is with_max iff f .: X is with_max );

:: deftheorem defines with_min MEASURE6:def 13 :

for X being set

for f being Function of X,REAL holds

( f is with_min iff f .: X is with_min );

for X being set

for f being Function of X,REAL holds

( f is with_min iff f .: X is with_min );

Lm9: for X being non empty set

for f being Function of X,REAL st f is with_max holds

- f is with_min

proof end;

Lm10: for X being non empty set

for f being Function of X,REAL st f is with_min holds

- f is with_max

proof end;

theorem Th66: :: MEASURE6:66

for X being non empty set

for f being Function of X,REAL holds

( f is with_min iff - f is with_max )

for f being Function of X,REAL holds

( f is with_min iff - f is with_max )

proof end;

theorem :: MEASURE6:67

for X being non empty set

for f being Function of X,REAL holds

( f is with_max iff - f is with_min )

for f being Function of X,REAL holds

( f is with_max iff - f is with_min )

proof end;

theorem :: MEASURE6:68

for X being set

for A being Subset of REAL

for f being Function of X,REAL holds (- f) " A = f " (-- A)

for A being Subset of REAL

for f being Function of X,REAL holds (- f) " A = f " (-- A)

proof end;

theorem :: MEASURE6:69

for X, A being set

for f being Function of X,REAL

for s being Real holds (s + f) .: A = s ++ (f .: A)

for f being Function of X,REAL

for s being Real holds (s + f) .: A = s ++ (f .: A)

proof end;

theorem :: MEASURE6:70

for X being set

for A being Subset of REAL

for f being Function of X,REAL

for q3 being Real holds (q3 + f) " A = f " ((- q3) ++ A)

for A being Subset of REAL

for f being Function of X,REAL

for q3 being Real holds (q3 + f) " A = f " ((- q3) ++ A)

proof end;

definition

let C be set ;

let D be real-membered set ;

let f be PartFunc of C,D;

:: original: Inv

redefine func Inv f -> PartFunc of C,REAL;

coherence

Inv f is PartFunc of C,REAL

end;
let D be real-membered set ;

let f be PartFunc of C,D;

:: original: Inv

redefine func Inv f -> PartFunc of C,REAL;

coherence

Inv f is PartFunc of C,REAL

proof end;

theorem :: MEASURE6:71

for X being set

for A being without_zero Subset of REAL

for f being Function of X,REAL holds (Inv f) " A = f " (Inv A)

for A being without_zero Subset of REAL

for f being Function of X,REAL holds (Inv f) " A = f " (Inv A)

proof end;

theorem :: MEASURE6:72

for A being Subset of REAL

for x being Real st x in -- A holds

ex a being Real st

( a in A & x = - a )

for x being Real st x in -- A holds

ex a being Real st

( a in A & x = - a )

proof end;