:: Infimum and Supremum of the Set of Real Numbers. Measure Theory
:: by J\'ozef Bia{\l}as
::
:: Received September 27, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users


begin

definition
mode R_eal is Element of ExtREAL ;
end;

definition
:: original: +infty
redefine func +infty -> R_eal;
coherence
+infty is R_eal
by XXREAL_0:def 1;
:: original: -infty
redefine func -infty -> R_eal;
coherence
-infty is R_eal
by XXREAL_0:def 1;
end;

definition
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
let X be ext-real-membered set ;
func SetMajorant X -> ext-real-membered set means :Def14: :: SUPINF_1:def 14
for x being ext-real number holds
( x in it iff x is UpperBound of X );
existence
ex b1 being ext-real-membered set st
for x being ext-real number holds
( x in b1 iff x is UpperBound of X )
proof end;
uniqueness
for b1, b2 being ext-real-membered set st ( for x being ext-real number holds
( x in b1 iff x is UpperBound of X ) ) & ( for x being ext-real number holds
( x in b2 iff x is UpperBound of X ) ) holds
b1 = b2
proof end;
end;

:: deftheorem SUPINF_1:def 1 :
canceled;

:: deftheorem SUPINF_1:def 2 :
canceled;

:: deftheorem SUPINF_1:def 3 :
canceled;

:: deftheorem SUPINF_1:def 4 :
canceled;

:: deftheorem SUPINF_1:def 5 :
canceled;

:: deftheorem SUPINF_1:def 6 :
canceled;

:: deftheorem SUPINF_1:def 7 :
canceled;

:: deftheorem SUPINF_1:def 8 :
canceled;

:: deftheorem SUPINF_1:def 9 :
canceled;

:: deftheorem SUPINF_1:def 10 :
canceled;

:: deftheorem SUPINF_1:def 11 :
canceled;

:: deftheorem SUPINF_1:def 12 :
canceled;

:: deftheorem SUPINF_1:def 13 :
canceled;

:: deftheorem Def14 defines SetMajorant SUPINF_1:def 14 :
for X, b2 being ext-real-membered set holds
( b2 = SetMajorant X iff for x being ext-real number holds
( x in b2 iff x is UpperBound of X ) );

registration
let X be ext-real-membered set ;
cluster SetMajorant X -> non empty ext-real-membered ;
coherence
not SetMajorant X is empty
proof end;
end;

theorem :: SUPINF_1:1
canceled;

theorem :: SUPINF_1:2
canceled;

theorem :: SUPINF_1:3
canceled;

theorem :: SUPINF_1:4
canceled;

theorem :: SUPINF_1:5
canceled;

theorem :: SUPINF_1:6
canceled;

theorem :: SUPINF_1:7
canceled;

theorem :: SUPINF_1:8
canceled;

theorem :: SUPINF_1:9
canceled;

theorem :: SUPINF_1:10
canceled;

theorem :: SUPINF_1:11
canceled;

theorem :: SUPINF_1:12
canceled;

theorem :: SUPINF_1:13
canceled;

theorem :: SUPINF_1:14
canceled;

theorem :: SUPINF_1:15
canceled;

theorem :: SUPINF_1:16
canceled;

theorem :: SUPINF_1:17
canceled;

theorem :: SUPINF_1:18
canceled;

theorem :: SUPINF_1:19
canceled;

theorem :: SUPINF_1:20
canceled;

theorem :: SUPINF_1:21
canceled;

theorem :: SUPINF_1:22
canceled;

theorem :: SUPINF_1:23
canceled;

theorem :: SUPINF_1:24
canceled;

theorem :: SUPINF_1:25
canceled;

theorem :: SUPINF_1:26
canceled;

theorem :: SUPINF_1:27
canceled;

theorem :: SUPINF_1:28
canceled;

theorem :: SUPINF_1:29
canceled;

theorem :: SUPINF_1:30
canceled;

theorem :: SUPINF_1:31
canceled;

theorem :: SUPINF_1:32
canceled;

theorem :: SUPINF_1:33
canceled;

theorem :: SUPINF_1:34
canceled;

theorem :: SUPINF_1:35
canceled;

theorem :: SUPINF_1:36
canceled;

theorem :: SUPINF_1:37
canceled;

theorem :: SUPINF_1:38
canceled;

theorem :: SUPINF_1:39
canceled;

theorem :: SUPINF_1:40
canceled;

theorem :: SUPINF_1:41
canceled;

theorem :: SUPINF_1:42
canceled;

theorem :: SUPINF_1:43
canceled;

theorem :: SUPINF_1:44
canceled;

theorem :: SUPINF_1:45
canceled;

theorem :: SUPINF_1:46
canceled;

theorem :: SUPINF_1:47
canceled;

theorem :: SUPINF_1:48
canceled;

theorem :: SUPINF_1:49
canceled;

theorem :: SUPINF_1:50
canceled;

theorem :: SUPINF_1:51
canceled;

theorem :: SUPINF_1:52
canceled;

theorem :: SUPINF_1:53
for X, Y being ext-real-membered set st X c= Y holds
for x being ext-real number st x in SetMajorant Y holds
x in SetMajorant X
proof end;

definition
let X be ext-real-membered set ;
func SetMinorant X -> ext-real-membered set means :Def15: :: SUPINF_1:def 15
for x being ext-real number holds
( x in it iff x is LowerBound of X );
existence
ex b1 being ext-real-membered set st
for x being ext-real number holds
( x in b1 iff x is LowerBound of X )
proof end;
uniqueness
for b1, b2 being ext-real-membered set st ( for x being ext-real number holds
( x in b1 iff x is LowerBound of X ) ) & ( for x being ext-real number holds
( x in b2 iff x is LowerBound of X ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines SetMinorant SUPINF_1:def 15 :
for X, b2 being ext-real-membered set holds
( b2 = SetMinorant X iff for x being ext-real number holds
( x in b2 iff x is LowerBound of X ) );

registration
let X be ext-real-membered set ;
cluster SetMinorant X -> non empty ext-real-membered ;
coherence
not SetMinorant X is empty
proof end;
end;

theorem :: SUPINF_1:54
canceled;

theorem :: SUPINF_1:55
canceled;

theorem :: SUPINF_1:56
canceled;

theorem :: SUPINF_1:57
for X, Y being ext-real-membered set st X c= Y holds
for x being ext-real number st x in SetMinorant Y holds
x in SetMinorant X
proof end;

theorem :: SUPINF_1:58
canceled;

theorem :: SUPINF_1:59
canceled;

theorem :: SUPINF_1:60
canceled;

theorem :: SUPINF_1:61
canceled;

theorem :: SUPINF_1:62
canceled;

theorem :: SUPINF_1:63
canceled;

theorem :: SUPINF_1:64
canceled;

theorem :: SUPINF_1:65
canceled;

theorem :: SUPINF_1:66
canceled;

theorem :: SUPINF_1:67
canceled;

theorem :: SUPINF_1:68
canceled;

theorem :: SUPINF_1:69
canceled;

theorem :: SUPINF_1:70
canceled;

theorem :: SUPINF_1:71
canceled;

theorem :: SUPINF_1:72
canceled;

theorem :: SUPINF_1:73
canceled;

theorem :: SUPINF_1:74
canceled;

theorem :: SUPINF_1:75
canceled;

theorem :: SUPINF_1:76
canceled;

theorem :: SUPINF_1:77
canceled;

theorem :: SUPINF_1:78
canceled;

theorem :: SUPINF_1:79
canceled;

theorem :: SUPINF_1:80
canceled;

theorem :: SUPINF_1:81
canceled;

theorem :: SUPINF_1:82
for X being non empty ext-real-membered set holds
( sup X = inf (SetMajorant X) & inf X = sup (SetMinorant X) )
proof end;

theorem :: SUPINF_1:83
canceled;

theorem :: SUPINF_1:84
canceled;

theorem :: SUPINF_1:85
canceled;

theorem :: SUPINF_1:86
canceled;

theorem :: SUPINF_1:87
canceled;

theorem :: SUPINF_1:88
canceled;

theorem :: SUPINF_1:89
canceled;

theorem :: SUPINF_1:90
canceled;

theorem :: SUPINF_1:91
canceled;

theorem :: SUPINF_1:92
canceled;

theorem :: SUPINF_1:93
canceled;

theorem :: SUPINF_1:94
canceled;

theorem :: SUPINF_1:95
canceled;

theorem :: SUPINF_1:96
canceled;

theorem :: SUPINF_1:97
canceled;

theorem :: SUPINF_1:98
canceled;

theorem :: SUPINF_1:99
canceled;

theorem :: SUPINF_1:100
canceled;

theorem :: SUPINF_1:101
canceled;

theorem :: SUPINF_1:102
canceled;

theorem :: SUPINF_1:103
canceled;

theorem :: SUPINF_1:104
canceled;

theorem :: SUPINF_1:105
canceled;

theorem :: SUPINF_1:106
canceled;

theorem :: SUPINF_1:107
canceled;

theorem :: SUPINF_1:108
canceled;

registration
let X be non empty set ;
cluster non empty with_non-empty_elements Element of K6(K6(X));
existence
ex b1 being Subset-Family of X st
( not b1 is empty & b1 is with_non-empty_elements )
proof end;
end;

definition
let X be non empty set ;
mode bool_DOMAIN of X is non empty with_non-empty_elements Subset-Family of X;
end;

definition
let F be bool_DOMAIN of ExtREAL;
canceled;
canceled;
canceled;
func SUP F -> ext-real-membered set means :Def19: :: SUPINF_1:def 19
for a being ext-real number holds
( a in it iff ex A being non empty ext-real-membered set st
( A in F & a = sup A ) );
existence
ex b1 being ext-real-membered set st
for a being ext-real number holds
( a in b1 iff ex A being non empty ext-real-membered set st
( A in F & a = sup A ) )
proof end;
uniqueness
for b1, b2 being ext-real-membered set st ( for a being ext-real number holds
( a in b1 iff ex A being non empty ext-real-membered set st
( A in F & a = sup A ) ) ) & ( for a being ext-real number holds
( a in b2 iff ex A being non empty ext-real-membered set st
( A in F & a = sup A ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem SUPINF_1:def 16 :
canceled;

:: deftheorem SUPINF_1:def 17 :
canceled;

:: deftheorem SUPINF_1:def 18 :
canceled;

:: deftheorem Def19 defines SUP SUPINF_1:def 19 :
for F being bool_DOMAIN of ExtREAL
for b2 being ext-real-membered set holds
( b2 = SUP F iff for a being ext-real number holds
( a in b2 iff ex A being non empty ext-real-membered set st
( A in F & a = sup A ) ) );

registration
let F be bool_DOMAIN of ExtREAL;
cluster SUP F -> non empty ext-real-membered ;
coherence
not SUP F is empty
proof end;
end;

theorem :: SUPINF_1:109
canceled;

theorem :: SUPINF_1:110
canceled;

theorem :: SUPINF_1:111
canceled;

theorem Th112: :: SUPINF_1:112
for F being bool_DOMAIN of ExtREAL
for S being non empty ext-real-membered number st S = union F holds
sup S is UpperBound of SUP F
proof end;

theorem Th113: :: SUPINF_1:113
for F being bool_DOMAIN of ExtREAL
for S being ext-real-membered set st S = union F holds
sup (SUP F) is UpperBound of S
proof end;

theorem :: SUPINF_1:114
for F being bool_DOMAIN of ExtREAL
for S being non empty ext-real-membered set st S = union F holds
sup S = sup (SUP F)
proof end;

definition
let F be bool_DOMAIN of ExtREAL;
func INF F -> ext-real-membered set means :Def20: :: SUPINF_1:def 20
for a being ext-real number holds
( a in it iff ex A being non empty ext-real-membered set st
( A in F & a = inf A ) );
existence
ex b1 being ext-real-membered set st
for a being ext-real number holds
( a in b1 iff ex A being non empty ext-real-membered set st
( A in F & a = inf A ) )
proof end;
uniqueness
for b1, b2 being ext-real-membered set st ( for a being ext-real number holds
( a in b1 iff ex A being non empty ext-real-membered set st
( A in F & a = inf A ) ) ) & ( for a being ext-real number holds
( a in b2 iff ex A being non empty ext-real-membered set st
( A in F & a = inf A ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines INF SUPINF_1:def 20 :
for F being bool_DOMAIN of ExtREAL
for b2 being ext-real-membered set holds
( b2 = INF F iff for a being ext-real number holds
( a in b2 iff ex A being non empty ext-real-membered set st
( A in F & a = inf A ) ) );

registration
let F be bool_DOMAIN of ExtREAL;
cluster INF F -> non empty ext-real-membered ;
coherence
not INF F is empty
proof end;
end;

theorem :: SUPINF_1:115
canceled;

theorem :: SUPINF_1:116
canceled;

theorem Th117: :: SUPINF_1:117
for F being bool_DOMAIN of ExtREAL
for S being non empty ext-real-membered set st S = union F holds
inf S is LowerBound of INF F
proof end;

theorem Th118: :: SUPINF_1:118
for F being bool_DOMAIN of ExtREAL
for S being ext-real-membered set st S = union F holds
inf (INF F) is LowerBound of S
proof end;

theorem :: SUPINF_1:119
for F being bool_DOMAIN of ExtREAL
for S being non empty ext-real-membered set st S = union F holds
inf S = inf (INF F)
proof end;