:: 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 )
proofend;
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
proofend;
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
proofend;
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
proofend;

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

::
:: 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) )
proofend;

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

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

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

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

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

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