Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Schemes of Existence of Some Types of Functions

**by****Jaroslaw Kotowicz**- Received September 21, 1990
- MML identifier: SCHEME1

- [ Mizar article, MML identifier index ]

environ vocabulary NAT_1, SEQ_1, SEQM_3, FUNCT_1, RELAT_1, ORDINAL2, ARYTM_3, ARYTM_1, PARTFUN1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, SEQ_1, SEQM_3; constructors NAT_1, SEQ_1, SEQM_3, PARTFUN1, MEMBERED, XBOOLE_0; clusters RELSET_1, XREAL_0, SEQM_3, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin reserve x,y,z for set; reserve n,m,k for Nat; reserve r for Real; theorem :: SCHEME1:1 for n ex m st n = 2*m or n = 2*m+1; theorem :: SCHEME1:2 for n ex m st n = 3*m or n = 3*m+1 or n = 3*m+2; theorem :: SCHEME1:3 for n ex m st n = 4*m or n = 4*m+1 or n = 4*m+2 or n = 4*m+3; theorem :: SCHEME1:4 for n ex m st n = 5*m or n = 5*m+1 or n = 5*m+2 or n = 5*m+3 or n = 5*m+4; scheme ExRealSubseq{s()->Real_Sequence,P[set]}: ex q being Real_Sequence st q is_subsequence_of s() & (for n holds P[q.n]) & for n st (for r st r = s().n holds P[r]) ex m st s().n = q.m provided for n ex m st n <= m & P[s().m]; scheme ExRealSeq2{F,G(set)->Real}: ex s being Real_Sequence st for n holds s.(2*n) = F(n) & s.(2*n+1) = G(n); scheme ExRealSeq3{F,G,H(set)->Real}: ex s being Real_Sequence st for n holds s.(3*n) = F(n) & s.(3*n+1) = G(n) & s.(3*n+2) = H(n); scheme ExRealSeq4{F,G,H,I(set)->Real}: ex s being Real_Sequence st for n holds s.(4*n) = F(n) & s.(4*n+1) = G(n) & s.(4*n+2) = H(n) & s.(4*n+3) = I(n); scheme ExRealSeq5{F,G,H,I,J(set)->Real}: ex s being Real_Sequence st for n holds s.(5*n) = F(n) & s.(5*n+1) = G(n) & s.(5*n+2) = H(n) & s.(5*n+3) = I(n) & s.(5*n+4) = J(n); scheme PartFuncExD2{C, D()->non empty set, P,Q[set], F,G(set)->Element of D()}: ex f being PartFunc of C(),D() st (for c be Element of C() holds c in dom f iff P[c] or Q[c]) & (for c be Element of C() st c in dom f holds (P[c] implies f.c = F(c)) & (Q[c] implies f.c = G(c))) provided for c be Element of C() st P[c] holds not Q[c]; scheme PartFuncExD2'{C, D()->non empty set,P,Q[set], F,G(set)->Element of D()}: ex f being PartFunc of C(),D() st (for c be Element of C() holds c in dom f iff P[c] or Q[c]) & (for c be Element of C() st c in dom f holds (P[c] implies f.c = F(c)) & (Q[c] implies f.c = G(c))) provided for c be Element of C() st P[c] & Q[c] holds F(c)=G(c); scheme PartFuncExD2''{C, D()->non empty set,P[set], F,G(set)->Element of D()}: ex f being PartFunc of C(),D() st f is total & (for c be Element of C() st c in dom f holds (P[c] implies f.c = F(c)) & (not P[c] implies f.c = G(c))); scheme PartFuncExD3{C, D()->non empty set,P,Q,R[set], F,G,H(set)->Element of D()}: ex f being PartFunc of C(),D() st (for c be Element of C() holds c in dom f iff P[c] or Q[c] or R[c]) & (for c be Element of C() st c in dom f holds (P[c] implies f.c = F(c)) & (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c))) provided for c be Element of C() holds (P[c] implies not Q[c]) & (P[c] implies not R[c]) & (Q[c] implies not R[c]); scheme PartFuncExD3'{C, D()->non empty set,P,Q,R[set], F,G,H(set)->Element of D()}: ex f being PartFunc of C(),D() st (for c be Element of C() holds c in dom f iff P[c] or Q[c] or R[c]) & (for c be Element of C() st c in dom f holds (P[c] implies f.c = F(c)) & (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c))) provided for c be Element of C() holds (P[c] & Q[c] implies F(c)=G(c)) & (P[c] & R[c] implies F(c)=H(c)) & (Q[c] & R[c] implies G(c)=H(c)); scheme PartFuncExD4{C, D()->non empty set,P,Q,R,S[set], F,G,H,I(set)->Element of D()}: ex f being PartFunc of C(),D() st (for c be Element of C() holds c in dom f iff P[c] or Q[c] or R[c] or S[c]) & (for c be Element of C() st c in dom f holds (P[c] implies f.c = F(c)) & (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c)) & (S[c] implies f.c = I(c))) provided for c be Element of C() holds (P[c] implies not Q[c]) & (P[c] implies not R[c]) & (P[c] implies not S[c]) & (Q[c] implies not R[c]) & (Q[c] implies not S[c]) & (R[c] implies not S[c]); scheme PartFuncExS2{X, Y()->set,P,Q[set],F,G(set)->set}: ex f being PartFunc of X(),Y() st (for x holds x in dom f iff x in X() & (P[x] or Q[x])) & (for x st x in dom f holds (P[x] implies f.x=F(x)) & (Q[x] implies f.x=G(x))) provided for x st x in X() holds P[x] implies not Q[x] and for x st x in X() & P[x] holds F(x) in Y() and for x st x in X() & Q[x] holds G(x) in Y(); scheme PartFuncExS3{X, Y()->set,P,Q,R[set], F,G,H(set)->set}: ex f being PartFunc of X(),Y() st (for x holds x in dom f iff x in X() & (P[x] or Q[x] or R[x])) & (for x st x in dom f holds (P[x] implies f.x=F(x)) & (Q[x] implies f.x=G(x)) & (R[x] implies f.x=H(x))) provided for x st x in X() holds (P[x] implies not Q[x]) & (P[x] implies not R[x]) & (Q[x] implies not R[x]) and for x st x in X() & P[x] holds F(x) in Y() and for x st x in X() & Q[x] holds G(x) in Y() and for x st x in X() & R[x] holds H(x) in Y(); scheme PartFuncExS4{X, Y()->set,P,Q,R,S[set], F,G,H,I(set)->set}: ex f being PartFunc of X(),Y() st (for x holds x in dom f iff x in X() & (P[x] or Q[x] or R[x] or S[x])) & (for x st x in dom f holds (P[x] implies f.x=F(x)) & (Q[x] implies f.x=G(x)) & (R[x] implies f.x=H(x)) & (S[x] implies f.x=I(x))) provided for x st x in X() holds (P[x] implies not Q[x]) & (P[x] implies not R[x]) & (P[x] implies not S[x]) & (Q[x] implies not R[x]) & (Q[x] implies not S[x]) & (R[x] implies not S[x]) and for x st x in X() & P[x] holds F(x) in Y() and for x st x in X() & Q[x] holds G(x) in Y() and for x st x in X() & R[x] holds H(x) in Y() and for x st x in X() & S[x] holds I(x) in Y(); scheme PartFuncExC_D2{C, D, E()->non empty set, P,Q[set,set], F,G(set,set)->Element of E()}: ex f being PartFunc of [:C(),D():],E() st (for c be Element of C() ,d be Element of D() holds [c,d] in dom f iff P[c,d] or Q[c,d]) & for c be Element of C() ,d be Element of D() st [c,d] in dom f holds (P[c,d] implies f.[c,d]=F(c,d)) & (Q[c,d] implies f.[c,d]=G(c,d)) provided for c be Element of C() ,d be Element of D() st P[c,d] holds not Q[c,d]; scheme PartFuncExC_D3{C, D, E()->non empty set, P,Q,R[set,set], F,G,H(set,set)->Element of E()}: ex f being PartFunc of [:C(),D():],E() st (for c be Element of C() ,d be Element of D() holds [c,d] in dom f iff P[c,d] or Q[c,d] or R[c,d]) & for c be Element of C() ,r be Element of D() st [c,r] in dom f holds (P[c,r] implies f.[c,r]=F(c,r)) & (Q[c,r] implies f.[c,r]=G(c,r)) & (R[c,r] implies f.[c,r]=H(c,r)) provided for c be Element of C() ,s be Element of D() holds (P[c,s] implies not Q[c,s]) & (P[c,s] implies not R[c,s]) & (Q[c,s] implies not R[c,s]); scheme PartFuncExC_S2{X, Y, Z()->set,P,Q[set,set], F,G(set,set)->set}: ex f being PartFunc of [:X(),Y():],Z() st (for x,y holds [x,y] in dom f iff x in X() & y in Y() & (P[x,y] or Q[x,y])) & (for x,y st [x,y] in dom f holds (P[x,y] implies f.[x,y]=F(x,y)) & (Q[x,y] implies f.[x,y]=G(x,y))) provided for x,y st x in X() & y in Y() holds P[x,y] implies not Q[x,y] and for x,y st x in X() & y in Y() & P[x,y] holds F(x,y) in Z() and for x,y st x in X() & y in Y() & Q[x,y] holds G(x,y) in Z(); scheme PartFuncExC_S3{X, Y, Z()->set, P,Q,R[set,set], F,G,H(set,set)->set}: ex f being PartFunc of [:X(),Y():],Z() st (for x,y holds [x,y] in dom f iff x in X() & y in Y() & (P[x,y] or Q[x,y] or R[x,y])) & (for x,y st [x,y] in dom f holds (P[x,y] implies f.[x,y]=F(x,y)) & (Q[x,y] implies f.[x,y]=G(x,y)) & (R[x,y] implies f.[x,y]=H(x,y))) provided for x,y st x in X() & y in Y() holds (P[x,y] implies not Q[x,y]) & (P[x,y] implies not R[x,y]) & (Q[x,y] implies not R[x,y]) and for x,y st x in X() & y in Y() holds P[x,y] implies F(x,y) in Z() and for x,y st x in X() & y in Y() holds Q[x,y] implies G(x,y) in Z() and for x,y st x in X() & y in Y() holds R[x,y] implies H(x,y) in Z(); scheme ExFuncD3{C, D()->non empty set,P,Q,R[set], F,G,H(set)->Element of D()}: ex f being Function of C(),D() st for c be Element of C() holds (P[c] implies f.c = F(c)) & (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c)) provided for c be Element of C() holds (P[c] implies not Q[c]) & (P[c] implies not R[c]) & (Q[c] implies not R[c]) and for c be Element of C() holds P[c] or Q[c] or R[c]; scheme ExFuncD4{C, D()->non empty set, P,Q,R,S[set], F,G,H,I(set)->Element of D()}: ex f being Function of C(),D() st for c be Element of C() holds (P[c] implies f.c = F(c)) & (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c)) & (S[c] implies f.c = I(c)) provided for c be Element of C() holds (P[c] implies not Q[c]) & (P[c] implies not R[c]) & (P[c] implies not S[c]) & (Q[c] implies not R[c]) & (Q[c] implies not S[c]) & (R[c] implies not S[c]) and for c be Element of C() holds P[c] or Q[c] or R[c] or S[c]; scheme FuncExC_D2{C, D, E()->non empty set,P[set,set], F,G(set,set)->Element of E()}: ex f being Function of [:C(),D():],E() st for c be Element of C() ,d be Element of D() st [c,d] in dom f holds (P[c,d] implies f.[c,d]=F(c,d)) & (not P[c,d] implies f.[c,d]=G(c,d)); scheme FuncExC_D3{C, D, E()->non empty set, P,Q,R[set,set], F,G,H(set,set)->Element of E()}: ex f being Function of [:C(),D():],E() st (for c be Element of C() ,d be Element of D() holds [c,d] in dom f iff P[c,d] or Q[c,d] or R[c,d]) & for c be Element of C() ,d be Element of D() st [c,d] in dom f holds (P[c,d] implies f.[c,d]=F(c,d)) & (Q[c,d] implies f.[c,d]=G(c,d)) & (R[c,d] implies f.[c,d]=H(c,d)) provided for c be Element of C() ,d be Element of D() holds (P[c,d] implies not Q[c,d]) & (P[c,d] implies not R[c,d]) & (Q[c,d] implies not R[c,d]) and for c be Element of C() ,d be Element of D() holds P[c,d] or Q[c,d] or R[c,d];

Back to top