:: SUPINF_1 semantic presentation

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
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
defpred S1[ ext-real number ] means $1 is UpperBound of X;
consider Y being ext-real-membered set  such that
A1: for x being ext-real number holds
( x in Y iff S1[x] ) from MEMBERED:sch_2();
take  Y ; ::_thesis: for x being ext-real number holds
( x in Y iff x is UpperBound of X )
thus  for x being ext-real number holds
( x in Y iff x is UpperBound of X ) by A1; ::_thesis: verum
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
let Y1, Y2 be ext-real-membered set ; ::_thesis: ( ( for x being ext-real number holds
( x in Y1 iff x is UpperBound of X ) ) & ( for x being ext-real number holds
( x in Y2 iff x is UpperBound of X ) ) implies Y1 = Y2 )
assume that
A2: for x being ext-real number holds
( x in Y1 iff x is UpperBound of X ) and
A3: for x being ext-real number holds
( x in Y2 iff x is UpperBound of X ) ; ::_thesis: Y1 = Y2
let x be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not x in Y1 or x in Y2 ) & ( not x in Y2 or x in Y1 ) )
 ( x in Y1 iff x is UpperBound of X ) by A2;
hence  ( ( not x in Y1 or x in Y2 ) & ( not x in Y2 or x in Y1 ) ) by A3; ::_thesis: verum
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
set x = the UpperBound of X;
 the UpperBound of X in SetMajorant X by Def1;
hence  not SetMajorant X is empty ; ::_thesis: verum
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
let X, Y be ext-real-membered set ; ::_thesis: ( X c= Y implies for x being ext-real number st x in SetMajorant Y holds
x in SetMajorant X )
assume A1: X c= Y ; ::_thesis: for x being ext-real number st x in SetMajorant Y holds
x in SetMajorant X
let x be ext-real number ; ::_thesis: ( x in SetMajorant Y implies x in SetMajorant X )
assume  x in SetMajorant Y ; ::_thesis: x in SetMajorant X
then  x is UpperBound of Y by Def1;
then  x is UpperBound of X by A1, XXREAL_2:6;
hence  x in SetMajorant X by Def1; ::_thesis: verum
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
defpred S1[ ext-real number ] means $1 is LowerBound of X;
consider Y being ext-real-membered set  such that
A1: for x being ext-real number holds
( x in Y iff S1[x] ) from MEMBERED:sch_2();
take  Y ; ::_thesis: for x being ext-real number holds
( x in Y iff x is LowerBound of X )
thus  for x being ext-real number holds
( x in Y iff x is LowerBound of X ) by A1; ::_thesis: verum
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
let Y1, Y2 be ext-real-membered set ; ::_thesis: ( ( for x being ext-real number holds
( x in Y1 iff x is LowerBound of X ) ) & ( for x being ext-real number holds
( x in Y2 iff x is LowerBound of X ) ) implies Y1 = Y2 )
assume that
A2: for x being ext-real number holds
( x in Y1 iff x is LowerBound of X ) and
A3: for x being ext-real number holds
( x in Y2 iff x is LowerBound of X ) ; ::_thesis: Y1 = Y2
let x be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not x in Y1 or x in Y2 ) & ( not x in Y2 or x in Y1 ) )
 ( x in Y1 iff x is LowerBound of X ) by A2;
hence  ( ( not x in Y1 or x in Y2 ) & ( not x in Y2 or x in Y1 ) ) by A3; ::_thesis: verum
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
set x = the LowerBound of X;
 the LowerBound of X in SetMinorant X by Def2;
hence  not SetMinorant X is empty ; ::_thesis: verum
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
let X, Y be ext-real-membered set ; ::_thesis: ( X c= Y implies for x being ext-real number st x in SetMinorant Y holds
x in SetMinorant X )
assume A1: X c= Y ; ::_thesis: for x being ext-real number st x in SetMinorant Y holds
x in SetMinorant X
let x be ext-real number ; ::_thesis: ( x in SetMinorant Y implies x in SetMinorant X )
assume  x in SetMinorant Y ; ::_thesis: x in SetMinorant X
then  x is LowerBound of Y by Def2;
then  x is LowerBound of X by A1, XXREAL_2:5;
hence  x in SetMinorant X by Def2; ::_thesis: verum
end;

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
let X be non empty ext-real-membered set ; ::_thesis: ( sup X = inf (SetMajorant X) & inf X = sup (SetMinorant X) )
 for y being ext-real number st y in SetMajorant X holds
sup X <= y
proof
let y be ext-real number ; ::_thesis: ( y in SetMajorant X implies sup X <= y )
assume  y in SetMajorant X ; ::_thesis: sup X <= y
then  y is UpperBound of X by Def1;
hence  sup X <= y by XXREAL_2:def_3; ::_thesis: verum
end;
then A1: sup X is LowerBound of SetMajorant X by XXREAL_2:def_2;
 inf X is LowerBound of X by XXREAL_2:def_4;
then A2: inf X in SetMinorant X by Def2;
 for y being ext-real number st y in SetMinorant X holds
y <= inf X
proof
let y be ext-real number ; ::_thesis: ( y in SetMinorant X implies y <= inf X )
assume  y in SetMinorant X ; ::_thesis: y <= inf X
then  y is LowerBound of X by Def2;
hence  y <= inf X by XXREAL_2:def_4; ::_thesis: verum
end;
then A3: inf X is UpperBound of SetMinorant X by XXREAL_2:def_1;
 sup X is UpperBound of X by XXREAL_2:def_3;
then  sup X in SetMajorant X by Def1;
hence  ( sup X = inf (SetMajorant X) & inf X = sup (SetMinorant X) ) by A1, A2, A3, XXREAL_2:55, XXREAL_2:56; ::_thesis: verum
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
take  {([#] X)} ; ::_thesis: ( not {([#] X)} is empty & {([#] X)} is with_non-empty_elements )
thus  not {([#] X)} is empty ; ::_thesis: {([#] X)} is with_non-empty_elements
assume  {} in {([#] X)} ; :: according to SETFAM_1:def_8 ::_thesis: contradiction
hence  contradiction by TARSKI:def_1; ::_thesis: verum
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
defpred S1[ ext-real number ] means  ex A being non empty ext-real-membered set st
( A in F & $1 = sup A );
consider S being ext-real-membered set  such that
A1: for a being ext-real number holds
( a in S iff S1[a] ) from MEMBERED:sch_2();
reconsider S = S as ext-real-membered set ;
take  S ; ::_thesis: for a being ext-real number holds
( a in S iff ex A being non empty ext-real-membered set st
( A in F & a = sup A ) )
thus  for a being ext-real number holds
( a in S iff ex A being non empty ext-real-membered set st
( A in F & a = sup A ) ) by A1; ::_thesis: verum
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
let S1, S2 be ext-real-membered set ; ::_thesis: ( ( for a being ext-real number holds
( a in S1 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 S2 iff ex A being non empty ext-real-membered set st
( A in F & a = sup A ) ) ) implies S1 = S2 )
assume that
A2: for a being ext-real number holds
( a in S1 iff ex A being non empty ext-real-membered set st
( A in F & a = sup A ) ) and
A3: for a being ext-real number holds
( a in S2 iff ex A being non empty ext-real-membered set st
( A in F & a = sup A ) ) ; ::_thesis: S1 = S2
let a be ext-real number ; :: according to MEMBERED:def_14 ::_thesis: ( ( not a in S1 or a in S2 ) & ( not a in S2 or a in S1 ) )
hereby  ::_thesis: ( not a in S2 or a in S1 )
assume  a in S1 ; ::_thesis: a in S2
then  ex A being non empty ext-real-membered set st
( A in F & a = sup A ) by A2;
hence  a in S2 by A3; ::_thesis: verum
end;
assume  a in S2 ; ::_thesis: a in S1
then  ex A being non empty ext-real-membered set st
( A in F & a = sup A ) by A3;
hence  a in S1 by A2; ::_thesis: verum
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
set A = the Element of F;
reconsider A = the Element of F as non empty ext-real-membered set by SETFAM_1:def_8;
 sup A = sup A ;
hence  not SUP F is empty by Def3; ::_thesis: verum
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
let F be bool_DOMAIN of ExtREAL; ::_thesis: for S being non empty ext-real-membered number st S = union F holds
sup S is UpperBound of SUP F
let S be non empty ext-real-membered set ; ::_thesis: ( S = union F implies sup S is UpperBound of SUP F )
assume A1: S = union F ; ::_thesis: sup S is UpperBound of SUP F
 for x being ext-real number st x in SUP F holds
x <= sup S
proof
let x be ext-real number ; ::_thesis: ( x in SUP F implies x <= sup S )
assume  x in SUP F ; ::_thesis: x <= sup S
then consider A being non empty ext-real-membered set  such that
A2: A in F and
A3: x = sup A by Def3;
 A c= S
proof
let a be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not a in A or a in S )
assume  a in A ; ::_thesis: a in S
hence  a in S by A1, A2, TARSKI:def_4; ::_thesis: verum
end;
hence  x <= sup S by A3, XXREAL_2:59; ::_thesis: verum
end;
hence  sup S is UpperBound of SUP F by XXREAL_2:def_1; ::_thesis: verum
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
let F be bool_DOMAIN of ExtREAL; ::_thesis: for S being ext-real-membered set st S = union F holds
sup (SUP F) is UpperBound of S
let S be ext-real-membered set ; ::_thesis: ( S = union F implies sup (SUP F) is UpperBound of S )
assume A1: S = union F ; ::_thesis: sup (SUP F) is UpperBound of S
 for x being ext-real number st x in S holds
x <= sup (SUP F)
proof
let x be ext-real number ; ::_thesis: ( x in S implies x <= sup (SUP F) )
assume  x in S ; ::_thesis: x <= sup (SUP F)
then consider Z being set  such that
A2: x in Z and
A3: Z in F by A1, TARSKI:def_4;
reconsider Z = Z as non empty ext-real-membered set by A2, A3;
consider a being set  such that
A4: a = sup Z ;
reconsider a = a as ext-real number by A4;
 ( sup Z is UpperBound of Z & a in SUP F ) by A3, A4, Def3, XXREAL_2:def_3;
hence  x <= sup (SUP F) by A2, A4, XXREAL_2:61, XXREAL_2:def_1; ::_thesis: verum
end;
hence  sup (SUP F) is UpperBound of S by XXREAL_2:def_1; ::_thesis: verum
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
let F be bool_DOMAIN of ExtREAL; ::_thesis: for S being non empty ext-real-membered set st S = union F holds
sup S = sup (SUP F)
let S be non empty ext-real-membered set ; ::_thesis: ( S = union F implies sup S = sup (SUP F) )
set a = sup S;
set b = sup (SUP F);
assume A1: S = union F ; ::_thesis: sup S = sup (SUP F)
then  sup S is UpperBound of SUP F by Th4;
then A2: sup (SUP F) <= sup S by XXREAL_2:def_3;
 sup (SUP F) is UpperBound of S by A1, Th5;
then  sup S <= sup (SUP F) by XXREAL_2:def_3;
hence  sup S = sup (SUP F) by A2, XXREAL_0:1; ::_thesis: verum
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
set A = the Element of F;
defpred S1[ ext-real number ] means  ex A being non empty ext-real-membered set st
( A in F & $1 = inf A );
reconsider A = the Element of F as non empty ext-real-membered set by SETFAM_1:def_8;
consider S being ext-real-membered set  such that
A1: for a being ext-real number holds
( a in S iff S1[a] ) from MEMBERED:sch_2();
 inf A = inf A ;
then reconsider S = S as non empty ext-real-membered set by A1;
take  S ; ::_thesis: for a being ext-real number holds
( a in S iff ex A being non empty ext-real-membered set st
( A in F & a = inf A ) )
thus  for a being ext-real number holds
( a in S iff ex A being non empty ext-real-membered set st
( A in F & a = inf A ) ) by A1; ::_thesis: verum
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
let S1, S2 be ext-real-membered set ; ::_thesis: ( ( for a being ext-real number holds
( a in S1 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 S2 iff ex A being non empty ext-real-membered set st
( A in F & a = inf A ) ) ) implies S1 = S2 )
assume that
A2: for a being ext-real number holds
( a in S1 iff ex A being non empty ext-real-membered set st
( A in F & a = inf A ) ) and
A3: for a being ext-real number holds
( a in S2 iff ex A being non empty ext-real-membered set st
( A in F & a = inf A ) ) ; ::_thesis: S1 = S2
 for a being set holds
( a in S1 iff a in S2 )
proof
let a be set ; ::_thesis: ( a in S1 iff a in S2 )
hereby  ::_thesis: ( a in S2 implies a in S1 )
assume A4: a in S1 ; ::_thesis: a in S2
then reconsider a9 = a as ext-real number ;
 ex A being non empty ext-real-membered set st
( A in F & a9 = inf A ) by A2, A4;
hence  a in S2 by A3; ::_thesis: verum
end;
assume A5: a in S2 ; ::_thesis: a in S1
then reconsider a = a as ext-real number ;
 ex A being non empty ext-real-membered set st
( A in F & a = inf A ) by A3, A5;
hence  a in S1 by A2; ::_thesis: verum
end;
hence  S1 = S2 by TARSKI:1; ::_thesis: verum
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
set A = the Element of F;
reconsider A = the Element of F as non empty ext-real-membered set by SETFAM_1:def_8;
 inf A = inf A ;
hence  not INF F is empty by Def4; ::_thesis: verum
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
let F be bool_DOMAIN of ExtREAL; ::_thesis: for S being non empty ext-real-membered set st S = union F holds
inf S is LowerBound of INF F
let S be non empty ext-real-membered set ; ::_thesis: ( S = union F implies inf S is LowerBound of INF F )
assume A1: S = union F ; ::_thesis: inf S is LowerBound of INF F
 for x being ext-real number st x in INF F holds
inf S <= x
proof
let x be ext-real number ; ::_thesis: ( x in INF F implies inf S <= x )
assume  x in INF F ; ::_thesis: inf S <= x
then consider A being non empty ext-real-membered set  such that
A2: A in F and
A3: x = inf A by Def4;
 A c= S
proof
let a be ext-real number ; :: according to MEMBERED:def_8 ::_thesis: ( not a in A or a in S )
assume  a in A ; ::_thesis: a in S
hence  a in S by A1, A2, TARSKI:def_4; ::_thesis: verum
end;
hence  inf S <= x by A3, XXREAL_2:60; ::_thesis: verum
end;
hence  inf S is LowerBound of INF F by XXREAL_2:def_2; ::_thesis: verum
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
let F be bool_DOMAIN of ExtREAL; ::_thesis: for S being ext-real-membered set st S = union F holds
inf (INF F) is LowerBound of S
let S be ext-real-membered set ; ::_thesis: ( S = union F implies inf (INF F) is LowerBound of S )
assume A1: S = union F ; ::_thesis: inf (INF F) is LowerBound of S
 for x being ext-real number st x in S holds
inf (INF F) <= x
proof
let x be ext-real number ; ::_thesis: ( x in S implies inf (INF F) <= x )
assume  x in S ; ::_thesis: inf (INF F) <= x
then consider Z being set  such that
A2: x in Z and
A3: Z in F by A1, TARSKI:def_4;
reconsider Z = Z as non empty ext-real-membered set by A2, A3;
consider a being set  such that
A4: a = inf Z ;
reconsider a = a as ext-real number by A4;
 ( inf Z is LowerBound of Z & a in INF F ) by A3, A4, Def4, XXREAL_2:def_4;
hence  inf (INF F) <= x by A2, A4, XXREAL_2:62, XXREAL_2:def_2; ::_thesis: verum
end;
hence  inf (INF F) is LowerBound of S by XXREAL_2:def_2; ::_thesis: verum
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
let F be bool_DOMAIN of ExtREAL; ::_thesis: for S being non empty ext-real-membered set st S = union F holds
inf S = inf (INF F)
let S be non empty ext-real-membered set ; ::_thesis: ( S = union F implies inf S = inf (INF F) )
set a = inf S;
set b = inf (INF F);
assume A1: S = union F ; ::_thesis: inf S = inf (INF F)
then  inf S is LowerBound of INF F by Th7;
then A2: inf S <= inf (INF F) by XXREAL_2:def_4;
 inf (INF F) is LowerBound of S by A1, Th8;
then  inf (INF F) <= inf S by XXREAL_2:def_4;
hence  inf S = inf (INF F) by A2, XXREAL_0:1; ::_thesis: verum
end;