:: Introduction to Arithmetic of Extended Real Numbers
:: by Library Committee
::
:: Received January 4, 2006
:: Copyright (c) 2006-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ORDINAL1, CARD_1, SUBSET_1, XBOOLE_0, ARYTM_2, ARYTM_3,
ZFMISC_1, XCMPLX_0, XXREAL_0, TARSKI, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ARYTM_2, NUMBERS;
constructors ARYTM_2, NUMBERS;
registrations ORDINAL1, XBOOLE_0;
requirements BOOLE, SUBSET;
definitions ORDINAL1;
equalities TARSKI, NUMBERS, ORDINAL1;
expansions TARSKI, ORDINAL1;
theorems XBOOLE_0, TARSKI, ORDINAL1, ARYTM_0, ZFMISC_1, ARYTM_1, ENUMSET1,
XTUPLE_0, XREGULAR, NUMBERS, SUBSET_1;
begin
Lm0: not REAL in REAL;
reserve x for set;
definition
let x be object;
attr x is ext-real means
:Def1:
x in ExtREAL;
end;
registration
cluster ext-real for object;
existence
proof
take 0;
NAT c= ExtREAL by NUMBERS:19,31;
hence 0 in ExtREAL;
end;
cluster ext-real for number;
existence
proof
take 0;
NAT c= ExtREAL by NUMBERS:19,31;
hence 0 in ExtREAL;
end;
cluster -> ext-real for Element of ExtREAL;
coherence;
end;
definition
mode ExtReal is ext-real Number;
end;
registration
sethood of ExtReal
proof
take ExtREAL;
thus thesis by Def1;
end;
end;
registration
let x be ExtReal;
reduce In(x,ExtREAL) to x;
reducibility by Def1,SUBSET_1:def 8;
end;
registration
let x,y be ExtReal;
reduce In([x,y],[:ExtREAL,ExtREAL:]) to [x,y];
reducibility
proof
[In(x,ExtREAL),In(y,ExtREAL)] in [:ExtREAL,ExtREAL:] by ZFMISC_1:87;
hence thesis by SUBSET_1:def 8;
end;
end;
definition
func +infty -> object equals
REAL;
coherence;
func -infty -> object equals
[0,REAL];
coherence;
end;
definition
redefine func ExtREAL equals :: redefines ExtREAL (NUMBERS, definition)
REAL \/ {+infty,-infty};
compatibility;
end;
registration
cluster +infty -> ext-real;
coherence
proof
+infty in {REAL,[0,REAL]} by TARSKI:def 2;
then +infty in ExtREAL by XBOOLE_0:def 3;
hence thesis;
end;
cluster -infty -> ext-real;
coherence
proof
-infty in {REAL,[0,REAL]} by TARSKI:def 2;
then -infty in ExtREAL by XBOOLE_0:def 3;
hence thesis;
end;
end;
definition
let x,y be ExtReal;
pred x <= y means
:Def5:
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 by ARYTM_0:5,XBOOLE_0:3;
reflexivity
proof
let x be ExtReal such that
A1: not((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+ & x in REAL+) & not(x in [:{0},REAL+:] & x in [:{0},REAL+
:]) implies x in REAL+ & x in [:{0},REAL+:] or x = -infty or x = +infty));
x in ExtREAL by Def1;
then
A2: x in REAL+ \/ [:{0},REAL+:] \ {[0,0]} or x in {+infty,-infty} by
XBOOLE_0:def 3;
per cases by A1;
suppose that
A3: x in REAL+ and
A4: not ex x9,y9 being Element of REAL+ st x = x9 & x = y9 & x9 <=' y9;
reconsider x9 = x as Element of REAL+ by A3;
not x9 <=' x9 by A4;
hence thesis;
end;
suppose that
A5: x in [:{0},REAL+:] and
A6: not ex x9,y9 being Element of REAL+ st x = [0,x9] & x = [0,y9] &
y9 <=' x9;
consider z,x9 being object such that
A7: z in {0} and
A8: x9 in REAL+ and
A9: x = [z,x9] by A5,ZFMISC_1:84;
reconsider x9 as Element of REAL+ by A8;
x = [0,x9] by A7,A9,TARSKI:def 1;
then not x9 <=' x9 by A6;
hence thesis;
end;
suppose
not(not x in REAL+ & not x in [:{0},REAL+:] implies x in REAL+
& x in [:{0},REAL+:] or x = -infty or x = +infty);
hence thesis by A2,TARSKI:def 2,XBOOLE_0:def 3;
end;
end;
connectedness
proof
let x,y be ExtReal such that
A10: not((x in REAL+ & y in REAL+ implies ex x9,y9 being Element of
REAL+ st x = x9 & y = y9 & x9 <=' y9) & (x in [:{0},REAL+:] & y in [:{0},REAL+
:] implies ex x9,y9 being Element of REAL+ st x = [0,x9] & y = [0,y9] & y9 <='
x9) & (not(x in REAL+ & y in REAL+) & not(x in [:{0},REAL+:] & y in [:{0},REAL+
:]) implies y in REAL+ & x in [:{0},REAL+:] or x = -infty or y = +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;
per cases by A10;
suppose that
A13: x in REAL+ & y in REAL+ and
A14: not ex x9,y9 being Element of REAL+ st x = x9 & y = y9 & x9 <=' y9;
hereby
assume y in REAL+ & x in REAL+;
then reconsider x9 = x, y9 = y as Element of REAL+;
take y9,x9;
thus y = y9 & x = x9;
thus y9 <=' x9 by A14;
end;
thus thesis by A13,ARYTM_0:5,XBOOLE_0:3;
end;
suppose that
A15: x in [:{0},REAL+:] & y in [:{0},REAL+:] and
A16: not ex x9,y9 being Element of REAL+ st x = [0,x9] & y = [0,y9]
& y9 <=' x9;
now
assume y in [:{0},REAL+:];
then consider z,y9 being object 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+:];
then consider z,x9 being object such that
A21: z in {0} and
A22: x9 in REAL+ and
A23: x = [z,x9] by ZFMISC_1:84;
reconsider x9,y9 as Element of REAL+ by A18,A22;
take y9,x9;
thus y = [0,y9] & x = [0,x9] by A17,A19,A21,A23,TARSKI:def 1;
z = 0 by A21,TARSKI:def 1;
hence x9 <=' y9 by A16,A19,A20,A23;
end;
hence thesis by A15,ARYTM_0:5,XBOOLE_0:3;
end;
suppose
not(not(x in REAL+ & y in REAL+) & not(x in [:{0},REAL+:] & y
in [:{0},REAL+:]) implies y in REAL+ & x in [:{0},REAL+:] or x = -infty or y =
+infty);
hence thesis by A11,A12,TARSKI:def 2,XBOOLE_0:def 3;
end;
end;
end;
reserve a,b,c,d for ExtReal;
notation
let a,b be ExtReal;
synonym b >= a for a <= b;
antonym b < a for a <= b;
antonym a > b for a <= b;
end;
Lm1: 0 in REAL by NUMBERS:19;
Lm2: +infty <> [0,0]
proof
assume +infty = [0,0];
then +infty = {{0},{0}} by ENUMSET1:29
.= {{0}} by ENUMSET1:29;
hence contradiction by TARSKI:def 1,Lm1;
end;
Lm3: not +infty in REAL+ by ARYTM_0:1,ORDINAL1:5;
Lm4: not -infty in REAL+
proof
{0,REAL} in {{0,REAL},{0}} & REAL in {0,REAL} by TARSKI:def 2;
hence thesis by ARYTM_0:1,XREGULAR:7;
end;
Lm5: not +infty in [:{0},REAL+:]
proof
assume +infty in [:{0},REAL+:];
then +infty in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def 3;
then +infty in REAL by Lm2,ZFMISC_1:56;
hence contradiction by Lm0;
end;
Lm6: not -infty in [:{0},REAL+:]
proof
assume -infty in [:{0},REAL+:];
then REAL in REAL+ by ZFMISC_1:87;
hence contradiction by ARYTM_0:1,ORDINAL1:5;
end;
Lm7: -infty < +infty
proof
-infty <> +infty by TARSKI:def 2,Lm1;
hence thesis by Def5,Lm4,Lm6;
end;
theorem Th1:
for a,b being ExtReal holds a <= b & b <= a implies a = b
proof
let a,b be ExtReal;
assume that
A1: a <= b and
A2: b <= a;
per cases;
suppose
a in REAL+ & b in REAL+;
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 thesis by ARYTM_1:4;
end;
suppose
A3: a in REAL+ & b in [:{0},REAL+:];
then ( not b in REAL+)& not a in [:{0},REAL+:] by ARYTM_0:5,XBOOLE_0:3;
hence thesis by A1,A3,Def5,Lm4,Lm5;
end;
suppose
A4: b in REAL+ & a in [:{0},REAL+:];
then ( not a in REAL+)& not b in [:{0},REAL+:] by ARYTM_0:5,XBOOLE_0:3;
hence thesis by A2,A4,Def5,Lm4,Lm5;
end;
suppose that
A5: a in [:{0},REAL+:] & b in [:{0},REAL+:];
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 thesis by A7,A8,A9,ARYTM_1:4;
end;
suppose
(a = -infty or a = +infty) & (b = -infty or b = +infty);
hence thesis by A1,A2,Lm7;
end;
suppose that
A10: ( not(a in REAL+ & b in REAL+))& not(a in [:{0},REAL+:] & b in [:
{0},REAL+:]) and
A11: not(b in REAL+ & a in [:{0},REAL+:]) and
A12: not(a in REAL+ & b in [:{0},REAL+:]);
a = -infty or b = +infty by A1,A10,A11,Def5;
hence thesis by A2,A10,A12,Def5,Lm7;
end;
end;
Lm8: for a being ExtReal holds -infty >= a implies a = -infty
proof
let a be ExtReal;
a >= -infty by Def5,Lm4,Lm6;
hence thesis by Th1;
end;
Lm9: for a being ExtReal holds +infty <= a implies a = +infty
proof
let a be ExtReal;
a <= +infty by Def5,Lm3,Lm5;
hence thesis by Th1;
end;
theorem Th2:
for a,b,c being ExtReal holds
a <= b & b <= c implies a <= c
proof
let a,b,c be ExtReal;
assume that
A1: a <= b and
A2: b <= c;
per cases;
suppose that
A3: a in REAL+ and
A4: b in REAL+ and
A5: c in REAL+;
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 thesis by A5,A9,A7,Def5;
end;
suppose
A11: a in REAL+ & b in [:{0},REAL+:];
then
( not(a in REAL+ & b in REAL+))& not(a in [:{0},REAL+:] & b in [:{0},
REAL+:]) by ARYTM_0:5,XBOOLE_0:3;
hence thesis by A1,A11,Def5,Lm4,Lm5;
end;
suppose
A12: b in REAL+ & c in [:{0},REAL+:];
then
( not(c in REAL+ & b in REAL+))& not(c in [:{0},REAL+:] & b in [:{0},
REAL+:]) by ARYTM_0:5,XBOOLE_0:3;
hence thesis by A2,A12,Def5,Lm4,Lm5;
end;
suppose that
A13: a in [:{0},REAL+:] & c in REAL+;
( not(a in REAL+ & c in REAL+))& not(a in [:{0},REAL+:] & c in [:{0},
REAL+:]) by A13,ARYTM_0:5,XBOOLE_0:3;
hence thesis by A13,Def5;
end;
suppose that
A14: a in [:{0},REAL+:] and
A15: b in [:{0},REAL+:] and
A16: c in [:{0},REAL+:];
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 thesis by A14,A16,A20,A18,Def5;
end;
suppose that
A23: not(a in REAL+ & b in REAL+ & c in REAL+) and
A24: not(a in REAL+ & b in [:{0},REAL+:]) and
A25: not(b in REAL+ & c in [:{0},REAL+:]) and
A26: not(a in [:{0},REAL+:] & c in REAL+) and
A27: not(a in [:{0},REAL+:] & b in [:{0},REAL+:] & c in [:{0},REAL+:]);
A28: b = +infty implies c = +infty by A2,Lm9;
A29: b = -infty implies a = -infty by A1,Lm8;
a = -infty or b = +infty or b = -infty or c = +infty by A1,A2,A23,A25,A26
,A27,Def5;
hence thesis by A1,A2,A23,A24,A25,A27,A28,A29,Def5;
end;
end;
theorem
a <= +infty by Def5,Lm3,Lm5;
theorem
+infty <= a implies a = +infty by Lm9;
theorem
a >= -infty by Def5,Lm4,Lm6;
theorem
-infty >= a implies a = -infty by Lm8;
theorem
-infty < +infty by Lm7;
theorem
not +infty in REAL by Lm0;
Lm10: a in REAL or a = +infty or a = -infty
proof
a in ExtREAL by Def1;
then a in REAL or a in { +infty, -infty } by XBOOLE_0:def 3;
hence thesis by TARSKI:def 2;
end;
theorem Th9:
a in REAL implies +infty > a
proof
assume a in REAL;
then
A1: a <> +infty by Lm0;
+infty >= a by Def5,Lm3,Lm5;
hence thesis by A1,Th1;
end;
theorem Th10:
a in REAL & b >= a implies b in REAL or b = +infty
proof
assume that
A1: a in REAL and
A2: b >= a;
assume
A3: not b in REAL;
b = -infty implies a = -infty by A2,Lm8;
hence thesis by A1,A3,Lm10;
end;
theorem Th11:
not -infty in REAL
proof
A1: {0,REAL} in {{0,REAL},{0}} & REAL in {0,REAL} by TARSKI:def 2;
assume -infty in REAL;
hence contradiction by A1,XREGULAR:7;
end;
theorem Th12:
a in REAL implies -infty < a
proof
-infty <= a by Def5,Lm4,Lm6;
hence thesis by Th1,Th11;
end;
theorem Th13:
a in REAL & b <= a implies b in REAL or b = -infty
proof
assume that
A1: a in REAL and
A2: b <= a;
assume
A3: not b in REAL;
b = +infty implies a = +infty by A2,Lm9;
hence thesis by A1,A3,Lm10;
end;
theorem
a in REAL or a = +infty or a = -infty by Lm10;
begin :: positive & negative
registration
cluster natural -> ext-real for object;
coherence by NUMBERS:19,XBOOLE_0:def 3;
end;
:: notation
:: let a be number;
:: synonym a is zero for a is empty;
:: end;
definition
let a be ExtReal;
attr a is positive means
a > 0;
attr a is negative means
a < 0;
:: redefine attr a is zero means
:: a = 0;
:: compatibility;
::$CD
end;
registration
cluster positive -> non negative non zero for ExtReal;
coherence;
cluster non negative non zero -> positive for ExtReal;
coherence by Th1;
cluster negative -> non positive non zero for ExtReal;
coherence;
cluster non positive non zero -> negative for ExtReal;
coherence;
cluster zero -> non negative non positive for ExtReal;
coherence;
cluster non negative non positive -> zero for ExtReal;
coherence;
end;
registration
cluster +infty -> positive;
coherence by Th9,Lm1;
cluster -infty -> negative;
coherence by Th12,Lm1;
end;
registration
cluster positive for ExtReal;
existence
proof
take +infty;
thus thesis;
end;
cluster negative for ExtReal;
existence
proof
take -infty;
thus thesis;
end;
cluster zero for ExtReal;
existence
proof
reconsider z = 0 as ExtReal;
take z;
thus z = 0;
end;
end;
begin :: min & max
definition
let a,b be ExtReal;
func min(a,b) -> ExtReal equals
:Def8:
a if a <= b otherwise b;
correctness;
commutativity by Th1;
idempotence;
func max(a,b) -> ExtReal equals
:Def9:
a if b <= a otherwise b;
correctness;
commutativity by Th1;
idempotence;
end;
theorem
min(a,b) = a or min(a,b) = b by Def8;
theorem
max(a,b) = a or max(a,b) = b by Def9;
registration
let a,b;
cluster min(a,b) -> ext-real;
coherence;
cluster max(a,b) -> ext-real;
coherence;
end;
theorem Th17:
min(a,b) <= a
proof
a <= b or not a <= b;
hence thesis by Def8;
end;
theorem Th18:
a <= b & c <= d implies min(a,c) <= min(b,d)
proof
assume that
A1: a <= b and
A2: c <= 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 thesis by A3,Def8;
end;
theorem
a < b & c < d implies min(a,c) < min(b,d)
proof
assume that
A1: a < b and
A2: c < 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 thesis by A3,Def8;
end;
theorem
a <= b & a <= c implies a <= min(b,c) by Def8;
theorem
a < b & a < c implies a < min(b,c) by Def8;
theorem
a <= min(b,c) implies a <= b
proof
min(b,c) <= b by Th17;
hence thesis by Th2;
end;
theorem
a < min(b,c) implies a < b
proof
min(b,c) <= b by Th17;
hence thesis by Th2;
end;
theorem
c <= a & c <= b & (for d st d <= a & d <= b holds d <= c) implies c =
min(a,b)
proof
assume that
A1: c <= a & c <= b and
A2: for d st d <= a & d <= b holds d <= c;
min(a,b) <= a & min(a,b) <= b by Th17;
then
A3: min(a,b) <= c by A2;
c <= min(a,b) by A1,Def8;
hence thesis by A3,Th1;
end;
theorem Th25:
a <= max(a,b)
proof
a <= b or not a <= b;
hence thesis by Def9;
end;
theorem Th26:
a <= b & c <= d implies max(a,c) <= max(b,d)
proof
assume that
A1: a <= b and
A2: c <= 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 thesis by A3,Def9;
end;
theorem
a < b & c < d implies max(a,c) < max(b,d)
proof
assume that
A1: a < b and
A2: c < 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 thesis by A3,Def9;
end;
theorem
b <= a & c <= a implies max(b,c) <= a by Def9;
theorem
b < a & c < a implies max(b,c) < a by Def9;
theorem
max(b,c) <= a implies b <= a
proof
b <= max(b,c) by Th25;
hence thesis by Th2;
end;
theorem
max(b,c) < a implies b < a
proof
b <= max(b,c) by Th25;
hence thesis by Th2;
end;
theorem
a <= c & b <= c & (for d st a <= d & b <= d holds c <= d) implies c =
max(a,b)
proof
assume that
A1: a <= c & b <= c and
A2: for d st a <= d & b <= d holds c <= d;
a <= max(a,b) & b <= max(a,b) by Th25;
then
A3: c <= max(a,b) by A2;
max(a,b) <= c by A1,Def9;
hence thesis by A3,Th1;
end;
theorem
min(min(a,b),c) = min(a,min(b,c))
proof
per cases by Th2;
suppose
a <= b & a <= c;
then min(a,b) = a & min(a,c) = a by Def8;
hence thesis by Def8;
end;
suppose
b <= a & b <= c;
then min(a,b) = b & min(b,c) = b by Def8;
hence thesis;
end;
suppose
c <= b & c <= a;
then min(b,c) = c & min(a,c) = c by Def8;
hence thesis by Def8;
end;
end;
theorem
max(max(a,b),c) = max(a,max(b,c))
proof
per cases by Th2;
suppose
A1: a <= b & a <= c;
A2: max(b,c) = b or max(b,c) = c by Def9;
max(a,b) = b by A1,Def9;
hence thesis by A1,A2,Def9;
end;
suppose
A3: b <= a & b <= c;
then max(a,b) = a by Def9;
hence thesis by A3,Def9;
end;
suppose
A4: c <= b & c <= a;
A5: max(a,b) = b or max(a,b) = a by Def9;
max(b,c) = b by A4,Def9;
hence thesis by A4,A5,Def9;
end;
end;
theorem
min(max(a,b),b) = b
by Th25,Def8;
theorem
max(min(a,b),b) = b
by Th17,Def9;
theorem Th37:
a <= c implies max(a,min(b,c)) = min(max(a,b),c)
proof
assume
A1: a <= c;
per cases;
suppose
A2: a <= b;
then a <= min(b,c) by A1,Def8;
hence max(a,min(b,c)) = min(b,c) by Def9
.= min(max(a,b),c) by A2,Def9;
end;
suppose
A3: b <= a;
then b <= c by A1,Th2;
hence max(a,min(b,c)) = max(a,b) by Def8
.= a by A3,Def9
.= min(a,c) by A1,Def8
.= min(max(a,b),c) by A3,Def9;
end;
end;
theorem
min(a,max(b,c)) = max(min(a,b),min(a,c))
proof
per cases;
suppose
A1: b <= c;
then
A2: min(a,b) <= min(a,c) by Th18;
thus min(a,max(b,c)) = min(a,c) by A1,Def9
.= max(min(a,b),min(a,c)) by A2,Def9;
end;
suppose
A3: c <= b;
then
A4: min(a,c) <= min(a,b) by Th18;
thus min(a,max(b,c)) = min(a,b) by A3,Def9
.= max(min(a,b),min(a,c)) by A4,Def9;
end;
end;
theorem
max(a,min(b,c)) = min(max(a,b),max(a,c))
proof
per cases;
suppose
A1: b <= c;
then
A2: max(a,b) <= max(a,c) by Th26;
thus max(a,min(b,c)) = max(a,b) by A1,Def8
.= min(max(a,b),max(a,c)) by A2,Def8;
end;
suppose
A3: c <= b;
then
A4: max(a,c) <= max(a,b) by Th26;
thus max(a,min(b,c)) = max(a,c) by A3,Def8
.= min(max(a,b),max(a,c)) by A4,Def8;
end;
end;
theorem
max(max(min(a,b),min(b,c)),min(c,a)) = min(min(max(a,b),max(b,c)),max( c,a))
proof
per cases;
suppose
A1: a <= c;
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
Def9
.= max(min(b,c),a) by A1,Def8
.= min(max(a,b),c) by A1,Th37
.= min(max(a,b),max(c,a)) by A1,Def9
.= min(min(max(a,b),max(b,c)),max(c,a)) by A2,Def8;
end;
suppose
A3: 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
Def9
.= max(min(a,b),c) by A3,Def8
.= min(max(c,b),a) by A3,Th37
.= min(max(c,b),max(c,a)) by A3,Def9
.= min(min(max(a,b),max(b,c)),max(c,a)) by A4,Def8;
end;
end;
theorem
max(a,+infty) = +infty
proof
a <= +infty by Def5,Lm3,Lm5;
hence thesis by Def9;
end;
theorem
min(a,+infty) = a
proof
a <= +infty by Def5,Lm3,Lm5;
hence thesis by Def8;
end;
theorem
max(a,-infty) = a
proof
a >= -infty by Def5,Lm4,Lm6;
hence thesis by Def9;
end;
theorem
min(a,-infty) = -infty
proof
a >= -infty by Def5,Lm4,Lm6;
hence thesis by Def8;
end;
begin :: Addenda
theorem
a in REAL & c in REAL & a <= b & b <= c implies b in REAL
proof
assume that
A1: a in REAL and
A2: c in REAL and
A3: a <= b and
A4: b <= c;
b in REAL or b = +infty by A1,A3,Th10;
hence thesis by A2,A4,Th13;
end;
theorem
a in REAL & a <= b & b < c implies b in REAL
proof
assume that
A1: a in REAL & a <= b and
A2: b < c;
b in REAL or b = +infty by A1,Th10;
hence thesis by A2,Lm9;
end;
theorem
c in REAL & a < b & b <= c implies b in REAL
proof
assume that
A1: c in REAL and
A2: a < b and
A3: b <= c;
b in REAL or b = -infty by A1,A3,Th13;
hence thesis by A2,Lm8;
end;
theorem
a < b & b < c implies b in REAL
proof
assume
A1: a < b & b < c;
b in REAL or b = +infty or b = -infty by Lm10;
hence thesis by A1,Lm8,Lm9;
end;
:: from AMI_2, 2008.02.14, A.T.
definition
let x,y be ExtReal, a,b be object;
func IFGT(x,y,a,b) -> object equals
:Def10:
a if x > y otherwise b;
correctness;
end;
registration
let x,y be ExtReal, a,b be natural Number;
cluster IFGT(x,y,a,b) -> natural;
coherence by Def10;
end;
:: from TOPREAL7, 2008.07.05, A.T.
theorem
max(a,b) <= a implies max(a,b) = a
proof
assume max(a,b) <= a;
then max(a,b) < a or max(a,b) = a by Th1;
hence thesis by Th25;
end;
theorem
a <= min(a,b) implies min(a,b) = a
proof
assume min(a,b) >= a;
then min(a,b) > a or min(a,b) = a by Th1;
hence thesis by Th17;
end;