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

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

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

proof end;

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 ;
:: original: ++
redefine func x ++ A -> Subset of REAL;
coherence
x ++ A is Subset of REAL by MEMBERED:3;

end;

:: deftheorem MEASURE6:def 2 :
canceled;

:: deftheorem MEASURE6:def 3 :
canceled;

:: deftheorem MEASURE6:def 4 :
canceled;

:: deftheorem MEASURE6:def 5 :
canceled;

Def6: 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 & y = x + z ) )

proof end;

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 ++ {} = {} ;

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 :: MEASURE6:66

for A being Interval
for x being real number holds x ++ A is Interval

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

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 :Def1: :: MEASURE6:def 6
not 0 in X;
compatibility
( X is without_zero iff not 0 in X ) by SETFAM_1:def 9;

end;

:: deftheorem Def1 defines without_zero MEASURE6:def 6 :
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 Def1;
cluster omega -> with_zero ;
coherence
not NAT is without_zero by Def1;

end;

registration

cluster non empty without_zero set ;
existence
ex b₁ being set st
( not b₁ is empty & b₁ is without_zero )

proof end;

cluster non empty with_zero set ;
existence
ex b₁ being set st
( not b₁ is empty & not b₁ is without_zero ) by Def1;

end;

registration

cluster non empty complex-membered ext-real-membered real-membered without_zero Element of bool REAL;
existence
ex b₁ being Subset of REAL st
( not b₁ is empty & b₁ is without_zero )

proof end;

cluster non empty complex-membered ext-real-membered real-membered with_zero Element of bool REAL;
existence
ex b₁ being Subset of REAL st
( not b₁ is empty & not b₁ is without_zero ) by Def1;

end;

theorem Th1: :: MEASURE6:70

for F being set st not F is empty & F is without_zero & F is c=-linear holds
F is centered

proof end;

registration

let F be set ;
cluster c=-linear non empty with_non-empty_elements -> centered Element of bool (bool F);
coherence
for b₁ being Subset-Family of F st not b₁ is empty & b₁ is without_zero & b₁ is c=-linear holds
b₁ is centered by Th1;

end;

registration

let X, Y be non empty set ;
let f be Function of X,Y;
cluster f .: X -> non empty ;
coherence
not f .: X is empty

proof end;

end;

definition

let X, Y be set ;
let f be Function of X,Y;
func " f -> Function of (bool Y),(bool X) means :Def2: :: MEASURE6:def 7
for y being Subset of Y holds it . y = f " y;
existence
ex b₁ being Function of (bool Y),(bool X) st
for y being Subset of Y holds b₁ . y = f " y

proof end;

uniqueness
for b₁, b₂ being Function of (bool Y),(bool X) st ( for y being Subset of Y holds b₁ . y = f " y ) & ( for y being Subset of Y holds b₂ . y = f " y ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines " MEASURE6:def 7 :
for X, Y being set
for f being Function of X,Y
for b₄ being Function of (bool Y),(bool X) holds
( b₄ = " f iff for y being Subset of Y holds b₄ . y = f " y );

theorem :: MEASURE6:71

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

proof end;

theorem Th3: :: MEASURE6:72

for r, s being real number st (abs r) + (abs s) = 0 holds
r = 0

proof end;

theorem Th4: :: MEASURE6:73

for r, s, t being real number st r < s & s < t holds
abs s < (abs r) + (abs t)

proof end;

theorem Th6: :: MEASURE6:74

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

proof end;

theorem Th7: :: MEASURE6:75

for seq being Real_Sequence holds
( rng seq is bounded iff seq is bounded )

proof end;

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 8
( X is bounded_above & upper_bound X in X );
compatibility
( X is with_max iff ( X is bounded_above & upper_bound X in X ) )

proof end;

redefine attr X is left_end means :: MEASURE6:def 9
( X is bounded_below & lower_bound X in X );
compatibility
( X is with_min iff ( X is bounded_below & lower_bound X in X ) )

proof end;

end;

:: deftheorem defines with_max MEASURE6:def 8 :
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 9 :
for X being real-membered set holds
( X is with_min iff ( X is bounded_below & lower_bound X in X ) );

registration

cluster non empty complex-membered ext-real-membered real-membered bounded closed Element of bool REAL;
existence
ex b₁ being Subset of REAL st
( not b₁ is empty & b₁ is closed & b₁ is bounded )

proof end;

end;

definition

let R be Subset-Family of REAL;
attr R is open means :: MEASURE6:def 10
for X being Subset of REAL st X in R holds
X is open ;
attr R is closed means :Def6X: :: MEASURE6:def 11
for X being Subset of REAL st X in R holds
X is closed ;

end;

:: deftheorem defines open MEASURE6:def 10 :
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 Def6X defines closed MEASURE6:def 11 :
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:76

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

Lm1: for X being Subset of REAL st X is bounded_above holds
-- X is bounded_below

proof end;

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

proof end;

theorem Th15: :: MEASURE6:77

for X being Subset of REAL holds
( X is bounded_above iff -- X is bounded_below )

proof end;

theorem :: MEASURE6:78

for X being Subset of REAL holds
( X is bounded_below iff -- X is bounded_above )

proof end;

theorem Th17: :: MEASURE6:79

for X being non empty Subset of REAL st X is bounded_below holds
lower_bound X = - (upper_bound (-- X))

proof end;

theorem Th18: :: MEASURE6:80

for X being non empty Subset of REAL st X is bounded_above holds
upper_bound X = - (lower_bound (-- X))

proof end;

Lm3: for X being Subset of REAL st X is closed holds
-- X is closed

proof end;

theorem :: MEASURE6:81

for X being Subset of REAL holds
( X is closed iff -- X is closed )

proof end;

LmX: 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 Th20: :: MEASURE6:82

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 )

proof end;

theorem :: MEASURE6:83

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

theorem :: MEASURE6:84

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

Lm4: 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:85

for X being Subset of REAL
for q3 being Real holds
( X is bounded_above iff q3 ++ X is bounded_above )

proof end;

Lm5: 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:86

for X being Subset of REAL
for q3 being Real holds
( X is bounded_below iff q3 ++ X is bounded_below )

proof end;

theorem :: MEASURE6:87

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)

proof end;

theorem :: MEASURE6:88

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)

proof end;

Lm6: for q3 being Real
for X being Subset of REAL st X is closed holds
q3 ++ X is closed

proof end;

theorem :: MEASURE6:89

for X being Subset of REAL
for q3 being Real holds
( X is closed iff q3 ++ X is closed )

proof end;

definition

let X be Subset of REAL;
func Inv X -> Subset of REAL equals :: MEASURE6:def 12
{ (1 / r3) where r3 is Real : r3 in X } ;
coherence
{ (1 / r3) where r3 is Real : r3 in X } is Subset of REAL

proof end;

involutiveness
for b₁, b₂ being Subset of REAL st b₁ = { (1 / r3) where r3 is Real : r3 in b₂ } holds
b₂ = { (1 / r3) where r3 is Real : r3 in b₁ }

proof end;

end;

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

theorem Th28: :: MEASURE6:90

for r being real number
for X being Subset of REAL holds
( r in X iff 1 / r in Inv X )

proof end;

registration

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

proof end;

end;

registration

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

proof end;

end;

theorem :: MEASURE6:91

for X being without_zero Subset of REAL st X is closed & X is bounded holds
Inv X is closed

proof end;

theorem Th31: :: MEASURE6:92

for Z being Subset-Family of REAL st Z is closed holds
meet Z is closed

proof end;

definition

let X be Subset of REAL;
func Cl X -> Subset of REAL equals :: MEASURE6:def 13
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 ) } is Subset of REAL

proof end;

projectivity
for b₁, b₂ being Subset of REAL st b₁ = meet { A where A is Subset of REAL : ( b₂ c= A & A is closed ) } holds
b₁ = meet { A where A is Subset of REAL : ( b₁ c= A & A is closed ) }

proof end;

end;

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

registration

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

proof end;

end;

theorem Th32: :: MEASURE6:93

for X being Subset of REAL
for Y being closed Subset of REAL st X c= Y holds
Cl X c= Y

proof end;

theorem Th33: :: MEASURE6:94

for X being Subset of REAL holds X c= Cl X

proof end;

theorem Th34: :: MEASURE6:95

for X being Subset of REAL holds
( X is closed iff X = Cl X )

proof end;

theorem :: MEASURE6:96

Cl ({} REAL) = {} by Th34;

theorem :: MEASURE6:97

Cl ([#] REAL) = REAL by Th34;

theorem :: MEASURE6:98

for X, Y being Subset of REAL st X c= Y holds
Cl X c= Cl Y

proof end;

theorem Th38: :: MEASURE6:99

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 )

proof end;

theorem :: MEASURE6:100

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 )

proof end;

begin

definition

let X be set ;
let f be Function of X,REAL;
:: original: bounded_below
redefine attr f is bounded_below means :: MEASURE6:def 14
f .: X is bounded_below ;
compatibility
( f is bounded_below iff f .: X is bounded_below )

proof end;

:: original: bounded_above
redefine attr f is bounded_above means :: MEASURE6:def 15
f .: X is bounded_above ;
compatibility
( f is bounded_above iff f .: X is bounded_above )

proof end;

end;

:: deftheorem defines bounded_below MEASURE6:def 14 :
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 15 :
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;
attr f is with_max means :: MEASURE6:def 16
f .: X is with_max ;
attr f is with_min means :: MEASURE6:def 17
f .: X is with_min ;

end;

:: deftheorem defines with_max MEASURE6:def 16 :
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 17 :
for X being set
for f being Function of X,REAL holds
( f is with_min iff f .: X is with_min );

theorem Th40: :: MEASURE6:101

for X, A being set
for f being Function of X,REAL holds (- f) .: A = -- (f .: A)

proof end;

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

Lm8: 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 Th41: :: MEASURE6:102

for X being non empty set
for f being Function of X,REAL holds
( f is with_min iff - f is with_max )

proof end;

theorem :: MEASURE6:103

for X being non empty set
for f being Function of X,REAL holds
( f is with_max iff - f is with_min )

proof end;

theorem :: MEASURE6:104

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

proof end;

theorem :: MEASURE6:105

for X, A being set
for f being Function of X,REAL
for s being Real holds (s + f) .: A = s ++ (f .: A)

proof end;

theorem :: MEASURE6:106

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)

proof end;

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

proof end;

end;

theorem :: MEASURE6:107

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)

proof end;

theorem :: MEASURE6:108

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 )

proof end;