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