:: Infimum and Supremum of the Set of Real Numbers. Measure Theory
:: by J\'ozef Bia{\l}as
::
:: Received September 27, 1990
:: Copyright (c) 1990 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 b₁ being ext-real-membered set st
for x being ext-real number holds
( x in b₁ iff x is UpperBound of X )

proof end;

uniqueness
for b₁, b₂ being ext-real-membered set st ( for x being ext-real number holds
( x in b₁ iff x is UpperBound of X ) ) & ( for x being ext-real number holds
( x in b₂ iff x is UpperBound of X ) ) holds
b₁ = b₂

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, b₂ being ext-real-membered set holds
( b₂ = SetMajorant X iff for x being ext-real number holds
( x in b₂ 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 b₁ being ext-real-membered set st
for x being ext-real number holds
( x in b₁ iff x is LowerBound of X )

proof end;

uniqueness
for b₁, b₂ being ext-real-membered set st ( for x being ext-real number holds
( x in b₁ iff x is LowerBound of X ) ) & ( for x being ext-real number holds
( x in b₂ iff x is LowerBound of X ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def15 defines SetMinorant SUPINF_1:def 15 :
for X, b₂ being ext-real-membered set holds
( b₂ = SetMinorant X iff for x being ext-real number holds
( x in b₂ 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 b₁ being Subset-Family of X st
( not b₁ is empty & b₁ 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 b₁ being ext-real-membered set st
for a being ext-real number holds
( a in b₁ iff ex A being non empty ext-real-membered set st
( A in F & a = sup A ) )

proof end;

uniqueness
for b₁, b₂ being ext-real-membered set st ( for a being ext-real number holds
( a in b₁ 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 b₂ iff ex A being non empty ext-real-membered set st
( A in F & a = sup A ) ) ) holds
b₁ = b₂

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 b₂ being ext-real-membered set holds
( b₂ = SUP F iff for a being ext-real number holds
( a in b₂ 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 b₁ being ext-real-membered set st
for a being ext-real number holds
( a in b₁ iff ex A being non empty ext-real-membered set st
( A in F & a = inf A ) )

proof end;

uniqueness
for b₁, b₂ being ext-real-membered set st ( for a being ext-real number holds
( a in b₁ 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 b₂ iff ex A being non empty ext-real-membered set st
( A in F & a = inf A ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def20 defines INF SUPINF_1:def 20 :
for F being bool_DOMAIN of ExtREAL
for b₂ being ext-real-membered set holds
( b₂ = INF F iff for a being ext-real number holds
( a in b₂ 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;