:: Miscellaneous Facts about Functions
:: by Grzegorz Bancerek and Andrzej Trybulec
::
:: Received January 12, 1996
:: Copyright (c) 1996-2017 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, FUNCT_1, RELAT_1, TARSKI, XBOOLE_0, FUNCOP_1,
PBOOLE, ZFMISC_1, FUNCT_4, FINSEQ_1, ARYTM_3, CARD_1, NAT_1, XXREAL_0,
FINSET_1, SETFAM_1, FINSEQ_2, ORDINAL4, MCART_1, PARTFUN1, REWRITE1,
FUNCT_2, ARYTM_1, RFINSEQ, CLASSES1, FUNCT_7, VALUED_1, ORDINAL1;
notations TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, XTUPLE_0, SUBSET_1, CARD_1,
WELLORD2, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, SETFAM_1, PBOOLE,
DOMAIN_1, RELAT_1, FUNCT_1, RELSET_1, BINOP_1, FINSET_1, PARTFUN1,
FUNCOP_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FUNCT_4, CLASSES1, RFINSEQ, NAT_D,
REWRITE1, VALUED_1;
constructors SETFAM_1, PARTFUN1, WELLORD2, BINOP_1, DOMAIN_1, FUNCT_4,
XXREAL_0, NAT_1, INT_1, PBOOLE, RFINSEQ, NAT_D, REWRITE1, RELAT_2,
REAL_1, CLASSES1, RELSET_1, VALUED_1, FINSEQ_2, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1,
FUNCOP_1, FUNCT_4, XREAL_0, NAT_1, INT_1, CARD_1, FINSEQ_1, FUNCT_2,
RELSET_1, XXREAL_0, XTUPLE_0, FINSEQ_3;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
reserve a,x,y for object, A,B for set,
l,m,n for Nat;
theorem :: FUNCT_7:1
for f being Function, X being set st rng f c= X holds (id X)*f = f;
theorem :: FUNCT_7:2
for X being set, Y being non empty set, f being Function of X,Y st f
is one-to-one for B being Subset of X, C being Subset of Y st C c= f.:B holds f
"C c= B;
theorem :: FUNCT_7:3
for X,Y be non empty set, f being Function of X,Y st f is
one-to-one for x being Element of X, A being Subset of X st f.x in f.:A holds x
in A;
theorem :: FUNCT_7:4
for X,Y be non empty set, f being Function of X,Y st f is
one-to-one for x being Element of X, A being Subset of X, B being Subset of Y
st f.x in f.:A \ B holds x in A \ f"B;
theorem :: FUNCT_7:5
for X,Y be non empty set, f being Function of X,Y st f is one-to-one
for y being Element of Y, A being Subset of X, B being Subset of Y st y in f.:A
\ B holds f".y in A \ f"B;
theorem :: FUNCT_7:6
for f being Function, a being set st a in dom f holds f|{a} = a
.--> f.a;
registration
let x,y be object;
cluster x .--> y -> non empty;
end;
registration
let x,y,a,b be object;
cluster (x,y) --> (a,b) -> non empty;
end;
theorem :: FUNCT_7:7
for I being set, M being ManySortedSet of I for i being set st i
in I holds i.--> (M.i) = M|{i};
theorem :: FUNCT_7:8
for I,J being set, M being ManySortedSet of [:I,J:] for i,j being set
st i in I & j in J holds (i,j):-> (M.(i,j)) = M|([:{i},{j}:] qua set);
theorem :: FUNCT_7:9
for f,g,h being Function st rng h c= dom f holds f*(g +* h) = (f
*g) +* (f*h);
theorem :: FUNCT_7:10
for f,g,h being Function holds (g +* h)*f = (g*f) +* (h*f);
theorem :: FUNCT_7:11
for f,g,h being Function st rng f misses dom g holds (h +* g)*f = h*f;
theorem :: FUNCT_7:12
for A,B be set, y be set st A meets rng(id B +* (A --> y)) holds
y in A;
theorem :: FUNCT_7:13
for x,y be set, A be set st x <> y holds not x in rng(id A +* (x .-->
y));
theorem :: FUNCT_7:14
for X being set, a being set, f being Function st dom f = X \/ {a}
holds f = f|X +* (a .--> f.a);
theorem :: FUNCT_7:15
for f being Function, X,y,z being set holds (f+*(X-->y))+*(X-->z) = f
+*(X-->z);
theorem :: FUNCT_7:16
INT <> INT*;
theorem :: FUNCT_7:17
{}* = {{}};
theorem :: FUNCT_7:18
for x being object holds <*x*> in A* iff x in A;
theorem :: FUNCT_7:19
A* c= B* implies A c= B;
theorem :: FUNCT_7:20
for A being Subset of NAT st for n,m st n in A & m < n holds m in A
holds A is Cardinal;
theorem :: FUNCT_7:21
for A being finite set, X being non empty Subset-Family of A ex C
being Element of X st for B being Element of X holds B c= C implies B = C;
theorem :: FUNCT_7:22
for p,q being FinSequence st len p = len q+1
for i being Nat holds i in dom q iff i in dom p & i+1 in dom p;
registration
cluster Function-yielding non empty non-empty for FinSequence;
end;
registration
cluster empty -> Function-yielding for Function;
end;
registration
let n be Nat, f be Function;
cluster n |-> f -> Function-yielding;
end;
registration
let p,q be Function-yielding FinSequence;
cluster p^q -> Function-yielding;
end;
theorem :: FUNCT_7:23
for p,q being FinSequence st p^q is Function-yielding holds p is
Function-yielding & q is Function-yielding;
begin :: Some useful schemes
scheme :: FUNCT_7:sch 1
Kappa2D{ X,Y,Z()->non empty set,F(Element of X(),Element of Y())->object}:
ex f being Function of [:X(),Y():], Z() st
for x being Element of X(), y being Element of Y() holds f.(x,y)=F(x,y)
provided
for x being Element of X(), y being Element of Y() holds F(x,y) in Z
();
scheme :: FUNCT_7:sch 2
FinMono{ A() -> set, D() -> non empty set, F,G(object) -> object }:
{ F(d) where d
is Element of D() : G(d) in A() } is finite
provided
A() is finite and
for d1,d2 being Element of D() st G(d1) = G(d2) holds d1 = d2;
scheme :: FUNCT_7:sch 3
CardMono{ A() -> set, D() -> non empty set, G(object) -> object }:
A(),{ d where d is Element of D() : G(d) in A() } are_equipotent
provided
for x being set st x in A() ex d being Element of D() st x = G(d) and
for d1,d2 being Element of D() st G(d1) = G(d2) holds d1 = d2;
scheme :: FUNCT_7:sch 4
CardMono9{ A() -> set, D() -> non empty set, G(object) -> object }:
A(),{ G(d) where d is Element of D() : d in A() } are_equipotent
provided
A() c= D() and
for d1,d2 being Element of D() st G(d1) = G(d2) holds d1 = d2;
scheme :: FUNCT_7:sch 5
FuncSeqInd {P[object]}: for p being Function-yielding FinSequence holds P[p]
provided
P[ {} ] and
for p being Function-yielding FinSequence st P[p] for f being
Function holds P[p^<*f*>];
begin :: Some auxiliary concepts
definition
::$CD
let f,g be Function;
let A be set;
pred f,g equal_outside A means
:: FUNCT_7:def 2
f|(dom f \ A) = g|(dom g \ A);
end;
::$CT
theorem :: FUNCT_7:25
for f be Function, A be set holds f,f equal_outside A;
theorem :: FUNCT_7:26
for f,g be Function, A be set st f,g equal_outside A holds g,f
equal_outside A;
theorem :: FUNCT_7:27
for f,g,h be Function, A be set st f,g equal_outside A & g,h
equal_outside A holds f,h equal_outside A;
theorem :: FUNCT_7:28
for f,g be Function, A be set st f,g equal_outside A holds dom f
\ A = dom g \ A;
theorem :: FUNCT_7:29
for f,g being Function, A be set st dom g c= A holds f, f +* g
equal_outside A;
definition
let f be Function, i, x be object;
func f+*(i,x) -> Function equals
:: FUNCT_7:def 3
f+*(i.-->x) if i in dom f otherwise
f;
end;
theorem :: FUNCT_7:30
for f be Function, d,i be object holds dom(f+*(i,d)) = dom f;
registration
let f be empty Function, i, x be object;
cluster f+*(i,x) -> empty;
end;
registration
let f be non empty Function, i, x be object;
cluster f+*(i,x) -> non empty;
end;
theorem :: FUNCT_7:31
for f be Function, d,i be object st i in dom f holds (f+*(i,d)).i = d;
theorem :: FUNCT_7:32
for f be Function, d,i,j be object st i <> j holds (f+*(i,d)).j = f.j;
theorem :: FUNCT_7:33
for f be Function, d,e,i,j be set st i <> j holds f+*(i,d)+*(j,e) = f
+*(j,e)+*(i,d);
theorem :: FUNCT_7:34
for f be Function, d,e,i be set holds f+*(i,d)+*(i,e) = f+*(i,e);
theorem :: FUNCT_7:35
for f be Function, i be set holds f+*(i,f.i) = f;
registration
let f be FinSequence, i,x be object;
cluster f+*(i,x) -> FinSequence-like;
end;
definition
let D be set, f be FinSequence of D, i be Nat, d be Element of D;
redefine func f+*(i,d) -> FinSequence of D;
end;
theorem :: FUNCT_7:36
for D be non empty set, f be FinSequence of D, d be Element of D, i be
Nat st i in dom f holds (f+*(i,d))/.i = d;
theorem :: FUNCT_7:37
for D be non empty set, f be FinSequence of D, d be Element of D, i,j
be Nat st i <> j & j in dom f holds (f+*(i,d))/.j = f/.j;
theorem :: FUNCT_7:38
for D be non empty set, f be FinSequence of D, d,e be Element of D, i
be Nat holds f+*(i,f/.i) = f;
begin :: On the composition of a finite sequence of functions
definition
let X be set;
let p be Function-yielding FinSequence;
func compose(p,X) -> Function means
:: FUNCT_7:def 4
ex f being ManySortedFunction of
NAT st it = f.len p & f.0 = id X & for i being Nat st i+1 in dom p
for g,h being Function st g = f.i & h = p.(i+1) holds f.(i+1) = h*g;
end;
definition
let p be Function-yielding FinSequence;
let x be object;
func apply(p,x) -> FinSequence means
:: FUNCT_7:def 5
len it = len p+1 & it.1 = x &
for i being Nat, f being Function st i in dom p & f = p.i holds it.(
i+1) = f.(it.i);
end;
reserve X,Y for set, x for object,
p,q for Function-yielding FinSequence,
f,g,h for Function;
theorem :: FUNCT_7:39
compose({},X) = id X;
theorem :: FUNCT_7:40
apply({},x) = <*x*>;
theorem :: FUNCT_7:41
compose(p^<*f*>,X) = f*compose(p,X);
theorem :: FUNCT_7:42
apply(p^<*f*>,x) = apply(p,x)^<*f.(apply(p,x).(len p+1))*>;
theorem :: FUNCT_7:43
compose(<*f*>^p,X) = compose(p,f.:X)*(f|X);
theorem :: FUNCT_7:44
apply(<*f*>^p,x) = <*x*>^apply(p,f.x);
theorem :: FUNCT_7:45
compose(<*f*>,X) = f*id X;
theorem :: FUNCT_7:46
dom f c= X implies compose(<*f*>,X) = f;
theorem :: FUNCT_7:47
apply(<*f*>,x) = <*x,f.x*>;
theorem :: FUNCT_7:48
rng compose(p,X) c= Y implies compose(p^q,X) = compose(q,Y)*compose(p,
X );
theorem :: FUNCT_7:49
apply(p^q,x).(len (p^q)+1) = apply(q,apply(p,x).(len p+1)).(len
q+1);
theorem :: FUNCT_7:50
apply(p^q,x) = apply(p,x)$^apply(q,apply(p,x).(len p+1));
theorem :: FUNCT_7:51
compose(<*f,g*>,X) = g*f*id X;
theorem :: FUNCT_7:52
dom f c= X or dom(g*f) c= X implies compose(<*f,g*>,X) = g*f;
theorem :: FUNCT_7:53
apply(<*f,g*>,x) = <*x,f.x,g.(f.x)*>;
theorem :: FUNCT_7:54
compose(<*f,g,h*>,X) = h*g*f*id X;
theorem :: FUNCT_7:55
dom f c= X or dom(g*f) c= X or dom(h*g*f) c= X implies compose(<*f,g,h
*>,X) = h*g*f;
theorem :: FUNCT_7:56
apply(<*f,g,h*>,x) = <*x*>^<*f.x,g.(f.x),h.(g.(f.x))*>;
definition
let F be FinSequence;
func firstdom F -> set means
:: FUNCT_7:def 6
it is empty if F is empty otherwise it = proj1
(F.1);
func lastrng F -> set means
:: FUNCT_7:def 7
it is empty if F is empty otherwise it = proj2
(F.len F);
end;
theorem :: FUNCT_7:57
firstdom {} = {} & lastrng {} = {};
theorem :: FUNCT_7:58
for p being FinSequence holds firstdom (<*f*>^p) = dom f &
lastrng (p^<*f*>) = rng f;
theorem :: FUNCT_7:59
for p being Function-yielding FinSequence st p <> {} holds rng
compose(p,X) c= lastrng p;
definition
let IT be FinSequence;
attr IT is FuncSeq-like means
:: FUNCT_7:def 8
ex p being FinSequence st len p = len
IT+1 & for i being Nat st i in dom IT holds IT.i in Funcs(p.i, p.(i+
1));
end;
theorem :: FUNCT_7:60
for p,q being FinSequence st p^q is FuncSeq-like holds p is
FuncSeq-like & q is FuncSeq-like;
registration
cluster FuncSeq-like -> Function-yielding for FinSequence;
end;
registration
cluster empty -> FuncSeq-like for FinSequence;
end;
registration
let f be Function;
cluster <*f*> -> FuncSeq-like;
end;
registration
cluster FuncSeq-like non empty non-empty for FinSequence;
end;
definition
mode FuncSequence is FuncSeq-like FinSequence;
end;
theorem :: FUNCT_7:61
for p being FuncSequence st p <> {} holds dom compose(p,X) = (
firstdom p) /\ X;
theorem :: FUNCT_7:62
for p being FuncSequence holds dom compose(p,firstdom p) =
firstdom p;
theorem :: FUNCT_7:63
for p being FuncSequence, f being Function st rng f c= firstdom p
holds <*f*>^p is FuncSequence;
theorem :: FUNCT_7:64
for p being FuncSequence, f being Function st lastrng p c= dom f holds
p^<*f*> is FuncSequence;
theorem :: FUNCT_7:65
for p being FuncSequence st x in firstdom p & x in X holds apply(p,x).
(len p+1) = compose(p,X).x;
definition
let X,Y be set such that
Y is empty implies X is empty;
mode FuncSequence of X,Y -> FuncSequence means
:: FUNCT_7:def 9
firstdom it = X &
lastrng it c= Y;
end;
definition
let Y be non empty set, X be set;
let F be FuncSequence of X,Y;
redefine func compose(F,X) -> Function of X,Y;
end;
definition
let q be non-empty non empty FinSequence;
mode FuncSequence of q -> FinSequence means
:: FUNCT_7:def 10
len it+1 = len q & for i
being Nat st i in dom it holds it.i in Funcs(q.i,q.(i+1));
end;
registration
let q be non-empty non empty FinSequence;
cluster -> FuncSeq-like non-empty for FuncSequence of q;
end;
theorem :: FUNCT_7:66
for q being non-empty non empty FinSequence, p being
FuncSequence of q st p <> {} holds firstdom p = q.1 & lastrng p c= q.len q;
theorem :: FUNCT_7:67
for q being non-empty non empty FinSequence, p being FuncSequence of q
holds dom compose(p,q.1) = q.1 & rng compose(p,q.1) c= q.len q;
:: Moved from FUNCT_4
registration
let X be set;
let f be sequence of bool [:X,X:];
let n be Nat;
cluster f.n -> Relation-like;
end;
definition
let f be Relation;
let n be Nat;
func iter (f,n) -> Relation means
:: FUNCT_7:def 11
ex p being sequence of bool [:field f,field f:] st
it = p.n & p.0 = id(field f) &
for k being Nat holds p.(k+1) = f*(p.k);
end;
registration
let f be Function;
let n be Nat;
cluster iter (f,n) -> Function-like;
end;
reserve m,n,k for Nat, R for Relation;
theorem :: FUNCT_7:68
iter (R,0) = id(field R);
theorem :: FUNCT_7:69
for n be Nat holds iter(R,n+1) = R*iter(R,n);
theorem :: FUNCT_7:70
iter(R,1) = R;
theorem :: FUNCT_7:71
for n being Nat holds iter(R,n+1) = iter(R,n)*R;
theorem :: FUNCT_7:72
dom iter(R,n) c= field R & rng iter(R,n) c= field R;
theorem :: FUNCT_7:73
n <> 0 implies dom iter(R,n) c= dom R & rng iter(R,n) c= rng R;
theorem :: FUNCT_7:74
for n being Nat st rng R c= dom R holds dom iter(R,n) = dom R &
rng iter(R,n) c= dom R;
theorem :: FUNCT_7:75
id(field R)*iter(R,n) = iter(R,n);
theorem :: FUNCT_7:76
iter(R,n)*id(field R) = iter(R,n);
theorem :: FUNCT_7:77
iter(R,m)*iter(R,n) = iter(R,n+m);
theorem :: FUNCT_7:78
n <> 0 implies iter(iter(R,m),n) = iter(R,m*n);
theorem :: FUNCT_7:79
rng R c= dom R implies iter(iter(R,m),n) = iter(R,m*n);
theorem :: FUNCT_7:80
iter({},n) = {};
theorem :: FUNCT_7:81
iter(id(X),n) = id(X);
theorem :: FUNCT_7:82
rng R misses dom R implies iter(R,2) = {};
theorem :: FUNCT_7:83
for n being Nat for f being Function of X,X holds iter(f,n) is
Function of X,X;
theorem :: FUNCT_7:84
for f being Function of X,X holds iter(f,0) = id X;
theorem :: FUNCT_7:85
for f being Function of X,X holds iter(iter(f,m),n) = iter(f,m*n);
theorem :: FUNCT_7:86
for f being PartFunc of X,X holds iter(f,n) is PartFunc of X,X;
theorem :: FUNCT_7:87
n <> 0 & a in X & f = X --> a implies iter(f,n) = f;
theorem :: FUNCT_7:88
for f being Function, n being Nat holds iter(f,n) = compose
(n|->f,field f);
begin :: Addenda
:: from SCMFSA6A, 2006.03.14, A.T.
theorem :: FUNCT_7:89
for f,g being Function, x,y being set st g c= f & not x in dom g holds
g c= f+*(x,y);
theorem :: FUNCT_7:90
for f,g being Function, A being set st f|A = g|A & f,g equal_outside A
holds f = g;
theorem :: FUNCT_7:91
for f being Function, a,b,A being set st a in A holds f,f+*(a,b)
equal_outside A;
theorem :: FUNCT_7:92
for f being Function, a,b being object,
A being set holds a in A or (f+*(a,b))
|A = f|A;
theorem :: FUNCT_7:93
for f,g being Function, a,b be object,
A being set st f|A = g|A holds (f+*(a,b))|
A = (g+*(a,b))|A;
:: from YELLOW14, 2006.03.14, A.T.
theorem :: FUNCT_7:94
for f being Function, a, b being object holds (f +* (a .--> b)).a =
b;
:: from SCMFSA6A, 2006.03.14, A.T.
theorem :: FUNCT_7:95
for a, b being set holds <*a*> +* (1,b) = <*b*>;
:: from SCMFSA8C, 2006.03.15
theorem :: FUNCT_7:96
for f be Function, x be set st x in dom f holds f +* (x .--> f.x) = f;
:: from JORDAN2B, 2007.03.18, A.T.
reserve i,j for Nat;
theorem :: FUNCT_7:97
for w being FinSequence,r being object,i being natural Number
holds len (w+*(i,r))=len w;
theorem :: FUNCT_7:98
for D being non empty set, w being FinSequence of D, r being Element
of D st i in dom w holds w+*(i,r)=(w|(i-'1))^<*r*>^(w/^i);
:: comp. FINSEQ_7, 2007.03.18, A.T.
reserve F for Function,
e,x,y,z for object;
definition
let F;
let x,y be object;
func Swap(F,x,y) -> set equals
:: FUNCT_7:def 12
F+*(x,F.y)+*(y,F.x) if x in dom F & y in dom
F otherwise F;
end;
registration
let F;
let x,y be object;
cluster Swap(F,x,y) -> Relation-like Function-like;
end;
theorem :: FUNCT_7:99
for x,y being object holds dom Swap(F,x,y) = dom F;
theorem :: FUNCT_7:100
for x,y being object holds rng(F+*(x,y)) c= rng F \/ {y};
theorem :: FUNCT_7:101
for x,y being object holds rng F c= rng(F+*(x,y)) \/ {F.x};
theorem :: FUNCT_7:102
x in dom F implies y in rng(F+*(x,y));
theorem :: FUNCT_7:103
for x,y being object holds rng Swap(F,x,y) = rng F;
:: from SCMFSA_7, 2007.07.22, A.T.
scheme :: FUNCT_7:sch 6
{ A() -> set, D() -> non empty set, G(object) -> object }:
A(),{ G(d) where d is Element of D() : d in A() } are_equipotent
provided
A() c= D() and
for d1,d2 being Element of D() st d1 in A() & d2 in A() & G(d1) = G(
d2) holds d1 = d2;
:: from SCMFSA6A, 2007.07.23, A.T.
theorem :: FUNCT_7:104
for f,g,h being Function, A being set holds f, g equal_outside A
implies f +* h, g +* h equal_outside A;
theorem :: FUNCT_7:105
for f,g,h being Function, A being set holds f, g equal_outside A
implies h +* f, h +* g equal_outside A;
theorem :: FUNCT_7:106
for f,g,h being Function holds f +* h = g +* h iff f,g equal_outside
dom h;
:: from SF_MASTR, 2007.07.25, A.T.
theorem :: FUNCT_7:107
for x, y, a being object, f being Function st f.x = f.y holds f.a
= (f*((id dom f)+*(x,y))).a;
theorem :: FUNCT_7:108
for x, y being set, f being Function st x in dom f implies y in dom f
& f.x = f.y holds f = f*((id dom f)+*(x,y));
:: from SCMFSA8C, 2007.07.26, A.T.
theorem :: FUNCT_7:109
for f be Function, x be set st x in dom f holds f +* (x .--> f.x) = f;
:: from SFMASTR3, 2007.07.26, A.T.
theorem :: FUNCT_7:110
for X being set, p being Permutation of X, x, y being Element
of X holds p+*(x, p.y)+*(y, p.x) is Permutation of X;
theorem :: FUNCT_7:111
for f being Function, x, y being set st x in dom f & y in dom f ex p
being Permutation of dom f st f+*(x, f.y)+*(y, f.x) = f*p;
:: from SCMISORT, 2007.07.26, A.T.
theorem :: FUNCT_7:112
for f be Function,d,r be set st d in dom f holds dom f=dom (f+*(d.-->r
));
:: from SCMBISORT, 2007.07.26, A.T.
theorem :: FUNCT_7:113
for f,g be FinSequence of INT,m,n be Nat st 1<=n & n <= len
f & 1<=m & m <= len f & g=f+*(m,f/.n) +*(n,f/.m) holds f.m=g.n & f.n=g.m & (for
k be set st k<>m & k<>n & k in dom f holds f.k=g.k) & f,g
are_fiberwise_equipotent;
:: from SCMFSA10, 2007.07.27, A.T.
theorem :: FUNCT_7:114
for f being Function, a, A, b, B, c, C being set st a <> b & a <> c
holds ( f +* (a .--> A) +* (b .--> B) +* (c .--> C) ).a = A;
:: comp TOPALG_3:1, 2008.01.18, A.T.
theorem :: FUNCT_7:115
for A, B, a, b being set, f being Function of A,B st b in B
holds f +* (a,b) is Function of A,B;
:: missing, 2008.03.23, A.T.
theorem :: FUNCT_7:116
rng f c= A implies f+~(x,y) = (id A+*(x,y))*f;
theorem :: FUNCT_7:117
(f+*g)+~(x,y) = f+~(x,y)+*(g+~(x,y));
definition
let a,b be set;
func a followed_by b -> set equals
:: FUNCT_7:def 13
(NAT --> b) +* (0,a);
end;
registration
let a,b be set;
cluster a followed_by b -> Function-like Relation-like;
end;
reserve a,b,c for set;
theorem :: FUNCT_7:118
dom(a followed_by b) = NAT;
definition
let X be non empty set;
let a,b be Element of X;
redefine func a followed_by b -> sequence of X;
end;
theorem :: FUNCT_7:119
(a followed_by b).0 = a;
theorem :: FUNCT_7:120
for n st n > 0 holds (a followed_by b).n = b;
:: from DYNKIN, 2008.09.24, A.T.
definition
let a,b,c be set;
func (a,b) followed_by c -> set equals
:: FUNCT_7:def 14
(NAT --> c) +* ((0,1) --> (a,b));
end;
registration
let a,b,c be set;
cluster (a,b) followed_by c -> Function-like Relation-like;
end;
theorem :: FUNCT_7:121
dom (a,b) followed_by c = NAT;
theorem :: FUNCT_7:122
((a,b) followed_by c).0 = a;
theorem :: FUNCT_7:123
((a,b) followed_by c).1 = b;
theorem :: FUNCT_7:124
for n st n > 1 holds ((a,b) followed_by c).n = c;
theorem :: FUNCT_7:125
(a,b) followed_by c = (a followed_by c) +* (1,b);
definition
let X be non empty set;
let a,b,c be Element of X;
redefine func (a,b) followed_by c -> sequence of X;
end;
theorem :: FUNCT_7:126
rng(a followed_by b) = {a,b};
theorem :: FUNCT_7:127
rng (a,b) followed_by c = {a,b,c};
:: from POLYNOM1, 2008.12.15, A.T.
definition
let A, B be set, f be Function of A, B, x be set, y be Element of B;
redefine func f+*(x,y) -> Function of A, B;
end;
:: missing, 2008.12.14, A.T.
theorem :: FUNCT_7:128
for A, B being non empty set, f being Function of A, B, x being
Element of A, y being set holds f+*(x,y).x = y;
theorem :: FUNCT_7:129
for A, B being non empty set, f,g being Function of A, B, x being
Element of A st for y being Element of A st f.y <> g.y holds y = x holds f = g
+*(x,f.x);
theorem :: FUNCT_7:130
for g being A-defined Function holds f,f+*g equal_outside A;
theorem :: FUNCT_7:131
for f,g being A-defined Function holds f,g equal_outside A;
theorem :: FUNCT_7:132
for f,g being A-defined Function, h being Function
holds h+*f, h+*g equal_outside A;
theorem :: FUNCT_7:133
for I being NAT-defined Function holds card Shift(I,m) = card I;
theorem :: FUNCT_7:134
dom f = dom g & dom f c= A \/ B & f|B = g|B
implies f,g equal_outside A;
theorem :: FUNCT_7:135
dom f = dom g & B c= dom f & A misses B & f,g equal_outside A
implies f|B = g|B;
reserve A,B,I for set, X,Y for ManySortedSet of I;
theorem :: FUNCT_7:136
I c= A \/ B & X|B = Y|B implies X,Y equal_outside A;
theorem :: FUNCT_7:137
B c= I & A misses B & X,Y equal_outside A implies X|B = Y|B;
registration let V be non empty set;
let f be V-valued Function, x be object, y be Element of V;
cluster f+*(x,y) -> V-valued;
end;
theorem :: FUNCT_7:138
f c= g & not x in dom f implies f c= g+*(x,y);
theorem :: FUNCT_7:139
for I being non empty set, X being ManySortedSet of I,
l1,l2 being Element of I, i1,i2 being set
holds X +*((l1,l2) --> (i1, i2)) = X +* (l1,i1) +* (l2,i2);
scheme :: FUNCT_7:sch 7
Unionx { A()-> non empty set, a,b()-> Element of A(),
f() -> A()-valued Function,
x() -> object, F(object) -> object }:
{ F(i) where i is Element of A() : i in rng f()} =
{ F(j) where j is Element of A() : j in rng(f()+*(x(),a()))}
provided
F(b()) = F(a()) and
b() = f().x();