:: Some Properties of the Intervals
:: by J\'ozef Bia\las
::
:: Received February 5, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users


begin

theorem :: MEASURE6:1
ex F being Function of NAT,[:NAT,NAT:] st
( F is one-to-one & dom F = NAT & rng F = [:NAT,NAT:] )
proofend;

theorem :: MEASURE6:2
for F being Function of NAT,ExtREAL st F is nonnegative holds
0. <= SUM F
proofend;

theorem :: MEASURE6:3
for F being Function of NAT,ExtREAL
for x being R_eal st ex n being Element of NAT st x <= F . n &amp; F is nonnegative holds
x <= SUM F
proofend;

definition
let x be ext-real number ;
func R_EAL x ->  R_eal equals :: MEASURE6:def 1
x;
coherence
 x is R_eal by XXREAL_0:def_1;
end;

:: deftheorem  defines R_EAL MEASURE6:def_1_:_
 for x being ext-real number holds R_EAL x = x;

theorem :: MEASURE6:4
for eps being R_eal st 0. < eps holds
ex F being Function of NAT,ExtREAL st
( ( for n being Element of NAT holds 0. < F . n ) &amp; SUM F < eps )
proofend;

theorem :: MEASURE6:5
for eps being R_eal
for X being non empty Subset of ExtREAL st 0. < eps &amp; inf X is Real holds
ex x being ext-real number st
( x in X &amp; x < (inf X) + eps )
proofend;

theorem :: MEASURE6:6
for eps being R_eal
for X being non empty Subset of ExtREAL st 0. < eps &amp; sup X is Real holds
ex x being ext-real number st
( x in X &amp; (sup X) - eps < x )
proofend;

theorem :: MEASURE6:7
for F being Function of NAT,ExtREAL st F is nonnegative &amp; SUM F < +infty holds
for n being Element of NAT holds F . n in REAL
proofend;

:: PROPERTIES OF THE INTERVALS
registration
cluster non empty complex-membered ext-real-membered real-membered interval for Element of bool REAL;
existence
 ex b1 being Subset of REAL st
( not b1 is empty &amp; b1 is interval )
proofend;
end;

theorem :: MEASURE6:8
for A being non empty Interval
for a being R_eal st ex b being R_eal st
( a <= b &amp; A = ].a,b.[ ) holds
a = inf A by XXREAL_1:28, XXREAL_2:28;

theorem :: MEASURE6:9
for A being non empty Interval
for a being R_eal st ex b being R_eal st
( a <= b &amp; A = ].a,b.] ) holds
a = inf A by XXREAL_1:26, XXREAL_2:27;

theorem :: MEASURE6:10
for A being non empty Interval
for a being R_eal st ex b being R_eal st
( a <= b &amp; A = [.a,b.] ) holds
a = inf A by XXREAL_2:25;

theorem Th11: :: MEASURE6:11
for A being non empty Interval
for a being R_eal st ex b being R_eal st
( a <= b &amp; A = [.a,b.[ ) holds
a = inf A
proofend;

theorem :: MEASURE6:12
for A being non empty Interval
for b being R_eal st ex a being R_eal st
( a <= b &amp; A = ].a,b.[ ) holds
b = sup A by XXREAL_1:28, XXREAL_2:32;

theorem Th13: :: MEASURE6:13
for A being non empty Interval
for b being R_eal st ex a being R_eal st
( a <= b &amp; A = ].a,b.] ) holds
b = sup A
proofend;

theorem :: MEASURE6:14
for A being non empty Interval
for b being R_eal st ex a being R_eal st
( a <= b &amp; A = [.a,b.] ) holds
b = sup A by XXREAL_2:29;

theorem Th15: :: MEASURE6:15
for A being non empty Interval
for b being R_eal st ex a being R_eal st
( a <= b &amp; A = [.a,b.[ ) holds
b = sup A
proofend;

theorem :: MEASURE6:16
for A being non empty Interval st A is open_interval holds
A = ].(inf A),(sup A).[
proofend;

theorem :: MEASURE6:17
for A being non empty Interval st A is closed_interval holds
A = [.(inf A),(sup A).]
proofend;

theorem :: MEASURE6:18
for A being non empty Interval st A is right_open_interval holds
A = [.(inf A),(sup A).[
proofend;

theorem :: MEASURE6:19
for A being non empty Interval st A is left_open_interval holds
A = ].(inf A),(sup A).]
proofend;

theorem :: MEASURE6:20
for A, B being non empty Interval
for a, b being real number st a in A &amp; b in B &amp; sup A <= inf B holds
a <= b
proofend;

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 &amp; z in A &amp; y = x + z ) )
proofend;

theorem :: MEASURE6:22
for A, B being non empty Interval st sup A = inf B &amp; ( sup A in A or inf B in B ) holds
A \/ B is Interval
proofend;

definition
let A be real-membered set ;
let x be real number ;
:: original:++
redefine funcx ++ A ->  Subset of REAL;
coherence
 x ++ A is Subset of REAL by MEMBERED:3;
end;

Lm1:  for A being real-membered set
for x being real number
for y being Real holds
( y in x ++ A iff ex z being Real st
( z in A &amp; y = x + z ) )
proofend;

theorem Th23: :: MEASURE6:23
for A being Subset of REAL
for x being real number holds (- x) ++ (x ++ A) = A
proofend;

theorem :: MEASURE6:24
for x being real number
for A being Subset of REAL st A = REAL holds
x ++ A = A
proofend;

theorem :: MEASURE6:25
for x being real number holds x ++ {} = {} ;

theorem Th26: :: MEASURE6:26
for A being Interval
for x being real number holds
( A is open_interval iff x ++ A is open_interval )
proofend;

theorem Th27: :: MEASURE6:27
for A being Interval
for x being real number holds
( A is closed_interval iff x ++ A is closed_interval )
proofend;

theorem Th28: :: MEASURE6:28
for A being Interval
for x being real number holds
( A is right_open_interval iff x ++ A is right_open_interval )
proofend;

theorem Th29: :: MEASURE6:29
for A being Interval
for x being real number holds
( A is left_open_interval iff x ++ A is left_open_interval )
proofend;

theorem :: MEASURE6:30
for A being Interval
for x being real number holds x ++ A is Interval
proofend;

theorem Th31: :: MEASURE6:31
for A being real-membered set
for x being real number
for y being R_eal st x = y holds
sup (x ++ A) = y + (sup A)
proofend;

theorem Th32: :: MEASURE6:32
for A being real-membered set
for x being real number
for y being R_eal st x = y holds
inf (x ++ A) = y + (inf A)
proofend;

theorem :: MEASURE6:33
for A being Interval
for x being real number holds diameter A = diameter (x ++ A)
proofend;

begin

notation
let X be set ;
synonym  without_zero X for  with_non-empty_elements ;
antonym  with_zero X for  with_non-empty_elements ;
end;

definition
let X be set ;
redefine attr X is with_non-empty_elements  means :Def2: :: MEASURE6:def 2
 not 0 in X;
compatibility
 ( X is without_zero iff not 0 in X ) by SETFAM_1:def_8;
end;

:: deftheorem Def2 defines without_zero MEASURE6:def_2_:_
 for X being set holds
( X is without_zero iff not 0 in X );

registration
cluster REAL  ->  with_zero ;
coherence
 not REAL is without_zero by Def2;
cluster omega  ->  with_zero ;
coherence
 not NAT is without_zero by Def2;
end;

registration
cluster non empty without_zero for set ;
existence
 ex b1 being set st
( not b1 is empty &amp; b1 is without_zero )
proofend;
cluster non empty with_zero for set ;
existence
 ex b1 being set st
( not b1 is empty &amp; b1 is with_zero ) by Def2;
end;

registration
cluster non empty complex-membered ext-real-membered real-membered without_zero for Element of bool REAL;
existence
 ex b1 being Subset of REAL st
( not b1 is empty &amp; b1 is without_zero )
proofend;
cluster non empty complex-membered ext-real-membered real-membered with_zero for Element of bool REAL;
existence
 ex b1 being Subset of REAL st
( not b1 is empty &amp; b1 is with_zero ) by Def2;
end;

theorem Th34: :: MEASURE6:34
for F being set st not F is empty &amp; F is with_non-empty_elements &amp; F is c=-linear holds
F is centered
proofend;

registration
let F be set ;
cluster c=-linear non empty with_non-empty_elements  ->  centered for Element of bool (bool F);
coherence
 for b1 being Subset-Family of F st not b1 is empty &amp; b1 is with_non-empty_elements &amp; b1 is c=-linear holds
b1 is centered by Th34;
end;

registration
let X, Y be non empty set ;
let f be Function of X,Y;
clusterf .: X ->  non empty ;
coherence
 not f .: X is empty
proofend;
end;

definition
let X, Y be set ;
let f be Function of X,Y;
func " f ->  Function of (bool Y),(bool X) means :Def3: :: MEASURE6:def 3
 for y being Subset of Y holds it . y = f " y;
existence
 ex b1 being Function of (bool Y),(bool X) st
for y being Subset of Y holds b1 . y = f " y
proofend;
uniqueness
 for b1, b2 being Function of (bool Y),(bool X) st ( for y being Subset of Y holds b1 . y = f " y ) &amp; ( for y being Subset of Y holds b2 . y = f " y ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines " MEASURE6:def_3_:_
 for X, Y being set
for f being Function of X,Y
for b4 being Function of (bool Y),(bool X) holds
( b4 = " f iff for y being Subset of Y holds b4 . y = f " y );

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
proofend;

theorem Th36: :: MEASURE6:36
for r, s being real number st (abs r) + (abs s) = 0 holds
r = 0
proofend;

theorem Th37: :: MEASURE6:37
for r, s, t being real number st r < s &amp; s < t holds
abs s < (abs r) + (abs t)
proofend;

theorem Th38: :: MEASURE6:38
for seq being Real_Sequence st seq is convergent &amp; seq is non-zero &amp; lim seq = 0 holds
not seq " is bounded
proofend;

theorem Th39: :: MEASURE6:39
for seq being Real_Sequence holds
( rng seq is real-bounded iff seq is bounded )
proofend;

notation
let X be real-membered set ;
synonym  with_max X for  right_end ;
synonym  with_min X for  left_end ;
end;

definition
let X be real-membered set ;
redefine attr X is right_end  means :: MEASURE6:def 4
( X is bounded_above &amp; upper_bound X in X );
compatibility
 ( X is with_max iff ( X is bounded_above &amp; upper_bound X in X ) )
proofend;
redefine attr X is left_end  means :: MEASURE6:def 5
( X is bounded_below &amp; lower_bound X in X );
compatibility
 ( X is with_min iff ( X is bounded_below &amp; lower_bound X in X ) )
proofend;
end;

:: deftheorem  defines with_max MEASURE6:def_4_:_
 for X being real-membered set holds
( X is with_max iff ( X is bounded_above &amp; 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 &amp; lower_bound X in X ) );

registration
cluster non empty complex-membered ext-real-membered real-membered real-bounded closed for Element of bool REAL;
existence
 ex b1 being Subset of REAL st
( not b1 is empty &amp; b1 is closed &amp; b1 is real-bounded )
proofend;
end;

definition
let R be Subset-Family of REAL;
attrR is open  means :: MEASURE6:def 6
 for X being Subset of REAL st X in R holds
X is open ;
attrR is closed  means :Def7: :: MEASURE6:def 7
 for X being Subset of REAL st X in R holds
X is closed ;
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 );

:: deftheorem Def7 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 );

definition
let X be Subset of REAL;
:: original:--
redefine func -- X ->  Subset of REAL;
coherence
 -- X is Subset of REAL by MEMBERED:3;
end;

theorem :: MEASURE6:40
for r being real number
for X being Subset of REAL holds
( r in X iff - r in -- X ) by MEMBER_1:11;

Lm2:  for X being Subset of REAL st X is bounded_above holds
-- X is bounded_below
proofend;

Lm3:  for X being Subset of REAL st X is bounded_below holds
-- X is bounded_above
proofend;

theorem Th41: :: MEASURE6:41
for X being Subset of REAL holds
( X is bounded_above iff -- X is bounded_below )
proofend;

theorem :: MEASURE6:42
for X being Subset of REAL holds
( X is bounded_below iff -- X is bounded_above )
proofend;

theorem Th43: :: MEASURE6:43
for X being non empty Subset of REAL st X is bounded_below holds
lower_bound X = - (upper_bound (-- X))
proofend;

theorem Th44: :: MEASURE6:44
for X being non empty Subset of REAL st X is bounded_above holds
upper_bound X = - (lower_bound (-- X))
proofend;

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

theorem :: MEASURE6:45
for X being Subset of REAL holds
( X is closed iff -- X is closed )
proofend;

Lm5:  for X being Subset of REAL
for p being Real holds p ++ X =  {  (p + r3) where r3 is Real : r3 in X  }
proofend;

theorem Th46: :: MEASURE6:46
for r being real number
for X being Subset of REAL
for q3 being Real holds
( r in X iff q3 + r in q3 ++ X )
proofend;

theorem :: MEASURE6:47
for X being Subset of REAL holds X = 0 ++ X by MEMBER_1:146;

theorem :: MEASURE6:48
for X being Subset of REAL
for q3, p3 being Real holds q3 ++ (p3 ++ X) = (q3 + p3) ++ X by MEMBER_1:147;

Lm6:  for X being Subset of REAL
for s being Real st X is bounded_above holds
s ++ X is bounded_above
proofend;

theorem :: MEASURE6:49
for X being Subset of REAL
for q3 being Real holds
( X is bounded_above iff q3 ++ X is bounded_above )
proofend;

Lm7:  for X being Subset of REAL
for p being Real st X is bounded_below holds
p ++ X is bounded_below
proofend;

theorem :: MEASURE6:50
for X being Subset of REAL
for q3 being Real holds
( X is bounded_below iff q3 ++ X is bounded_below )
proofend;

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)
proofend;

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)
proofend;

Lm8:  for q3 being Real
for X being Subset of REAL st X is closed holds
q3 ++ X is closed
proofend;

theorem :: MEASURE6:53
for X being Subset of REAL
for q3 being Real holds
( X is closed iff q3 ++ X is closed )
proofend;

definition
let X be Subset of REAL;
func Inv X ->  Subset of REAL equals :: MEASURE6:def 8
 {  (1 / r3) where r3 is Real : r3 in X  }  ;
coherence
  {  (1 / r3) where r3 is Real : r3 in X  }  is Subset of REAL
proofend;
involutiveness
 for b1, b2 being Subset of REAL st b1 =  {  (1 / r3) where r3 is Real : r3 in b2  }  holds
b2 =  {  (1 / r3) where r3 is Real : r3 in b1  }
proofend;
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  }  ;

theorem Th54: :: MEASURE6:54
for r being real number
for X being Subset of REAL holds
( r in X iff 1 / r in Inv X )
proofend;

registration
let X be non empty Subset of REAL;
cluster Inv X ->  non empty ;
coherence
 not Inv X is empty
proofend;
end;

registration
let X be without_zero Subset of REAL;
cluster Inv X ->  without_zero ;
coherence
 Inv X is without_zero
proofend;
end;

theorem :: MEASURE6:55
for X being without_zero Subset of REAL st X is closed &amp; X is real-bounded holds
Inv X is closed
proofend;

theorem Th56: :: MEASURE6:56
for Z being Subset-Family of REAL st Z is closed holds
meet Z is closed
proofend;

definition
let X be Subset of REAL;
func Cl X ->  Subset of REAL equals :: MEASURE6:def 9
 meet  {  A where A is Subset of REAL : ( X c= A &amp; A is closed )  }  ;
coherence
 meet  {  A where A is Subset of REAL : ( X c= A &amp; A is closed )  }  is Subset of REAL
proofend;
projectivity
 for b1, b2 being Subset of REAL st b1 = meet  {  A where A is Subset of REAL : ( b2 c= A &amp; A is closed )  }  holds
b1 = meet  {  A where A is Subset of REAL : ( b1 c= A &amp; A is closed )  }
proofend;
end;

:: deftheorem  defines Cl MEASURE6:def_9_:_
 for X being Subset of REAL holds Cl X = meet  {  A where A is Subset of REAL : ( X c= A &amp; A is closed )  }  ;

registration
let X be Subset of REAL;
cluster Cl X ->  closed ;
coherence
 Cl X is closed
proofend;
end;

theorem Th57: :: MEASURE6:57
for X being Subset of REAL
for Y being closed Subset of REAL st X c= Y holds
Cl X c= Y
proofend;

theorem Th58: :: MEASURE6:58
for X being Subset of REAL holds X c= Cl X
proofend;

theorem Th59: :: MEASURE6:59
for X being Subset of REAL holds
( X is closed iff X = Cl X )
proofend;

theorem :: MEASURE6:60
Cl ({} REAL) = {} by Th59;

theorem :: MEASURE6:61
Cl ([#] REAL) = REAL by Th59;

theorem :: MEASURE6:62
for X, Y being Subset of REAL st X c= Y holds
Cl X c= Cl Y
proofend;

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 )
proofend;

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 &amp; seq is convergent &amp; lim seq = r3 )
proofend;

begin

definition
let X be set ;
let f be Function of X,REAL;
:: original:bounded_below
redefine attrf is bounded_below  means :: MEASURE6:def 10
f .: X is bounded_below ;
compatibility
 ( f is bounded_below iff f .: X is bounded_below )
proofend;
:: original:bounded_above
redefine attrf is bounded_above  means :: MEASURE6:def 11
f .: X is bounded_above ;
compatibility
 ( f is bounded_above iff f .: X is bounded_above )
proofend;
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 );

:: 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 );

definition
let X be set ;
let f be Function of X,REAL;
attrf is with_max  means :: MEASURE6:def 12
f .: X is with_max ;
attrf is with_min  means :: MEASURE6:def 13
f .: X is with_min ;
end;

:: 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 );

:: 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 );

theorem Th65: :: MEASURE6:65
for X, A being set
for f being Function of X,REAL holds (- f) .: A = -- (f .: A)
proofend;

Lm9:  for X being non empty set
for f being Function of X,REAL st f is with_max holds
- f is with_min
proofend;

Lm10:  for X being non empty set
for f being Function of X,REAL st f is with_min holds
- f is with_max
proofend;

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 )
proofend;

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 )
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

notation
let f be real-valued Function;
synonym  Inv f for f " ;
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
proofend;
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)
proofend;

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 &amp; x = - a )
proofend;