:: Infimum and Supremum of the Set of Real Numbers. Measure Theory
:: by J\'ozef Bia{\l}as
::
:: Received September 27, 1990
:: Copyright (c) 1990-2012 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;

::
:: Set of UpperBound and set of LowerBound of X being a subset of ExtREAL
::
definition
let X be ext-real-membered set ;
func SetMajorant X -> ext-real-membered set means :Def1: :: SUPINF_1:def 1
 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 Def1 defines SetMajorant SUPINF_1:def 1 :
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
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 :Def2: :: SUPINF_1:def 2
 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 Def2 defines SetMinorant SUPINF_1:def 2 :
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:2
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;

::
:: sup X, inf X least upper bound and greatest lower bound of set X
::
theorem :: SUPINF_1:3
for X being non empty ext-real-membered set holds
( sup X = inf (SetMajorant X) & inf X = sup (SetMinorant X) )
proof end;

registration
let X be non empty set ;
cluster non empty with_non-empty_elements for 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;
func SUP F -> ext-real-membered set means :Def3: :: SUPINF_1:def 3
 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 Def3 defines SUP SUPINF_1:def 3 :
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 Th4: :: SUPINF_1:4
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 Th5: :: SUPINF_1:5
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:6
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 :Def4: :: SUPINF_1:def 4
 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 Def4 defines INF SUPINF_1:def 4 :
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 Th7: :: SUPINF_1:7
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 Th8: :: SUPINF_1:8
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:9
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;