:: XXREAL_0 semantic presentation
begin
definition
let x be set ;
attrx is ext-real means :Def1: :: XXREAL_0:def 1
x in ExtREAL ;
end;
:: deftheorem Def1 defines ext-real XXREAL_0:def_1_:_
for x being set holds
( x is ext-real iff x in ExtREAL );
registration
cluster ext-real for set ;
existence
ex b1 being number st b1 is ext-real
proof
take 0 ; ::_thesis: 0 is ext-real
thus 0 in ExtREAL by XBOOLE_0:def_3; :: according to XXREAL_0:def_1 ::_thesis: verum
end;
cluster -> ext-real for Element of ExtREAL ;
coherence
for b1 being Element of ExtREAL holds b1 is ext-real by Def1;
end;
registration
ext-real number ex b1 being set st
for b2 being ext-real number holds b2 in b1
proof
take ExtREAL ; ::_thesis: for b1 being ext-real number holds b1 in ExtREAL
thus for b1 being ext-real number holds b1 in ExtREAL by Def1; ::_thesis: verum
end;
end;
definition
func +infty -> set equals :: XXREAL_0:def 2
REAL ;
coherence
REAL is set ;
func -infty -> set equals :: XXREAL_0:def 3
[0,REAL];
coherence
[0,REAL] is set ;
end;
:: deftheorem defines +infty XXREAL_0:def_2_:_
+infty = REAL ;
:: deftheorem defines -infty XXREAL_0:def_3_:_
-infty = [0,REAL];
definition
redefine func ExtREAL equals :: XXREAL_0:def 4
REAL \/ {+infty,-infty};
compatibility
for b1 being set holds
( b1 = ExtREAL iff b1 = REAL \/ {+infty,-infty} ) ;
end;
:: deftheorem defines ExtREAL XXREAL_0:def_4_:_
ExtREAL = REAL \/ {+infty,-infty};
registration
cluster +infty -> ext-real ;
coherence
+infty is ext-real
proof
+infty in {REAL,[0,REAL]} by TARSKI:def_2;
then +infty in ExtREAL by XBOOLE_0:def_3;
hence +infty is ext-real ; ::_thesis: verum
end;
cluster -infty -> ext-real ;
coherence
-infty is ext-real
proof
-infty in {REAL,[0,REAL]} by TARSKI:def_2;
then -infty in ExtREAL by XBOOLE_0:def_3;
hence -infty is ext-real ; ::_thesis: verum
end;
end;
definition
let x, y be ext-real number ;
predx <= y means :Def5: :: XXREAL_0:def 5
ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & x9 <=' y9 ) if ( x in REAL+ & y in REAL+ )
ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & y9 <=' x9 ) if ( x in [:{0},REAL+:] & y in [:{0},REAL+:] )
otherwise ( ( y in REAL+ & x in [:{0},REAL+:] ) or x = -infty or y = +infty );
consistency
( x in REAL+ & y in REAL+ & x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & x9 <=' y9 ) iff ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & y9 <=' x9 ) ) ) by ARYTM_0:5, XBOOLE_0:3;
reflexivity
for x being ext-real number holds
( ( x in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( x = x9 & x = y9 & x9 <=' y9 ) ) & ( x in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( x = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not x in REAL+ or not x in REAL+ ) & ( not x in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & x in [:{0},REAL+:] ) & not x = -infty implies x = +infty ) )
proof
let x be ext-real number ; ::_thesis: ( ( x in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( x = x9 & x = y9 & x9 <=' y9 ) ) & ( x in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( x = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not x in REAL+ or not x in REAL+ ) & ( not x in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & x in [:{0},REAL+:] ) & not x = -infty implies x = +infty ) )
assume A1: ( ( x in REAL+ & x in REAL+ & ( for x9, y9 being Element of REAL+ holds
( not x = x9 or not x = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & x in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not x = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not x in REAL+ ) & ( not x in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not x = +infty ) ) ; ::_thesis: contradiction
x in ExtREAL by Def1;
then A2: ( x in (REAL+ \/ [:{0},REAL+:]) \ {[0,0]} or x in {+infty,-infty} ) by XBOOLE_0:def_3;
percases ( ( x in REAL+ & ( for x9, y9 being Element of REAL+ holds
( not x = x9 or not x = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not x = [0,y9] or not y9 <=' x9 ) ) ) or ( not x in REAL+ & not x in [:{0},REAL+:] & not ( x in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not x = +infty ) ) by A1;
supposethat A3: x in REAL+ and
A4: for x9, y9 being Element of REAL+ holds
( not x = x9 or not x = y9 or not x9 <=' y9 ) ; ::_thesis: contradiction
reconsider x9 = x as Element of REAL+ by A3;
not x9 <=' x9 by A4;
hence contradiction ; ::_thesis: verum
end;
supposethat A5: x in [:{0},REAL+:] and
A6: for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not x = [0,y9] or not y9 <=' x9 ) ; ::_thesis: contradiction
consider z, x9 being set such that
A7: z in {0} and
A8: x9 in REAL+ and
A9: x = [z,x9] by A5, ZFMISC_1:84;
reconsider x9 = x9 as Element of REAL+ by A8;
x = [0,x9] by A7, A9, TARSKI:def_1;
then not x9 <=' x9 by A6;
hence contradiction ; ::_thesis: verum
end;
suppose ( not x in REAL+ & not x in [:{0},REAL+:] & not ( x in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not x = +infty ) ; ::_thesis: contradiction
hence contradiction by A2, TARSKI:def_2, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
connectedness
for x, y being ext-real number st ( ( x in REAL+ & y in REAL+ & ( for x9, y9 being Element of REAL+ holds
( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & not ( y in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not y = +infty ) ) holds
( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )
proof
let x, y be ext-real number ; ::_thesis: ( ( ( x in REAL+ & y in REAL+ & ( for x9, y9 being Element of REAL+ holds
( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & not ( y in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not y = +infty ) ) implies ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) ) )
assume A10: ( ( x in REAL+ & y in REAL+ & ( for x9, y9 being Element of REAL+ holds
( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & not ( y in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not y = +infty ) ) ; ::_thesis: ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )
x in ExtREAL by Def1;
then A11: ( x in (REAL+ \/ [:{0},REAL+:]) \ {[0,0]} or x in {+infty,-infty} ) by XBOOLE_0:def_3;
y in ExtREAL by Def1;
then A12: ( y in (REAL+ \/ [:{0},REAL+:]) \ {[0,0]} or y in {+infty,-infty} ) by XBOOLE_0:def_3;
percases ( ( x in REAL+ & y in REAL+ & ( for x9, y9 being Element of REAL+ holds
( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & not ( y in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not y = +infty ) ) by A10;
supposethat A13: ( x in REAL+ & y in REAL+ ) and
A14: for x9, y9 being Element of REAL+ holds
( not x = x9 or not y = y9 or not x9 <=' y9 ) ; ::_thesis: ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )
hereby ::_thesis: ( ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )
assume ( y in REAL+ & x in REAL+ ) ; ::_thesis: ex y9, x9 being Element of REAL+ st
( y = y9 & x = x9 & y9 <=' x9 )
then reconsider x9 = x, y9 = y as Element of REAL+ ;
take y9 = y9; ::_thesis: ex x9 being Element of REAL+ st
( y = y9 & x = x9 & y9 <=' x9 )
take x9 = x9; ::_thesis: ( y = y9 & x = x9 & y9 <=' x9 )
thus ( y = y9 & x = x9 ) ; ::_thesis: y9 <=' x9
thus y9 <=' x9 by A14; ::_thesis: verum
end;
thus ( ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) ) by A13, ARYTM_0:5, XBOOLE_0:3; ::_thesis: verum
end;
supposethat A15: ( x in [:{0},REAL+:] & y in [:{0},REAL+:] ) and
A16: for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ; ::_thesis: ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )
now__::_thesis:_(_y_in_[:{0},REAL+:]_&_x_in_[:{0},REAL+:]_implies_ex_y9,_x9_being_Element_of_REAL+_st_
(_y_=_[0,y9]_&_x_=_[0,x9]_&_x9_<='_y9_)_)
assume y in [:{0},REAL+:] ; ::_thesis: ( x in [:{0},REAL+:] implies ex y9, x9 being Element of REAL+ st
( y = [0,y9] & x = [0,x9] & x9 <=' y9 ) )
then consider z, y9 being set such that
A17: z in {0} and
A18: y9 in REAL+ and
A19: y = [z,y9] by ZFMISC_1:84;
A20: z = 0 by A17, TARSKI:def_1;
assume x in [:{0},REAL+:] ; ::_thesis: ex y9, x9 being Element of REAL+ st
( y = [0,y9] & x = [0,x9] & x9 <=' y9 )
then consider z, x9 being set such that
A21: z in {0} and
A22: x9 in REAL+ and
A23: x = [z,x9] by ZFMISC_1:84;
reconsider x9 = x9, y9 = y9 as Element of REAL+ by A18, A22;
take y9 = y9; ::_thesis: ex x9 being Element of REAL+ st
( y = [0,y9] & x = [0,x9] & x9 <=' y9 )
take x9 = x9; ::_thesis: ( y = [0,y9] & x = [0,x9] & x9 <=' y9 )
thus ( y = [0,y9] & x = [0,x9] ) by A17, A19, A21, A23, TARSKI:def_1; ::_thesis: x9 <=' y9
z = 0 by A21, TARSKI:def_1;
hence x9 <=' y9 by A16, A19, A20, A23; ::_thesis: verum
end;
hence ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) ) by A15, ARYTM_0:5, XBOOLE_0:3; ::_thesis: verum
end;
suppose ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) & not ( y in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not y = +infty ) ; ::_thesis: ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )
hence ( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) ) by A11, A12, TARSKI:def_2, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
end;
:: deftheorem Def5 defines <= XXREAL_0:def_5_:_
for x, y being ext-real number holds
( ( x in REAL+ & y in REAL+ implies ( x <= y iff ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & x9 <=' y9 ) ) ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( x <= y iff ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & y9 <=' x9 ) ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) implies ( x <= y iff ( ( y in REAL+ & x in [:{0},REAL+:] ) or x = -infty or y = +infty ) ) ) );
notation
let a, b be ext-real number ;
synonym b >= a for a <= b;
antonym b < a for a <= b;
antonym a > b for a <= b;
end;
Lm1: +infty <> [0,0]
proof
assume +infty = [0,0] ; ::_thesis: contradiction
then +infty = {{0},{0}} by ENUMSET1:29
.= {{0}} by ENUMSET1:29 ;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
Lm2: not +infty in REAL+
by ARYTM_0:1, ORDINAL1:5;
Lm3: not -infty in REAL+
proof
A1: ( {0,REAL} in -infty & REAL in {0,REAL} ) by TARSKI:def_2;
assume -infty in REAL+ ; ::_thesis: contradiction
hence contradiction by A1, ARYTM_0:1, XREGULAR:7; ::_thesis: verum
end;
Lm4: not +infty in [:{0},REAL+:]
proof
assume +infty in [:{0},REAL+:] ; ::_thesis: contradiction
then +infty in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def_3;
then +infty in REAL by Lm1, ZFMISC_1:56;
hence contradiction ; ::_thesis: verum
end;
Lm5: not -infty in [:{0},REAL+:]
proof
assume -infty in [:{0},REAL+:] ; ::_thesis: contradiction
then REAL in REAL+ by ZFMISC_1:87;
hence contradiction by ARYTM_0:1, ORDINAL1:5; ::_thesis: verum
end;
Lm6: -infty < +infty
proof
-infty <> +infty by TARSKI:def_2;
hence -infty < +infty by Def5, Lm3, Lm5; ::_thesis: verum
end;
theorem Th1: :: XXREAL_0:1
for a, b being ext-real number st a <= b & b <= a holds
a = b
proof
let a, b be ext-real number ; ::_thesis: ( a <= b & b <= a implies a = b )
assume that
A1: a <= b and
A2: b <= a ; ::_thesis: a = b
percases ( ( a in REAL+ & b in REAL+ ) or ( a in REAL+ & b in [:{0},REAL+:] ) or ( b in REAL+ & a in [:{0},REAL+:] ) or ( a in [:{0},REAL+:] & b in [:{0},REAL+:] ) or ( ( a = -infty or a = +infty ) & ( b = -infty or b = +infty ) ) or ( ( not a in REAL+ or not b in REAL+ ) & ( not a in [:{0},REAL+:] or not b in [:{0},REAL+:] ) & ( not b in REAL+ or not a in [:{0},REAL+:] ) & ( not a in REAL+ or not b in [:{0},REAL+:] ) ) ) ;
suppose ( a in REAL+ & b in REAL+ ) ; ::_thesis: a = b
then ( ex a9, b9 being Element of REAL+ st
( a = a9 & b = b9 & a9 <=' b9 ) & ex b99, a99 being Element of REAL+ st
( b = b99 & a = a99 & b99 <=' a99 ) ) by A1, A2, Def5;
hence a = b by ARYTM_1:4; ::_thesis: verum
end;
supposeA3: ( a in REAL+ & b in [:{0},REAL+:] ) ; ::_thesis: a = b
then ( not b in REAL+ & not a in [:{0},REAL+:] ) by ARYTM_0:5, XBOOLE_0:3;
hence a = b by A1, A3, Def5, Lm3, Lm4; ::_thesis: verum
end;
supposeA4: ( b in REAL+ & a in [:{0},REAL+:] ) ; ::_thesis: a = b
then ( not a in REAL+ & not b in [:{0},REAL+:] ) by ARYTM_0:5, XBOOLE_0:3;
hence a = b by A2, A4, Def5, Lm3, Lm4; ::_thesis: verum
end;
supposeA5: ( a in [:{0},REAL+:] & b in [:{0},REAL+:] ) ; ::_thesis: a = b
consider a9, b9 being Element of REAL+ such that
A6: ( a = [0,a9] & b = [0,b9] ) and
A7: b9 <=' a9 by A1, A5, Def5;
consider b99, a99 being Element of REAL+ such that
A8: ( b = [0,b99] & a = [0,a99] ) and
A9: a99 <=' b99 by A2, A5, Def5;
( a9 = a99 & b9 = b99 ) by A6, A8, XTUPLE_0:1;
hence a = b by A7, A8, A9, ARYTM_1:4; ::_thesis: verum
end;
suppose ( ( a = -infty or a = +infty ) & ( b = -infty or b = +infty ) ) ; ::_thesis: a = b
hence a = b by A1, A2, Lm6; ::_thesis: verum
end;
supposethat A10: ( ( not a in REAL+ or not b in REAL+ ) & ( not a in [:{0},REAL+:] or not b in [:{0},REAL+:] ) ) and
A11: ( not b in REAL+ or not a in [:{0},REAL+:] ) and
A12: ( not a in REAL+ or not b in [:{0},REAL+:] ) ; ::_thesis: a = b
( a = -infty or b = +infty ) by A1, A10, A11, Def5;
hence a = b by A2, A10, A12, Def5, Lm6; ::_thesis: verum
end;
end;
end;
Lm7: for a being ext-real number st -infty >= a holds
a = -infty
proof
let a be ext-real number ; ::_thesis: ( -infty >= a implies a = -infty )
a >= -infty by Def5, Lm3, Lm5;
hence ( -infty >= a implies a = -infty ) by Th1; ::_thesis: verum
end;
Lm8: for a being ext-real number st +infty <= a holds
a = +infty
proof
let a be ext-real number ; ::_thesis: ( +infty <= a implies a = +infty )
a <= +infty by Def5, Lm2, Lm4;
hence ( +infty <= a implies a = +infty ) by Th1; ::_thesis: verum
end;
theorem Th2: :: XXREAL_0:2
for a, b, c being ext-real number st a <= b & b <= c holds
a <= c
proof
let a, b, c be ext-real number ; ::_thesis: ( a <= b & b <= c implies a <= c )
assume that
A1: a <= b and
A2: b <= c ; ::_thesis: a <= c
percases ( ( a in REAL+ & b in REAL+ & c in REAL+ ) or ( a in REAL+ & b in [:{0},REAL+:] ) or ( b in REAL+ & c in [:{0},REAL+:] ) or ( a in [:{0},REAL+:] & c in REAL+ ) or ( a in [:{0},REAL+:] & b in [:{0},REAL+:] & c in [:{0},REAL+:] ) or ( ( not a in REAL+ or not b in REAL+ or not c in REAL+ ) & ( not a in REAL+ or not b in [:{0},REAL+:] ) & ( not b in REAL+ or not c in [:{0},REAL+:] ) & ( not a in [:{0},REAL+:] or not c in REAL+ ) & ( not a in [:{0},REAL+:] or not b in [:{0},REAL+:] or not c in [:{0},REAL+:] ) ) ) ;
supposethat A3: a in REAL+ and
A4: b in REAL+ and
A5: c in REAL+ ; ::_thesis: a <= c
consider b99, c9 being Element of REAL+ such that
A6: b = b99 and
A7: c = c9 and
A8: b99 <=' c9 by A2, A4, A5, Def5;
consider a9, b9 being Element of REAL+ such that
A9: a = a9 and
A10: ( b = b9 & a9 <=' b9 ) by A1, A3, A4, Def5;
a9 <=' c9 by A10, A6, A8, ARYTM_1:3;
hence a <= c by A5, A9, A7, Def5; ::_thesis: verum
end;
supposeA11: ( a in REAL+ & b in [:{0},REAL+:] ) ; ::_thesis: a <= c
then ( ( not a in REAL+ or not b in REAL+ ) & ( not a in [:{0},REAL+:] or not b in [:{0},REAL+:] ) ) by ARYTM_0:5, XBOOLE_0:3;
hence a <= c by A1, A11, Def5, Lm3, Lm4; ::_thesis: verum
end;
supposeA12: ( b in REAL+ & c in [:{0},REAL+:] ) ; ::_thesis: a <= c
then ( ( not c in REAL+ or not b in REAL+ ) & ( not c in [:{0},REAL+:] or not b in [:{0},REAL+:] ) ) by ARYTM_0:5, XBOOLE_0:3;
hence a <= c by A2, A12, Def5, Lm3, Lm4; ::_thesis: verum
end;
supposeA13: ( a in [:{0},REAL+:] & c in REAL+ ) ; ::_thesis: a <= c
( ( not a in REAL+ or not c in REAL+ ) & ( not a in [:{0},REAL+:] or not c in [:{0},REAL+:] ) ) by A13, ARYTM_0:5, XBOOLE_0:3;
hence a <= c by A13, Def5; ::_thesis: verum
end;
supposethat A14: a in [:{0},REAL+:] and
A15: b in [:{0},REAL+:] and
A16: c in [:{0},REAL+:] ; ::_thesis: a <= c
consider b99, c9 being Element of REAL+ such that
A17: b = [0,b99] and
A18: c = [0,c9] and
A19: c9 <=' b99 by A2, A15, A16, Def5;
consider a9, b9 being Element of REAL+ such that
A20: a = [0,a9] and
A21: b = [0,b9] and
A22: b9 <=' a9 by A1, A14, A15, Def5;
b9 = b99 by A21, A17, XTUPLE_0:1;
then c9 <=' a9 by A22, A19, ARYTM_1:3;
hence a <= c by A14, A16, A20, A18, Def5; ::_thesis: verum
end;
supposethat A23: ( not a in REAL+ or not b in REAL+ or not c in REAL+ ) and
A24: ( not a in REAL+ or not b in [:{0},REAL+:] ) and
A25: ( not b in REAL+ or not c in [:{0},REAL+:] ) and
A26: ( not a in [:{0},REAL+:] or not c in REAL+ ) and
A27: ( not a in [:{0},REAL+:] or not b in [:{0},REAL+:] or not c in [:{0},REAL+:] ) ; ::_thesis: a <= c
A28: ( b = +infty implies c = +infty ) by A2, Lm8;
A29: ( b = -infty implies a = -infty ) by A1, Lm7;
( a = -infty or b = +infty or b = -infty or c = +infty ) by A1, A2, A23, A25, A26, A27, Def5;
hence a <= c by A1, A2, A23, A24, A25, A27, A28, A29, Def5; ::_thesis: verum
end;
end;
end;
theorem :: XXREAL_0:3
for a being ext-real number holds a <= +infty by Def5, Lm2, Lm4;
theorem :: XXREAL_0:4
for a being ext-real number st +infty <= a holds
a = +infty by Lm8;
theorem :: XXREAL_0:5
for a being ext-real number holds a >= -infty by Def5, Lm3, Lm5;
theorem :: XXREAL_0:6
for a being ext-real number st -infty >= a holds
a = -infty by Lm7;
theorem :: XXREAL_0:7
-infty < +infty by Lm6;
theorem :: XXREAL_0:8
not +infty in REAL ;
Lm9: for a being ext-real number holds
( a in REAL or a = +infty or a = -infty )
proof
let a be ext-real number ; ::_thesis: ( a in REAL or a = +infty or a = -infty )
a in ExtREAL by Def1;
then ( a in REAL or a in {+infty,-infty} ) by XBOOLE_0:def_3;
hence ( a in REAL or a = +infty or a = -infty ) by TARSKI:def_2; ::_thesis: verum
end;
theorem Th9: :: XXREAL_0:9
for a being ext-real number st a in REAL holds
+infty > a
proof
let a be ext-real number ; ::_thesis: ( a in REAL implies +infty > a )
assume a in REAL ; ::_thesis: +infty > a
then A1: a <> +infty ;
+infty >= a by Def5, Lm2, Lm4;
hence +infty > a by A1, Th1; ::_thesis: verum
end;
theorem Th10: :: XXREAL_0:10
for a, b being ext-real number st a in REAL & b >= a & not b in REAL holds
b = +infty
proof
let a, b be ext-real number ; ::_thesis: ( a in REAL & b >= a & not b in REAL implies b = +infty )
assume that
A1: a in REAL and
A2: b >= a ; ::_thesis: ( b in REAL or b = +infty )
assume A3: not b in REAL ; ::_thesis: b = +infty
( b = -infty implies a = -infty ) by A2, Lm7;
hence b = +infty by A1, A3, Lm9; ::_thesis: verum
end;
theorem Th11: :: XXREAL_0:11
not -infty in REAL
proof
A1: ( {0,REAL} in {{0,REAL},{0}} & REAL in {0,REAL} ) by TARSKI:def_2;
assume -infty in REAL ; ::_thesis: contradiction
hence contradiction by A1, XREGULAR:7; ::_thesis: verum
end;
theorem Th12: :: XXREAL_0:12
for a being ext-real number st a in REAL holds
-infty < a
proof
let a be ext-real number ; ::_thesis: ( a in REAL implies -infty < a )
-infty <= a by Def5, Lm3, Lm5;
hence ( a in REAL implies -infty < a ) by Th1, Th11; ::_thesis: verum
end;
theorem Th13: :: XXREAL_0:13
for a, b being ext-real number st a in REAL & b <= a & not b in REAL holds
b = -infty
proof
let a, b be ext-real number ; ::_thesis: ( a in REAL & b <= a & not b in REAL implies b = -infty )
assume that
A1: a in REAL and
A2: b <= a ; ::_thesis: ( b in REAL or b = -infty )
assume A3: not b in REAL ; ::_thesis: b = -infty
( b = +infty implies a = +infty ) by A2, Lm8;
hence b = -infty by A1, A3, Lm9; ::_thesis: verum
end;
theorem :: XXREAL_0:14
for a being ext-real number holds
( a in REAL or a = +infty or a = -infty ) by Lm9;
begin
registration
cluster natural -> ext-real for set ;
coherence
for b1 being number st b1 is natural holds
b1 is ext-real
proof
let a be number ; ::_thesis: ( a is natural implies a is ext-real )
assume a is natural ; ::_thesis: a is ext-real
then a in NAT by ORDINAL1:def_12;
hence a in ExtREAL by XBOOLE_0:def_3; :: according to XXREAL_0:def_1 ::_thesis: verum
end;
end;
notation
let a be number ;
synonym zero a for empty ;
end;
definition
let a be ext-real number ;
attra is positive means :: XXREAL_0:def 6
a > 0 ;
attra is negative means :: XXREAL_0:def 7
a < 0 ;
redefine attr a is empty means :: XXREAL_0:def 8
a = 0 ;
compatibility
( a is zero iff a = 0 ) ;
end;
:: deftheorem defines positive XXREAL_0:def_6_:_
for a being ext-real number holds
( a is positive iff a > 0 );
:: deftheorem defines negative XXREAL_0:def_7_:_
for a being ext-real number holds
( a is negative iff a < 0 );
:: deftheorem defines zero XXREAL_0:def_8_:_
for a being ext-real number holds
( a is zero iff a = 0 );
registration
cluster ext-real positive -> non zero ext-real non negative for set ;
coherence
for b1 being ext-real number st b1 is positive holds
( not b1 is negative & not b1 is zero )
proof
let r be ext-real number ; ::_thesis: ( r is positive implies ( not r is negative & not r is zero ) )
assume r > 0 ; :: according to XXREAL_0:def_6 ::_thesis: ( not r is negative & not r is zero )
hence ( r >= 0 & r <> 0 ) ; :: according to XXREAL_0:def_7,XXREAL_0:def_8 ::_thesis: verum
end;
cluster non zero ext-real non negative -> ext-real positive for set ;
coherence
for b1 being ext-real number st not b1 is negative & not b1 is zero holds
b1 is positive
proof
let r be ext-real number ; ::_thesis: ( not r is negative & not r is zero implies r is positive )
assume ( r >= 0 & r <> 0 ) ; :: according to XXREAL_0:def_7,XXREAL_0:def_8 ::_thesis: r is positive
hence r > 0 by Th1; :: according to XXREAL_0:def_6 ::_thesis: verum
end;
cluster ext-real negative -> non zero ext-real non positive for set ;
coherence
for b1 being ext-real number st b1 is negative holds
( not b1 is positive & not b1 is zero )
proof
let r be ext-real number ; ::_thesis: ( r is negative implies ( not r is positive & not r is zero ) )
assume r < 0 ; :: according to XXREAL_0:def_7 ::_thesis: ( not r is positive & not r is zero )
hence ( r <= 0 & r <> {} ) ; :: according to XXREAL_0:def_6,XXREAL_0:def_8 ::_thesis: verum
end;
cluster non zero ext-real non positive -> ext-real negative for set ;
coherence
for b1 being ext-real number st not b1 is positive & not b1 is zero holds
b1 is negative ;
cluster zero ext-real -> ext-real non positive non negative for set ;
coherence
for b1 being ext-real number st b1 is zero holds
( not b1 is negative & not b1 is positive ) ;
cluster ext-real non positive non negative -> zero ext-real for set ;
coherence
for b1 being ext-real number st not b1 is negative & not b1 is positive holds
b1 is zero ;
end;
registration
cluster +infty -> positive ;
coherence
+infty is positive
proof
thus 0 < +infty by Th9; :: according to XXREAL_0:def_6 ::_thesis: verum
end;
cluster -infty -> negative ;
coherence
-infty is negative
proof
thus 0 > -infty by Th12; :: according to XXREAL_0:def_7 ::_thesis: verum
end;
end;
registration
cluster ext-real positive for set ;
existence
ex b1 being ext-real number st b1 is positive
proof
take +infty ; ::_thesis: +infty is positive
thus +infty is positive ; ::_thesis: verum
end;
cluster ext-real negative for set ;
existence
ex b1 being ext-real number st b1 is negative
proof
take -infty ; ::_thesis: -infty is negative
thus -infty is negative ; ::_thesis: verum
end;
cluster zero ext-real for set ;
existence
ex b1 being ext-real number st b1 is zero
proof
reconsider z = 0 as ext-real number ;
take z ; ::_thesis: z is zero
thus z = 0 ; :: according to XXREAL_0:def_8 ::_thesis: verum
end;
end;
begin
definition
let a, b be ext-real number ;
func min (a,b) -> set equals :Def9: :: XXREAL_0:def 9
a if a <= b
otherwise b;
correctness
coherence
( ( a <= b implies a is set ) & ( not a <= b implies b is set ) );
consistency
for b1 being set holds verum;
;
commutativity
for b1 being set
for a, b being ext-real number st ( a <= b implies b1 = a ) & ( not a <= b implies b1 = b ) holds
( ( b <= a implies b1 = b ) & ( not b <= a implies b1 = a ) ) by Th1;
idempotence
for a being ext-real number holds
( ( a <= a implies a = a ) & ( not a <= a implies a = a ) ) ;
func max (a,b) -> set equals :Def10: :: XXREAL_0:def 10
a if b <= a
otherwise b;
correctness
coherence
( ( b <= a implies a is set ) & ( not b <= a implies b is set ) );
consistency
for b1 being set holds verum;
;
commutativity
for b1 being set
for a, b being ext-real number st ( b <= a implies b1 = a ) & ( not b <= a implies b1 = b ) holds
( ( a <= b implies b1 = b ) & ( not a <= b implies b1 = a ) ) by Th1;
idempotence
for a being ext-real number holds
( ( a <= a implies a = a ) & ( not a <= a implies a = a ) ) ;
end;
:: deftheorem Def9 defines min XXREAL_0:def_9_:_
for a, b being ext-real number holds
( ( a <= b implies min (a,b) = a ) & ( not a <= b implies min (a,b) = b ) );
:: deftheorem Def10 defines max XXREAL_0:def_10_:_
for a, b being ext-real number holds
( ( b <= a implies max (a,b) = a ) & ( not b <= a implies max (a,b) = b ) );
theorem :: XXREAL_0:15
for a, b being ext-real number holds
( min (a,b) = a or min (a,b) = b ) by Def9;
theorem :: XXREAL_0:16
for a, b being ext-real number holds
( max (a,b) = a or max (a,b) = b ) by Def10;
registration
let a, b be ext-real number ;
cluster min (a,b) -> ext-real ;
coherence
min (a,b) is ext-real by Def9;
cluster max (a,b) -> ext-real ;
coherence
max (a,b) is ext-real by Def10;
end;
theorem Th17: :: XXREAL_0:17
for a, b being ext-real number holds min (a,b) <= a
proof
let a, b be ext-real number ; ::_thesis: min (a,b) <= a
( a <= b or not a <= b ) ;
hence min (a,b) <= a by Def9; ::_thesis: verum
end;
theorem Th18: :: XXREAL_0:18
for a, b, c, d being ext-real number st a <= b & c <= d holds
min (a,c) <= min (b,d)
proof
let a, b, c, d be ext-real number ; ::_thesis: ( a <= b & c <= d implies min (a,c) <= min (b,d) )
assume that
A1: a <= b and
A2: c <= d ; ::_thesis: min (a,c) <= min (b,d)
min (a,c) <= c by Th17;
then A3: min (a,c) <= d by A2, Th2;
min (a,c) <= a by Th17;
then min (a,c) <= b by A1, Th2;
hence min (a,c) <= min (b,d) by A3, Def9; ::_thesis: verum
end;
theorem :: XXREAL_0:19
for a, b, c, d being ext-real number st a < b & c < d holds
min (a,c) < min (b,d)
proof
let a, b, c, d be ext-real number ; ::_thesis: ( a < b & c < d implies min (a,c) < min (b,d) )
assume that
A1: a < b and
A2: c < d ; ::_thesis: min (a,c) < min (b,d)
min (a,c) <= c by Th17;
then A3: min (a,c) < d by A2, Th2;
min (a,c) <= a by Th17;
then min (a,c) < b by A1, Th2;
hence min (a,c) < min (b,d) by A3, Def9; ::_thesis: verum
end;
theorem :: XXREAL_0:20
for a, b, c being ext-real number st a <= b & a <= c holds
a <= min (b,c) by Def9;
theorem :: XXREAL_0:21
for a, b, c being ext-real number st a < b & a < c holds
a < min (b,c) by Def9;
theorem :: XXREAL_0:22
for a, b, c being ext-real number st a <= min (b,c) holds
a <= b
proof
let a, b, c be ext-real number ; ::_thesis: ( a <= min (b,c) implies a <= b )
min (b,c) <= b by Th17;
hence ( a <= min (b,c) implies a <= b ) by Th2; ::_thesis: verum
end;
theorem :: XXREAL_0:23
for a, b, c being ext-real number st a < min (b,c) holds
a < b
proof
let a, b, c be ext-real number ; ::_thesis: ( a < min (b,c) implies a < b )
min (b,c) <= b by Th17;
hence ( a < min (b,c) implies a < b ) by Th2; ::_thesis: verum
end;
theorem :: XXREAL_0:24
for c, a, b being ext-real number st c <= a & c <= b & ( for d being ext-real number st d <= a & d <= b holds
d <= c ) holds
c = min (a,b)
proof
let c, a, b be ext-real number ; ::_thesis: ( c <= a & c <= b & ( for d being ext-real number st d <= a & d <= b holds
d <= c ) implies c = min (a,b) )
assume that
A1: ( c <= a & c <= b ) and
A2: for d being ext-real number st d <= a & d <= b holds
d <= c ; ::_thesis: c = min (a,b)
( min (a,b) <= a & min (a,b) <= b ) by Th17;
then A3: min (a,b) <= c by A2;
c <= min (a,b) by A1, Def9;
hence c = min (a,b) by A3, Th1; ::_thesis: verum
end;
theorem Th25: :: XXREAL_0:25
for a, b being ext-real number holds a <= max (a,b)
proof
let a, b be ext-real number ; ::_thesis: a <= max (a,b)
( a <= b or not a <= b ) ;
hence a <= max (a,b) by Def10; ::_thesis: verum
end;
theorem Th26: :: XXREAL_0:26
for a, b, c, d being ext-real number st a <= b & c <= d holds
max (a,c) <= max (b,d)
proof
let a, b, c, d be ext-real number ; ::_thesis: ( a <= b & c <= d implies max (a,c) <= max (b,d) )
assume that
A1: a <= b and
A2: c <= d ; ::_thesis: max (a,c) <= max (b,d)
d <= max (b,d) by Th25;
then A3: c <= max (b,d) by A2, Th2;
b <= max (b,d) by Th25;
then a <= max (b,d) by A1, Th2;
hence max (a,c) <= max (b,d) by A3, Def10; ::_thesis: verum
end;
theorem :: XXREAL_0:27
for a, b, c, d being ext-real number st a < b & c < d holds
max (a,c) < max (b,d)
proof
let a, b, c, d be ext-real number ; ::_thesis: ( a < b & c < d implies max (a,c) < max (b,d) )
assume that
A1: a < b and
A2: c < d ; ::_thesis: max (a,c) < max (b,d)
d <= max (b,d) by Th25;
then A3: c < max (b,d) by A2, Th2;
b <= max (b,d) by Th25;
then a < max (b,d) by A1, Th2;
hence max (a,c) < max (b,d) by A3, Def10; ::_thesis: verum
end;
theorem :: XXREAL_0:28
for b, a, c being ext-real number st b <= a & c <= a holds
max (b,c) <= a by Def10;
theorem :: XXREAL_0:29
for b, a, c being ext-real number st b < a & c < a holds
max (b,c) < a by Def10;
theorem :: XXREAL_0:30
for b, c, a being ext-real number st max (b,c) <= a holds
b <= a
proof
let b, c, a be ext-real number ; ::_thesis: ( max (b,c) <= a implies b <= a )
b <= max (b,c) by Th25;
hence ( max (b,c) <= a implies b <= a ) by Th2; ::_thesis: verum
end;
theorem :: XXREAL_0:31
for b, c, a being ext-real number st max (b,c) < a holds
b < a
proof
let b, c, a be ext-real number ; ::_thesis: ( max (b,c) < a implies b < a )
b <= max (b,c) by Th25;
hence ( max (b,c) < a implies b < a ) by Th2; ::_thesis: verum
end;
theorem :: XXREAL_0:32
for a, c, b being ext-real number st a <= c & b <= c & ( for d being ext-real number st a <= d & b <= d holds
c <= d ) holds
c = max (a,b)
proof
let a, c, b be ext-real number ; ::_thesis: ( a <= c & b <= c & ( for d being ext-real number st a <= d & b <= d holds
c <= d ) implies c = max (a,b) )
assume that
A1: ( a <= c & b <= c ) and
A2: for d being ext-real number st a <= d & b <= d holds
c <= d ; ::_thesis: c = max (a,b)
( a <= max (a,b) & b <= max (a,b) ) by Th25;
then A3: c <= max (a,b) by A2;
max (a,b) <= c by A1, Def10;
hence c = max (a,b) by A3, Th1; ::_thesis: verum
end;
theorem :: XXREAL_0:33
for a, b, c being ext-real number holds min ((min (a,b)),c) = min (a,(min (b,c)))
proof
let a, b, c be ext-real number ; ::_thesis: min ((min (a,b)),c) = min (a,(min (b,c)))
percases ( ( a <= b & a <= c ) or ( b <= a & b <= c ) or ( c <= b & c <= a ) ) by Th2;
suppose ( a <= b & a <= c ) ; ::_thesis: min ((min (a,b)),c) = min (a,(min (b,c)))
then ( min (a,b) = a & min (a,c) = a ) by Def9;
hence min ((min (a,b)),c) = min (a,(min (b,c))) by Def9; ::_thesis: verum
end;
suppose ( b <= a & b <= c ) ; ::_thesis: min ((min (a,b)),c) = min (a,(min (b,c)))
then ( min (a,b) = b & min (b,c) = b ) by Def9;
hence min ((min (a,b)),c) = min (a,(min (b,c))) ; ::_thesis: verum
end;
suppose ( c <= b & c <= a ) ; ::_thesis: min ((min (a,b)),c) = min (a,(min (b,c)))
then ( min (b,c) = c & min (a,c) = c ) by Def9;
hence min ((min (a,b)),c) = min (a,(min (b,c))) by Def9; ::_thesis: verum
end;
end;
end;
theorem :: XXREAL_0:34
for a, b, c being ext-real number holds max ((max (a,b)),c) = max (a,(max (b,c)))
proof
let a, b, c be ext-real number ; ::_thesis: max ((max (a,b)),c) = max (a,(max (b,c)))
percases ( ( a <= b & a <= c ) or ( b <= a & b <= c ) or ( c <= b & c <= a ) ) by Th2;
supposeA1: ( a <= b & a <= c ) ; ::_thesis: max ((max (a,b)),c) = max (a,(max (b,c)))
A2: ( max (b,c) = b or max (b,c) = c ) by Def10;
max (a,b) = b by A1, Def10;
hence max ((max (a,b)),c) = max (a,(max (b,c))) by A1, A2, Def10; ::_thesis: verum
end;
supposeA3: ( b <= a & b <= c ) ; ::_thesis: max ((max (a,b)),c) = max (a,(max (b,c)))
then max (a,b) = a by Def10;
hence max ((max (a,b)),c) = max (a,(max (b,c))) by A3, Def10; ::_thesis: verum
end;
supposeA4: ( c <= b & c <= a ) ; ::_thesis: max ((max (a,b)),c) = max (a,(max (b,c)))
A5: ( max (a,b) = b or max (a,b) = a ) by Def10;
max (b,c) = b by A4, Def10;
hence max ((max (a,b)),c) = max (a,(max (b,c))) by A4, A5, Def10; ::_thesis: verum
end;
end;
end;
theorem :: XXREAL_0:35
for a, b being ext-real number holds min ((max (a,b)),b) = b
proof
let a, b be ext-real number ; ::_thesis: min ((max (a,b)),b) = b
b <= max (a,b) by Th25;
hence min ((max (a,b)),b) = b by Def9; ::_thesis: verum
end;
theorem :: XXREAL_0:36
for a, b being ext-real number holds max ((min (a,b)),b) = b
proof
let a, b be ext-real number ; ::_thesis: max ((min (a,b)),b) = b
min (a,b) <= b by Th17;
hence max ((min (a,b)),b) = b by Def10; ::_thesis: verum
end;
theorem Th37: :: XXREAL_0:37
for a, c, b being ext-real number st a <= c holds
max (a,(min (b,c))) = min ((max (a,b)),c)
proof
let a, c, b be ext-real number ; ::_thesis: ( a <= c implies max (a,(min (b,c))) = min ((max (a,b)),c) )
assume A1: a <= c ; ::_thesis: max (a,(min (b,c))) = min ((max (a,b)),c)
percases ( a <= b or b <= a ) ;
supposeA2: a <= b ; ::_thesis: max (a,(min (b,c))) = min ((max (a,b)),c)
then a <= min (b,c) by A1, Def9;
hence max (a,(min (b,c))) = min (b,c) by Def10
.= min ((max (a,b)),c) by A2, Def10 ;
::_thesis: verum
end;
supposeA3: b <= a ; ::_thesis: max (a,(min (b,c))) = min ((max (a,b)),c)
then b <= c by A1, Th2;
hence max (a,(min (b,c))) = max (a,b) by Def9
.= a by A3, Def10
.= min (a,c) by A1, Def9
.= min ((max (a,b)),c) by A3, Def10 ;
::_thesis: verum
end;
end;
end;
theorem :: XXREAL_0:38
for a, b, c being ext-real number holds min (a,(max (b,c))) = max ((min (a,b)),(min (a,c)))
proof
let a, b, c be ext-real number ; ::_thesis: min (a,(max (b,c))) = max ((min (a,b)),(min (a,c)))
percases ( b <= c or c <= b ) ;
supposeA1: b <= c ; ::_thesis: min (a,(max (b,c))) = max ((min (a,b)),(min (a,c)))
then A2: min (a,b) <= min (a,c) by Th18;
thus min (a,(max (b,c))) = min (a,c) by A1, Def10
.= max ((min (a,b)),(min (a,c))) by A2, Def10 ; ::_thesis: verum
end;
supposeA3: c <= b ; ::_thesis: min (a,(max (b,c))) = max ((min (a,b)),(min (a,c)))
then A4: min (a,c) <= min (a,b) by Th18;
thus min (a,(max (b,c))) = min (a,b) by A3, Def10
.= max ((min (a,b)),(min (a,c))) by A4, Def10 ; ::_thesis: verum
end;
end;
end;
theorem :: XXREAL_0:39
for a, b, c being ext-real number holds max (a,(min (b,c))) = min ((max (a,b)),(max (a,c)))
proof
let a, b, c be ext-real number ; ::_thesis: max (a,(min (b,c))) = min ((max (a,b)),(max (a,c)))
percases ( b <= c or c <= b ) ;
supposeA1: b <= c ; ::_thesis: max (a,(min (b,c))) = min ((max (a,b)),(max (a,c)))
then A2: max (a,b) <= max (a,c) by Th26;
thus max (a,(min (b,c))) = max (a,b) by A1, Def9
.= min ((max (a,b)),(max (a,c))) by A2, Def9 ; ::_thesis: verum
end;
supposeA3: c <= b ; ::_thesis: max (a,(min (b,c))) = min ((max (a,b)),(max (a,c)))
then A4: max (a,c) <= max (a,b) by Th26;
thus max (a,(min (b,c))) = max (a,c) by A3, Def9
.= min ((max (a,b)),(max (a,c))) by A4, Def9 ; ::_thesis: verum
end;
end;
end;
theorem :: XXREAL_0:40
for a, b, c being ext-real number holds max ((max ((min (a,b)),(min (b,c)))),(min (c,a))) = min ((min ((max (a,b)),(max (b,c)))),(max (c,a)))
proof
let a, b, c be ext-real number ; ::_thesis: max ((max ((min (a,b)),(min (b,c)))),(min (c,a))) = min ((min ((max (a,b)),(max (b,c)))),(max (c,a)))
percases ( a <= c or c <= a ) ;
supposeA1: a <= c ; ::_thesis: max ((max ((min (a,b)),(min (b,c)))),(min (c,a))) = min ((min ((max (a,b)),(max (b,c)))),(max (c,a)))
then A2: max (a,b) <= max (b,c) by Th26;
min (a,b) <= min (b,c) by A1, Th18;
hence max ((max ((min (a,b)),(min (b,c)))),(min (c,a))) = max ((min (b,c)),(min (c,a))) by Def10
.= max ((min (b,c)),a) by A1, Def9
.= min ((max (a,b)),c) by A1, Th37
.= min ((max (a,b)),(max (c,a))) by A1, Def10
.= min ((min ((max (a,b)),(max (b,c)))),(max (c,a))) by A2, Def9 ;
::_thesis: verum
end;
supposeA3: c <= a ; ::_thesis: max ((max ((min (a,b)),(min (b,c)))),(min (c,a))) = min ((min ((max (a,b)),(max (b,c)))),(max (c,a)))
then A4: max (a,b) >= max (b,c) by Th26;
min (a,b) >= min (b,c) by A3, Th18;
hence max ((max ((min (a,b)),(min (b,c)))),(min (c,a))) = max ((min (a,b)),(min (c,a))) by Def10
.= max ((min (a,b)),c) by A3, Def9
.= min ((max (c,b)),a) by A3, Th37
.= min ((max (c,b)),(max (c,a))) by A3, Def10
.= min ((min ((max (a,b)),(max (b,c)))),(max (c,a))) by A4, Def9 ;
::_thesis: verum
end;
end;
end;
theorem :: XXREAL_0:41
for a being ext-real number holds max (a,+infty) = +infty
proof
let a be ext-real number ; ::_thesis: max (a,+infty) = +infty
a <= +infty by Def5, Lm2, Lm4;
hence max (a,+infty) = +infty by Def10; ::_thesis: verum
end;
theorem :: XXREAL_0:42
for a being ext-real number holds min (a,+infty) = a
proof
let a be ext-real number ; ::_thesis: min (a,+infty) = a
a <= +infty by Def5, Lm2, Lm4;
hence min (a,+infty) = a by Def9; ::_thesis: verum
end;
theorem :: XXREAL_0:43
for a being ext-real number holds max (a,-infty) = a
proof
let a be ext-real number ; ::_thesis: max (a,-infty) = a
a >= -infty by Def5, Lm3, Lm5;
hence max (a,-infty) = a by Def10; ::_thesis: verum
end;
theorem :: XXREAL_0:44
for a being ext-real number holds min (a,-infty) = -infty
proof
let a be ext-real number ; ::_thesis: min (a,-infty) = -infty
a >= -infty by Def5, Lm3, Lm5;
hence min (a,-infty) = -infty by Def9; ::_thesis: verum
end;
begin
theorem :: XXREAL_0:45
for a, c, b being ext-real number st a in REAL & c in REAL & a <= b & b <= c holds
b in REAL
proof
let a, c, b be ext-real number ; ::_thesis: ( a in REAL & c in REAL & a <= b & b <= c implies b in REAL )
assume that
A1: a in REAL and
A2: c in REAL and
A3: a <= b and
A4: b <= c ; ::_thesis: b in REAL
( b in REAL or b = +infty ) by A1, A3, Th10;
hence b in REAL by A2, A4, Th13; ::_thesis: verum
end;
theorem :: XXREAL_0:46
for a, b, c being ext-real number st a in REAL & a <= b & b < c holds
b in REAL
proof
let a, b, c be ext-real number ; ::_thesis: ( a in REAL & a <= b & b < c implies b in REAL )
assume that
A1: ( a in REAL & a <= b ) and
A2: b < c ; ::_thesis: b in REAL
( b in REAL or b = +infty ) by A1, Th10;
hence b in REAL by A2, Lm8; ::_thesis: verum
end;
theorem :: XXREAL_0:47
for c, a, b being ext-real number st c in REAL & a < b & b <= c holds
b in REAL
proof
let c, a, b be ext-real number ; ::_thesis: ( c in REAL & a < b & b <= c implies b in REAL )
assume that
A1: c in REAL and
A2: a < b and
A3: b <= c ; ::_thesis: b in REAL
( b in REAL or b = -infty ) by A1, A3, Th13;
hence b in REAL by A2, Lm7; ::_thesis: verum
end;
theorem :: XXREAL_0:48
for a, b, c being ext-real number st a < b & b < c holds
b in REAL
proof
let a, b, c be ext-real number ; ::_thesis: ( a < b & b < c implies b in REAL )
assume A1: ( a < b & b < c ) ; ::_thesis: b in REAL
( b in REAL or b = +infty or b = -infty ) by Lm9;
hence b in REAL by A1, Lm7, Lm8; ::_thesis: verum
end;
definition
let x, y be ext-real number ;
let a, b be set ;
func IFGT (x,y,a,b) -> set equals :Def11: :: XXREAL_0:def 11
a if x > y
otherwise b;
correctness
coherence
( ( x > y implies a is set ) & ( not x > y implies b is set ) );
consistency
for b1 being set holds verum;
;
end;
:: deftheorem Def11 defines IFGT XXREAL_0:def_11_:_
for x, y being ext-real number
for a, b being set holds
( ( x > y implies IFGT (x,y,a,b) = a ) & ( not x > y implies IFGT (x,y,a,b) = b ) );
registration
let x, y be ext-real number ;
let a, b be Nat;
cluster IFGT (x,y,a,b) -> natural ;
coherence
IFGT (x,y,a,b) is natural by Def11;
end;
theorem :: XXREAL_0:49
for a, b being ext-real number st max (a,b) <= a holds
max (a,b) = a
proof
let a, b be ext-real number ; ::_thesis: ( max (a,b) <= a implies max (a,b) = a )
assume max (a,b) <= a ; ::_thesis: max (a,b) = a
then ( max (a,b) < a or max (a,b) = a ) by Th1;
hence max (a,b) = a by Th25; ::_thesis: verum
end;
theorem :: XXREAL_0:50
for a, b being ext-real number st a <= min (a,b) holds
min (a,b) = a
proof
let a, b be ext-real number ; ::_thesis: ( a <= min (a,b) implies min (a,b) = a )
assume min (a,b) >= a ; ::_thesis: min (a,b) = a
then ( min (a,b) > a or min (a,b) = a ) by Th1;
hence min (a,b) = a by Th17; ::_thesis: verum
end;