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

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 ExtReal holds
( x in it iff x is UpperBound of X );

existence
ex b₁ being ext-real-membered set st
for x being ExtReal 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 ExtReal holds
( x in b₁ iff x is UpperBound of X ) ) & ( for x being ExtReal holds
( x in b₂ iff x is UpperBound of X ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines SetMajorant SUPINF_1:def 1 :
for X, b₂ being ext-real-membered set holds
( b₂ = SetMajorant X iff for x being ExtReal 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

for X, Y being ext-real-membered set st X c= Y holds
for x being ExtReal 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 ExtReal holds
( x in it iff x is LowerBound of X );

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

proof end;

end;

:: deftheorem Def2 defines SetMinorant SUPINF_1:def 2 :
for X, b₂ being ext-real-membered set holds
( b₂ = SetMinorant X iff for x being ExtReal 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:2

for X, Y being ext-real-membered set st X c= Y holds
for x being ExtReal 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 bool (bool 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;

func SUP F -> ext-real-membered set means :Def3: :: SUPINF_1:def 3
for a being ExtReal 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 ExtReal 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 ExtReal holds
( a in b₁ iff ex A being non empty ext-real-membered set st
( A in F & a = sup A ) ) ) & ( for a being ExtReal 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 Def3 defines SUP SUPINF_1:def 3 :
for F being bool_DOMAIN of ExtREAL
for b₂ being ext-real-membered set holds
( b₂ = SUP F iff for a being ExtReal 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 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 ExtReal 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 ExtReal 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 ExtReal holds
( a in b₁ iff ex A being non empty ext-real-membered set st
( A in F & a = inf A ) ) ) & ( for a being ExtReal 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 Def4 defines INF SUPINF_1:def 4 :
for F being bool_DOMAIN of ExtREAL
for b₂ being ext-real-membered set holds
( b₂ = INF F iff for a being ExtReal 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 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;