:: Introduction to Arithmetic of Extended Real Numbers :: by Library Committee :: :: Received January 4, 2006 :: Copyright (c) 2006-2018 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;