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

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;

theorem :: MEASURE6:4

canceled;

theorem :: MEASURE6:5

canceled;

theorem :: MEASURE6:6

canceled;

theorem :: MEASURE6:7

canceled;

theorem Th8: :: MEASURE6:8

for x, y being R_eal st x is Real holds
( (y - x) + x = y & (y + x) - x = y )

proof end;

theorem :: MEASURE6:9

canceled;

theorem Th10: :: MEASURE6:10

for x, y, z being R_eal st z in REAL holds
(z + x) - (z + y) = x - y

proof end;

theorem Th11: :: MEASURE6:11

for x, y, z being R_eal st z in REAL & x <= y holds
( z + x <= z + y & x + z <= y + z & x - z <= y - z )

proof end;

theorem Th12: :: MEASURE6:12

for x, y, z being R_eal st z in REAL & x < y holds
( z + x < z + y & x + z < y + z & x - z < y - z )

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:13

canceled;

theorem :: MEASURE6:14

canceled;

theorem :: MEASURE6:15

canceled;

theorem :: MEASURE6:16

canceled;

theorem :: MEASURE6:17

canceled;

theorem :: MEASURE6:18

canceled;

theorem Th19: :: MEASURE6:19

for x, y being R_eal st 0. < x & x < y holds
0. < y - x

proof end;

theorem :: MEASURE6:20

for x, y, z being R_eal st 0. <= x & 0. <= z & z + x < y holds
z < y - x

proof end;

theorem Th21: :: MEASURE6:21

for x being R_eal holds x - 0. = x

proof end;

theorem Th22: :: MEASURE6:22

for x, y, z being R_eal st 0. <= x & 0. <= z & z + x < y holds
z <= y

proof end;

theorem Th23: :: MEASURE6:23

for x being R_eal st 0. < x holds
ex y being R_eal st
( 0. < y & y < x )

proof end;

theorem Th24: :: MEASURE6:24

for x, z being R_eal st 0. < x & x < z holds
ex y being R_eal st
( 0. < y & x + y < z & y in REAL )

proof end;

theorem :: MEASURE6:25

for x, z being R_eal st 0. <= x & x < z holds
ex y being R_eal st
( 0. < y & x + y < z & y in REAL )

proof end;

theorem Th26: :: MEASURE6:26

for x being R_eal st 0. < x holds
ex y being R_eal st
( 0. < y & y + y < x )

proof end;

definition

let x be R_eal;
assume A1: 0. < x ;
func Seg x -> non empty Subset of ExtREAL means :Def2: :: MEASURE6:def 2
for y being R_eal holds
( y in it iff ( 0. < y & y + y < x ) );
existence
ex b₁ being non empty Subset of ExtREAL st
for y being R_eal holds
( y in b₁ iff ( 0. < y & y + y < x ) )

proof end;

uniqueness
for b₁, b₂ being non empty Subset of ExtREAL st ( for y being R_eal holds
( y in b₁ iff ( 0. < y & y + y < x ) ) ) & ( for y being R_eal holds
( y in b₂ iff ( 0. < y & y + y < x ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines Seg MEASURE6:def 2 :

for x being R_eal st 0. < x holds
for b₂ being non empty Subset of ExtREAL holds
( b₂ = Seg x iff for y being R_eal holds
( y in b₂ iff ( 0. < y & y + y < x ) ) );

definition

let x be R_eal;
func len x -> R_eal equals :: MEASURE6:def 3
sup (Seg x);
correctness
coherence
sup (Seg x) is R_eal;
;

end;

:: deftheorem defines len MEASURE6:def 3 :

for x being R_eal holds len x = sup (Seg x);

theorem Th27: :: MEASURE6:27

for x being R_eal st 0. < x holds
0. < len x

proof end;

theorem Th28: :: MEASURE6:28

for x being R_eal st 0. < x holds
len x <= x

proof end;

theorem Th29: :: MEASURE6:29

for x being R_eal st 0. < x & x < +infty holds
len x is Real

proof end;

theorem Th30: :: MEASURE6:30

for x being R_eal st 0. < x holds
(len x) + (len x) <= x

proof end;

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 connected Element of bool REAL ;
existence
ex b₁ being Subset of REAL st
( not b₁ is empty & b₁ is connected )

proof end;

end;

theorem :: MEASURE6:35

canceled;

theorem :: MEASURE6:36

canceled;

theorem :: MEASURE6:37

canceled;

theorem Def4A: :: 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 Def4B: :: 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

proof end;

theorem Def4C: :: 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

proof end;

theorem Def4D: :: 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 Def5A: :: 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 Def5B: :: 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 Def5C: :: 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

proof end;

theorem Def5D: :: 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;
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 b₁ being Subset of REAL st
for y being Real holds
( y in b₁ iff ex z being Real st
( z in A & y = x + z ) )

proof end;

uniqueness
for b₁, b₂ being Subset of REAL st ( for y being Real holds
( y in b₁ iff ex z being Real st
( z in A & y = x + z ) ) ) & ( for y being Real holds
( y in b₂ iff ex z being Real st
( z in A & y = x + z ) ) ) holds
b₁ = b₂

proof end;

end;

:: 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 b₃ being Subset of REAL holds
( b₃ = x ++ A iff for y being Real holds
( y in b₃ 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 Tx1: :: 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 Tx2: :: 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;