:: Introduction to Arithmetic of Extended Real Numbers
:: by Library Committee
::
:: Received January 4, 2006
:: Copyright (c) 2006-2016 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, NUMERALS;
begin
reserve x for set;
definition
let x be object;
attr x is ext-real means
:: XXREAL_0:def 1
x in ExtREAL;
end;
registration
cluster ext-real for object;
cluster ext-real for number;
cluster -> ext-real for Element of ExtREAL;
end;
definition
mode ExtReal is ext-real Number;
end;
registration
sethood of ExtReal;
end;
definition
func +infty -> object equals
:: XXREAL_0:def 2
REAL;
func -infty -> object equals
:: XXREAL_0:def 3
[0,REAL];
end;
definition
redefine func ExtREAL equals
:: XXREAL_0:def 4
REAL \/ {+infty,-infty};
end;
registration
cluster +infty -> ext-real;
cluster -infty -> ext-real;
end;
definition
let x,y be ExtReal;
pred x <= y means
:: 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;
reflexivity;
connectedness;
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;
theorem :: XXREAL_0:1
for a,b being ExtReal holds a <= b & b <= a implies a = b;
theorem :: XXREAL_0:2
for a,b,c being ExtReal holds
a <= b & b <= c implies a <= c;
theorem :: XXREAL_0:3
a <= +infty;
theorem :: XXREAL_0:4
+infty <= a implies a = +infty;
theorem :: XXREAL_0:5
a >= -infty;
theorem :: XXREAL_0:6
-infty >= a implies a = -infty;
theorem :: XXREAL_0:7
-infty < +infty;
theorem :: XXREAL_0:8
not +infty in REAL;
theorem :: XXREAL_0:9
a in REAL implies +infty > a;
theorem :: XXREAL_0:10
a in REAL & b >= a implies b in REAL or b = +infty;
theorem :: XXREAL_0:11
not -infty in REAL;
theorem :: XXREAL_0:12
a in REAL implies -infty < a;
theorem :: XXREAL_0:13
a in REAL & b <= a implies b in REAL or b = -infty;
theorem :: XXREAL_0:14
a in REAL or a = +infty or a = -infty;
begin :: positive & negative
registration
cluster natural -> ext-real for object;
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
:: XXREAL_0:def 6
a > 0;
attr a is negative means
:: XXREAL_0:def 7
a < 0;
:: redefine attr a is zero means
:: a = 0;
:: compatibility;
::$CD
end;
registration
cluster positive -> non negative non zero for ExtReal;
cluster non negative non zero -> positive for ExtReal;
cluster negative -> non positive non zero for ExtReal;
cluster non positive non zero -> negative for ExtReal;
cluster zero -> non negative non positive for ExtReal;
cluster non negative non positive -> zero for ExtReal;
end;
registration
cluster +infty -> positive;
cluster -infty -> negative;
end;
registration
cluster positive for ExtReal;
cluster negative for ExtReal;
cluster zero for ExtReal;
end;
begin :: min & max
definition
let a,b be ExtReal;
func min(a,b) -> ExtReal equals
:: XXREAL_0:def 9
a if a <= b otherwise b;
commutativity;
idempotence;
func max(a,b) -> ExtReal equals
:: XXREAL_0:def 10
a if b <= a otherwise b;
commutativity;
idempotence;
end;
theorem :: XXREAL_0:15
min(a,b) = a or min(a,b) = b;
theorem :: XXREAL_0:16
max(a,b) = a or max(a,b) = b;
registration
let a,b;
cluster min(a,b) -> ext-real;
cluster max(a,b) -> ext-real;
end;
theorem :: XXREAL_0:17
min(a,b) <= a;
theorem :: XXREAL_0:18
a <= b & c <= d implies min(a,c) <= min(b,d);
theorem :: XXREAL_0:19
a < b & c < d implies min(a,c) < min(b,d);
theorem :: XXREAL_0:20
a <= b & a <= c implies a <= min(b,c);
theorem :: XXREAL_0:21
a < b & a < c implies a < min(b,c);
theorem :: XXREAL_0:22
a <= min(b,c) implies a <= b;
theorem :: XXREAL_0:23
a < min(b,c) implies a < b;
theorem :: XXREAL_0:24
c <= a & c <= b & (for d st d <= a & d <= b holds d <= c) implies c =
min(a,b);
theorem :: XXREAL_0:25
a <= max(a,b);
theorem :: XXREAL_0:26
a <= b & c <= d implies max(a,c) <= max(b,d);
theorem :: XXREAL_0:27
a < b & c < d implies max(a,c) < max(b,d);
theorem :: XXREAL_0:28
b <= a & c <= a implies max(b,c) <= a;
theorem :: XXREAL_0:29
b < a & c < a implies max(b,c) < a;
theorem :: XXREAL_0:30
max(b,c) <= a implies b <= a;
theorem :: XXREAL_0:31
max(b,c) < a implies b < a;
theorem :: XXREAL_0:32
a <= c & b <= c & (for d st a <= d & b <= d holds c <= d) implies c =
max(a,b);
theorem :: XXREAL_0:33
min(min(a,b),c) = min(a,min(b,c));
theorem :: XXREAL_0:34
max(max(a,b),c) = max(a,max(b,c));
theorem :: XXREAL_0:35
min(max(a,b),b) = b;
theorem :: XXREAL_0:36
max(min(a,b),b) = b;
theorem :: XXREAL_0:37
a <= c implies max(a,min(b,c)) = min(max(a,b),c);
theorem :: XXREAL_0:38
min(a,max(b,c)) = max(min(a,b),min(a,c));
theorem :: XXREAL_0:39
max(a,min(b,c)) = min(max(a,b),max(a,c));
theorem :: XXREAL_0:40
max(max(min(a,b),min(b,c)),min(c,a)) = min(min(max(a,b),max(b,c)),max( c,a));
theorem :: XXREAL_0:41
max(a,+infty) = +infty;
theorem :: XXREAL_0:42
min(a,+infty) = a;
theorem :: XXREAL_0:43
max(a,-infty) = a;
theorem :: XXREAL_0:44
min(a,-infty) = -infty;
begin :: Addenda
theorem :: XXREAL_0:45
a in REAL & c in REAL & a <= b & b <= c implies b in REAL;
theorem :: XXREAL_0:46
a in REAL & a <= b & b < c implies b in REAL;
theorem :: XXREAL_0:47
c in REAL & a < b & b <= c implies b in REAL;
theorem :: XXREAL_0:48
a < b & b < c implies b in REAL;
:: 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
:: XXREAL_0:def 11
a if x > y otherwise b;
end;
registration
let x,y be ExtReal, a,b be natural Number;
cluster IFGT(x,y,a,b) -> natural;
end;
:: from TOPREAL7, 2008.07.05, A.T.
theorem :: XXREAL_0:49
max(a,b) <= a implies max(a,b) = a;
theorem :: XXREAL_0:50
a <= min(a,b) implies min(a,b) = a;
registration let x be ExtReal;
reduce In(x,ExtREAL) to x;
end;