:: Schemes of Existence of some Types of Functions
:: by Jaros{\l}aw Kotowicz
::
:: Received September 21, 1990
:: Copyright (c) 1990-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, SUBSET_1, REAL_1, RELAT_1, ARYTM_3, INT_1, CARD_1,
XXREAL_0, SEQ_1, VALUED_0, FUNCT_1, NAT_1, TARSKI, ORDINAL2, ARYTM_1,
XBOOLE_0, PARTFUN1, ZFMISC_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, NAT_1, NAT_D, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
VALUED_0, SEQ_1, XXREAL_0, RECDEF_1;
constructors PARTFUN1, XXREAL_0, NAT_1, NAT_D, SEQM_3, RECDEF_1, MEMBERED,
RELSET_1, NUMBERS;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, SEQM_3,
VALUED_0;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin
reserve x,y,z for object;
reserve n,m,k for Element of NAT;
reserve r for Real;
theorem :: SCHEME1:1
for n being Nat 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 :: SCHEME1:sch 1
ExRealSubseq{s()->Real_Sequence,P[object]}:
ex q being Real_Sequence st q is
subsequence of s() & (for n being Nat 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 :: SCHEME1:sch 2
ExRealSeq2{F,G(set)->Element of REAL}:
ex s being Real_Sequence st for n holds s.(2*n) = F(n) & s.(2*n+1) = G(n);
scheme :: SCHEME1:sch 3
ExRealSeq3{F,G,H(set)-> Element of 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 :: SCHEME1:sch 4
ExRealSeq4{F,G,H,I(set)->Element of 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 :: SCHEME1:sch 5
ExRealSeq5{F,G,H,I,J(set)->Element of 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 :: SCHEME1:sch 6
PartFuncExD2{C, D()->non empty set, P,Q[object],
F,G(object)->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 :: SCHEME1:sch 7
PartFuncExD29{C, D()->non empty set,P,Q[object],
F,G(object)->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 :: SCHEME1:sch 8
PartFuncExD299{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 :: SCHEME1:sch 9
PartFuncExD3{C, D()->non empty set,P,Q,R[object],
F,G,H(object)->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 :: SCHEME1:sch 10
PartFuncExD39{C, D()->non empty set,P,Q,R[object],
F,G,H(object)->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 :: SCHEME1:sch 11
PartFuncExD4{C, D()->non empty set,P,Q,R,S[object],
F,G,H,I(object)->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 :: SCHEME1:sch 12
PartFuncExS2{X, Y()->set,P,Q[object],F,G(object)->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 :: SCHEME1:sch 13
PartFuncExS3{X, Y()->set,P,Q,R[object], F,G,H(object)->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 :: SCHEME1:sch 14
PartFuncExS4{X, Y()->set,P,Q,R,S[object], F,G,H,I(object)->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 :: SCHEME1:sch 15
PartFuncExCD2{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 :: SCHEME1:sch 16
PartFuncExCD3{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 :: SCHEME1:sch 17
PartFuncExCS2{X, Y, Z()->set,P,Q[object,object],
F,G(object,object)->object}:
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 :: SCHEME1:sch 18
PartFuncExCS3{X, Y, Z()->set, P,Q,R[object,object],
F,G,H(object,object)->object}:
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 :: SCHEME1:sch 19
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 :: SCHEME1:sch 20
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 :: SCHEME1:sch 21
FuncExCD2{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 :: SCHEME1:sch 22
FuncExCD3{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];