:: Some Properties of the Intervals
:: by J\'ozef Bia\las
::
:: Received February 5, 1994
:: Copyright (c) 1994 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 :] )
proof end;

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

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 & F is nonnegative holds
x <= SUM F
proof end;

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

theorem :: MEASURE6:5
canceled;

theorem :: MEASURE6:6
canceled;

theorem :: MEASURE6:7
canceled;

theorem :: MEASURE6:8
canceled;

theorem :: MEASURE6:9
canceled;

theorem :: MEASURE6:10
canceled;

theorem :: MEASURE6:11
canceled;

theorem :: MEASURE6:12
canceled;

theorem :: MEASURE6:13
canceled;

theorem :: MEASURE6:14
canceled;

theorem :: MEASURE6:15
canceled;

theorem :: MEASURE6:16
canceled;

theorem :: MEASURE6:17
canceled;

theorem :: MEASURE6:18
canceled;

theorem :: MEASURE6:19
canceled;

theorem :: MEASURE6:20
canceled;

theorem :: MEASURE6:21
canceled;

theorem :: MEASURE6:22
canceled;

theorem :: MEASURE6:23
canceled;

theorem :: MEASURE6:24
canceled;

theorem :: MEASURE6:25
canceled;

theorem :: MEASURE6:26
canceled;

theorem :: MEASURE6:27
canceled;

theorem :: MEASURE6:28
canceled;

theorem :: MEASURE6:29
canceled;

theorem :: MEASURE6:30
canceled;

theorem :: MEASURE6:31
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 ) & SUM F < eps )
proof end;

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

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

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

registration
cluster non empty complex-membered ext-real-membered real-membered connected Element of bool REAL ;
existence
ex b1 being Subset of REAL st
( not b1 is empty & b1 is connected )
proof end;
end;

theorem :: MEASURE6:35
canceled;

theorem :: MEASURE6:36
canceled;

theorem :: MEASURE6:37
canceled;

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

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

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

theorem Th41: :: MEASURE6:41
for A being non empty Interval
for a being R_eal st ex b being R_eal st
( a <= b & A = [.a,b.[ ) holds
a = inf A
proof end;

theorem :: MEASURE6:42
canceled;

theorem :: MEASURE6:43
canceled;

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

theorem Th45: :: MEASURE6:45
for A being non empty Interval
for b being R_eal st ex a being R_eal st
( a <= b & A = ].a,b.] ) holds
b = sup A
proof end;

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

theorem Th47: :: MEASURE6:47
for A being non empty Interval
for b being R_eal st ex a being R_eal st
( a <= b & A = [.a,b.[ ) holds
b = sup A
proof end;

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

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

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

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

theorem :: MEASURE6:52
canceled;

theorem :: MEASURE6:53
canceled;

theorem :: MEASURE6:54
canceled;

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

theorem :: MEASURE6:56
canceled;

theorem :: MEASURE6:57
canceled;

theorem :: MEASURE6:58
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
proof end;

definition
canceled;
canceled;
canceled;
canceled;
let A be real-membered set ;
let x be real number ;
func x ++ A -> Subset of REAL means :Def6: :: MEASURE6:def 6
for y being Real holds
( y in it iff ex z being Real st
( z in A & y = x + z ) );
existence
ex b1 being Subset of REAL st
for y being Real holds
( y in b1 iff ex z being Real st
( z in A & y = x + z ) )
proof end;
uniqueness
for b1, b2 being Subset of REAL st ( for y being Real holds
( y in b1 iff ex z being Real st
( z in A & y = x + z ) ) ) & ( for y being Real holds
( y in b2 iff ex z being Real st
( z in A & y = x + z ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem MEASURE6:def 2 :
canceled;

:: deftheorem MEASURE6:def 3 :
canceled;

:: deftheorem MEASURE6:def 4 :
canceled;

:: deftheorem MEASURE6:def 5 :
canceled;

:: deftheorem Def6 defines ++ MEASURE6:def 6 :
for A being real-membered set
for x being real number
for b3 being Subset of REAL holds
( b3 = x ++ A iff for y being Real holds
( y in b3 iff ex z being Real st
( z in A & y = x + z ) ) );

theorem Th59: :: MEASURE6:59
for A being Subset of REAL
for x being real number holds (- x) ++ (x ++ A) = A
proof end;

theorem :: MEASURE6:60
for x being real number
for A being Subset of REAL st A = REAL holds
x ++ A = A
proof end;

theorem :: MEASURE6:61
for x being real number holds x ++ {} = {}
proof end;

theorem Th62: :: MEASURE6:62
for A being Interval
for x being real number holds
( A is open_interval iff x ++ A is open_interval )
proof end;

theorem Th63: :: MEASURE6:63
for A being Interval
for x being real number holds
( A is closed_interval iff x ++ A is closed_interval )
proof end;

theorem Th64: :: MEASURE6:64
for A being Interval
for x being real number holds
( A is right_open_interval iff x ++ A is right_open_interval )
proof end;

theorem Th65: :: MEASURE6:65
for A being Interval
for x being real number holds
( A is left_open_interval iff x ++ A is left_open_interval )
proof end;

theorem Th66: :: MEASURE6:66
for A being Interval
for x being real number holds x ++ A is Interval
proof end;

registration
let A be Interval;
let x be real number ;
cluster x ++ A -> interval ;
correctness
coherence
x ++ A is connected ;
by Th66;
end;

theorem Th67: :: MEASURE6:67
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)
proof end;

theorem Th68: :: MEASURE6:68
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)
proof end;

theorem :: MEASURE6:69
for A being Interval
for x being real number holds diameter A = diameter (x ++ A)
proof end;