:: by J\'ozef Bia{\l}as

::

:: Received September 27, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

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

definition

let X be ext-real-membered set ;

ex b_{1} being ext-real-membered set st

for x being ext-real number holds

( x in b_{1} iff x is UpperBound of X )

for b_{1}, b_{2} being ext-real-membered set st ( for x being ext-real number holds

( x in b_{1} iff x is UpperBound of X ) ) & ( for x being ext-real number holds

( x in b_{2} iff x is UpperBound of X ) ) holds

b_{1} = b_{2}

end;
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 for x being ext-real number holds

( x in it iff x is UpperBound of X );

ex b

for x being ext-real number holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def1 defines SetMajorant SUPINF_1:def 1 :

for X, b_{2} being ext-real-membered set holds

( b_{2} = SetMajorant X iff for x being ext-real number holds

( x in b_{2} iff x is UpperBound of X ) );

for X, b

( b

( x in b

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

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 ;

ex b_{1} being ext-real-membered set st

for x being ext-real number holds

( x in b_{1} iff x is LowerBound of X )

for b_{1}, b_{2} being ext-real-membered set st ( for x being ext-real number holds

( x in b_{1} iff x is LowerBound of X ) ) & ( for x being ext-real number holds

( x in b_{2} iff x is LowerBound of X ) ) holds

b_{1} = b_{2}

end;
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 for x being ext-real number holds

( x in it iff x is LowerBound of X );

ex b

for x being ext-real number holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def2 defines SetMinorant SUPINF_1:def 2 :

for X, b_{2} being ext-real-membered set holds

( b_{2} = SetMinorant X iff for x being ext-real number holds

( x in b_{2} iff x is LowerBound of X ) );

for X, b

( b

( x in b

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

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

::

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

( sup X = inf (SetMajorant X) & inf X = sup (SetMinorant X) )

proof end;

registration

let X be non empty set ;

existence

ex b_{1} being Subset-Family of X st

( not b_{1} is empty & b_{1} is with_non-empty_elements )

end;
existence

ex b

( not b

proof 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;
mode bool_DOMAIN of X is non empty with_non-empty_elements Subset-Family of X;

definition

let F be bool_DOMAIN of ExtREAL;

ex b_{1} being ext-real-membered set st

for a being ext-real number holds

( a in b_{1} iff ex A being non empty ext-real-membered set st

( A in F & a = sup A ) )

for b_{1}, b_{2} being ext-real-membered set st ( for a being ext-real number holds

( a in b_{1} 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_{2} iff ex A being non empty ext-real-membered set st

( A in F & a = sup A ) ) ) holds

b_{1} = b_{2}

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

ex b

for a being ext-real number holds

( a in b

( A in F & a = sup A ) )

proof end;

uniqueness for b

( a in b

( A in F & a = sup A ) ) ) & ( for a being ext-real number holds

( a in b

( A in F & a = sup A ) ) ) holds

b

proof end;

:: deftheorem Def3 defines SUP SUPINF_1:def 3 :

for F being bool_DOMAIN of ExtREAL

for b_{2} being ext-real-membered set holds

( b_{2} = SUP F iff for a being ext-real number holds

( a in b_{2} iff ex A being non empty ext-real-membered set st

( A in F & a = sup A ) ) );

for F being bool_DOMAIN of ExtREAL

for b

( b

( a in b

( A in F & a = sup A ) ) );

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

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

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)

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;

ex b_{1} being ext-real-membered set st

for a being ext-real number holds

( a in b_{1} iff ex A being non empty ext-real-membered set st

( A in F & a = inf A ) )

for b_{1}, b_{2} being ext-real-membered set st ( for a being ext-real number holds

( a in b_{1} 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_{2} iff ex A being non empty ext-real-membered set st

( A in F & a = inf A ) ) ) holds

b_{1} = b_{2}

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

ex b

for a being ext-real number holds

( a in b

( A in F & a = inf A ) )

proof end;

uniqueness for b

( a in b

( A in F & a = inf A ) ) ) & ( for a being ext-real number holds

( a in b

( A in F & a = inf A ) ) ) holds

b

proof end;

:: deftheorem Def4 defines INF SUPINF_1:def 4 :

for F being bool_DOMAIN of ExtREAL

for b_{2} being ext-real-membered set holds

( b_{2} = INF F iff for a being ext-real number holds

( a in b_{2} iff ex A being non empty ext-real-membered set st

( A in F & a = inf A ) ) );

for F being bool_DOMAIN of ExtREAL

for b

( b

( a in b

( A in F & a = inf A ) ) );

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

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

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)

for S being non empty ext-real-membered set st S = union F holds

inf S = inf (INF F)

proof end;

:: Set of UpperBound and set of LowerBound of X being a subset of ExtREAL

::