Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Basic Functions and Operations on Functions

by
Czeslaw Bylinski

MML identifier: FUNCT_3
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_1, RELAT_1, BOOLE, TARSKI, PARTFUN1, FUNCT_2, FUNCT_3;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1,
FUNCT_2;
constructors TARSKI, FUNCT_2, XBOOLE_0;
clusters FUNCT_1, RELSET_1, SUBSET_1, XBOOLE_0, ZFMISC_1;
requirements SUBSET, BOOLE;

begin

reserve p,q,x,x1,x2,y,y1,y2,z,z1,z2 for set;
reserve A,B,V,X,X1,X2,Y,Y1,Y2,Z for set;
reserve C,C1,C2,D,D1,D2 for non empty set;

theorem :: FUNCT_3:1
A c= Y implies id A = (id Y)|A;

theorem :: FUNCT_3:2
for f,g being Function st X c= dom(g*f) holds f.:X c= dom g;

theorem :: FUNCT_3:3
for f,g being Function st X c= dom f & f.:X c= dom g holds X c= dom(g*f);

theorem :: FUNCT_3:4
for f,g being Function
st Y c= rng(g*f) & g is one-to-one holds g"Y c= rng f;

theorem :: FUNCT_3:5
for f,g being Function st Y c= rng g & g"Y c= rng f holds Y c= rng(g*f);

scheme FuncEx_3{A()->set,B()-> set,P[set,set,set]}:
ex f being Function st dom f = [:A(),B():] &
for x,y st x in A() & y in B() holds P[x,y,f.[x,y]]
provided
for x,y,z1,z2 st x in A() & y in
B() & P[x,y,z1] & P[x,y,z2] holds z1 = z2 and
for x,y st x in A() & y in B() ex z st P[x,y,z];

scheme Lambda_3{A()->set,B()->set,F(set,set)->set}:
ex f being Function st dom f = [:A(),B():] &
for x,y st x in A() & y in B() holds f.[x,y] = F(x,y);

theorem :: FUNCT_3:6
for f,g being Function st dom f = [:X,Y:] & dom g = [:X,Y:] &
for x,y st x in X & y in Y holds f.[x,y] = g.[x,y]
holds f = g;

:: Function indicated by the image under a function

definition let f be Function;
func .:f -> Function means
:: FUNCT_3:def 1
dom it = bool dom f & for X st X c= dom f holds it.X = f.:X;
end;

canceled;

theorem :: FUNCT_3:8
for f being Function st X in dom(.:f) holds (.:f).X = f.:X;

theorem :: FUNCT_3:9
for f being Function holds (.:f).{} = {};

theorem :: FUNCT_3:10
for f being Function holds rng(.:f) c= bool rng f;

canceled;

theorem :: FUNCT_3:12
for f being Function holds (.:f).:A c= bool rng f;

theorem :: FUNCT_3:13
for f being Function holds (.:f)"B c= bool dom f;

theorem :: FUNCT_3:14
for f being Function of X,D holds (.:f)"B c= bool X;

theorem :: FUNCT_3:15
for f being Function holds union((.:f).:A) c= f.:(union A);

theorem :: FUNCT_3:16
for f being Function st A c= bool dom f holds f.:(union A) = union((.:f).:A)
;

theorem :: FUNCT_3:17
for f being Function of X,D st A c= bool X
holds f.:(union A) = union((.:f).:A);

theorem :: FUNCT_3:18
for f being Function holds union((.:f)"B) c= f"(union B);

theorem :: FUNCT_3:19
for f being Function st B c= bool rng f holds f"(union B) = union((.:f)"B)
;

theorem :: FUNCT_3:20
for f,g being Function holds .:(g*f) = .:g*.:f;

theorem :: FUNCT_3:21
for f being Function holds .:f is Function of bool dom f, bool rng f;

theorem :: FUNCT_3:22
for f being Function of X,Y st Y = {} implies X = {}
holds .:f is Function of bool X, bool Y;

definition let X,D; let f be Function of X,D;
redefine func .:f -> Function of bool X, bool D;
end;

:: Function indicated by the inverse image under a function

definition let f be Function;
func "f -> Function means
:: FUNCT_3:def 2
dom it = bool rng f & for Y st Y c= rng f holds it.Y = f"Y;
end;

canceled;

theorem :: FUNCT_3:24
for f being Function st Y in dom("f) holds ("f).Y = f"Y;

theorem :: FUNCT_3:25
for f being Function holds rng("f) c= bool dom f;

canceled;

theorem :: FUNCT_3:27
for f being Function holds ("f).:B c= bool dom f;

theorem :: FUNCT_3:28
for f being Function holds ("f)"A c= bool rng f;

theorem :: FUNCT_3:29
for f being Function holds union(("f).:B) c= f"(union B);

theorem :: FUNCT_3:30
for f being Function st B c= bool rng f holds union(("f).:B) = f"(union B)
;

theorem :: FUNCT_3:31
for f being Function holds union(("f)"A) c= f.:(union A);

theorem :: FUNCT_3:32
for f being Function st A c= bool dom f & f is one-to-one
holds union(("f)"A) = f.:(union A);

theorem :: FUNCT_3:33
for f being Function holds ("f).:B c= (.:f)"B;

theorem :: FUNCT_3:34
for f being Function st f is one-to-one holds ("f).:B = (.:f)"B;

theorem :: FUNCT_3:35
for f being Function,A be set st A c= bool dom f holds ("f)"A c= (.:f).:A;

theorem :: FUNCT_3:36
for f being Function,A be set st f is one-to-one holds (.:f).:A c= ("f)"A;

theorem :: FUNCT_3:37
for f being Function,A be set st f is one-to-one & A c= bool dom f
holds ("f)"A = (.:f).:A;

theorem :: FUNCT_3:38
for f,g being Function st g is one-to-one holds "(g*f) = "f*"g;

theorem :: FUNCT_3:39
for f being Function holds "f is Function of bool rng f, bool dom f;

:: Characteristic function

definition let A,X;
func chi(A,X) -> Function means
:: FUNCT_3:def 3
dom it = X &
for x st x in X
holds (x in A implies it.x = 1) & (not x in A implies it.x = 0);
end;

canceled 2;

theorem :: FUNCT_3:42
chi(A,X).x = 1 implies x in A;

theorem :: FUNCT_3:43
x in X \ A implies chi(A,X).x = 0;

canceled 3;

theorem :: FUNCT_3:47
A c= X & B c= X & chi(A,X) = chi(B,X) implies A = B;

theorem :: FUNCT_3:48
rng chi(A,X) c= {0,1};

theorem :: FUNCT_3:49
for f being Function of X,{0,1} holds f = chi(f"{1},X);

definition let A,X;
redefine func chi(A,X) -> Function of X,{0,1};
end;

definition
let Y; let A be Subset of Y;
func incl(A) -> Function of A,Y equals
:: FUNCT_3:def 4
id A;
end;

canceled 3;

theorem :: FUNCT_3:53
for A being Subset of Y holds incl A = (id Y)|A;

theorem :: FUNCT_3:54
for A being Subset of Y holds dom incl A = A & rng incl A = A;

theorem :: FUNCT_3:55
for A being Subset of Y st x in A holds (incl A).x = x;

theorem :: FUNCT_3:56
for A being Subset of Y st x in A holds incl(A).x in Y;

:: Projections

definition let X,Y;
func pr1(X,Y) -> Function means
:: FUNCT_3:def 5
dom it = [:X,Y:] & for x,y st x in X & y in Y holds it.[x,y] = x;
func pr2(X,Y) -> Function means
:: FUNCT_3:def 6
dom it = [:X,Y:] & for x,y st x in X & y in Y holds it.[x,y] = y;
end;

canceled 2;

theorem :: FUNCT_3:59
rng pr1(X,Y) c= X;

theorem :: FUNCT_3:60
Y <> {} implies rng pr1(X,Y) = X;

theorem :: FUNCT_3:61
rng pr2(X,Y) c= Y;

theorem :: FUNCT_3:62
X <> {} implies rng pr2(X,Y) = Y;

definition let X,Y; redefine
func pr1(X,Y) -> Function of [:X,Y:],X;
func pr2(X,Y) -> Function of [:X,Y:],Y;
end;

definition let X;
func delta(X) -> Function means
:: FUNCT_3:def 7
dom it = X & for x st x in X holds it.x = [x,x];
end;

canceled 3;

theorem :: FUNCT_3:66
rng delta X c= [:X,X:];

definition let X;
redefine func delta(X) -> Function of X,[:X,X:];
end;

:: Complex functions

definition let f,g be Function;
func <:f,g:> -> Function means
:: FUNCT_3:def 8
dom it = dom f /\ dom g & for x st x in dom it holds it.x = [f.x,g.x];
end;

canceled;

theorem :: FUNCT_3:68
for f,g being Function
st x in dom f /\ dom g holds <:f,g:>.x = [f.x,g.x];

theorem :: FUNCT_3:69
for f,g being Function
st dom f = X & dom g = X & x in X holds <:f,g:>.x = [f.x,g.x];

theorem :: FUNCT_3:70
for f,g being Function st dom f = X & dom g = X holds dom <:f,g:> = X;

theorem :: FUNCT_3:71
for f,g being Function holds rng <:f,g:> c= [:rng f,rng g:];

theorem :: FUNCT_3:72
for f,g being Function st dom f = dom g & rng f c= Y & rng g c= Z
holds pr1(Y,Z)*<:f,g:> = f & pr2(Y,Z)*<:f,g:> = g;

theorem :: FUNCT_3:73
<:pr1(X,Y),pr2(X,Y):> = id [:X,Y:];

theorem :: FUNCT_3:74
for f,g,h,k being Function
st dom f = dom g & dom k = dom h & <:f,g:> = <:k,h:> holds f = k & g = h;

theorem :: FUNCT_3:75
for f,g,h being Function holds <:f*h,g*h:> = <:f,g:>*h;

theorem :: FUNCT_3:76
for f,g being Function holds <:f,g:>.:A c= [:f.:A,g.:A:];

theorem :: FUNCT_3:77
for f,g being Function holds <:f,g:>"[:B,C:] = f"B /\ g"C;

theorem :: FUNCT_3:78
for f being Function of X,Y for g being Function of X,Z
st (Y = {} implies X = {}) & (Z = {} implies X = {})
holds <:f,g:> is Function of X,[:Y,Z:];

definition let X,D1,D2;
let f1 be Function of X,D1; let f2 be Function of X,D2;
redefine func <:f1,f2:> -> Function of X,[:D1,D2:];
end;

theorem :: FUNCT_3:79
for f1 being Function of C,D1 for f2 being Function of C,D2
for c being Element of C holds <:f1,f2:>.c = [f1.c,f2.c];

theorem :: FUNCT_3:80
for f being Function of X,Y for g being Function of X,Z
holds rng <:f,g:> c= [:Y,Z:];

theorem :: FUNCT_3:81
for f being Function of X,Y for g being Function of X,Z
st (Y = {} implies X = {}) & (Z = {} implies X = {})
holds pr1(Y,Z)*<:f,g:> = f & pr2(Y,Z)*<:f,g:> = g;

theorem :: FUNCT_3:82
for f being Function of X,D1 for g being Function of X,D2
holds pr1(D1,D2)*<:f,g:> = f & pr2(D1,D2)*<:f,g:> = g;

theorem :: FUNCT_3:83
for f1,f2 being Function of X,Y for g1,g2 being Function of X,Z
st (Y = {} implies X = {}) & (Z = {} implies X = {}) &
<:f1,g1:> = <:f2,g2:> holds f1 = f2 & g1 = g2;

theorem :: FUNCT_3:84
for f1,f2 being Function of X,D1 for g1,g2 being Function of X,D2
st <:f1,g1:> = <:f2,g2:> holds f1 = f2 & g1 = g2;

:: Product-functions

definition let f,g be Function;
func [:f,g:] -> Function means
:: FUNCT_3:def 9
dom it = [:dom f, dom g:] &
for x,y st x in dom f & y in dom g holds it.[x,y] = [f.x,g.y];
end;

canceled;

theorem :: FUNCT_3:86
for f,g being Function, x,y
st [x,y] in [:dom f,dom g:] holds [:f,g:].[x,y] = [f.x,g.y];

theorem :: FUNCT_3:87
for f,g being Function holds
[:f,g:] = <:f*pr1(dom f,dom g),g*pr2(dom f,dom g):>;

theorem :: FUNCT_3:88
for f,g being Function holds rng [:f,g:] = [:rng f,rng g:];

theorem :: FUNCT_3:89
for f,g being Function st dom f = X & dom g = X
holds <:f,g:> = [:f,g:]*(delta X);

theorem :: FUNCT_3:90
[:id X, id Y:] = id [:X,Y:];

theorem :: FUNCT_3:91
for f,g,h,k being Function holds [:f,h:]*<:g,k:> = <:f*g,h*k:>;

theorem :: FUNCT_3:92
for f,g,h,k being Function holds [:f,h:]*[:g,k:] = [:f*g,h*k:];

theorem :: FUNCT_3:93
for f,g being Function holds [:f,g:].:[:B,A:] = [:f.:B,g.:A:];

theorem :: FUNCT_3:94
for f,g being Function holds [:f,g:]"[:B,A:] = [:f"B,g"A:];

theorem :: FUNCT_3:95
for f being Function of X,Y for g being Function of V,Z
holds [:f,g:] is Function of [:X,V:],[:Y,Z:];

definition let X1,X2,Y1,Y2;
let f1 be Function of X1,Y1; let f2 be Function of X2,Y2;
redefine func [:f1,f2:] -> Function of [:X1,X2:],[:Y1,Y2:];
end;

theorem :: FUNCT_3:96
for f1 being Function of C1,D1 for f2 being Function of C2,D2
for c1 being Element of C1 for c2 being Element of C2
holds [:f1,f2:].[c1,c2] = [f1.c1,f2.c2];

theorem :: FUNCT_3:97
for f1 being Function of X1,Y1 for f2 being Function of X2,Y2
st (Y1 = {} implies X1 = {}) & (Y2 = {} implies X2 = {})
holds [:f1,f2:] = <:f1*pr1(X1,X2),f2*pr2(X1,X2):>;

theorem :: FUNCT_3:98
for f1 being Function of X1,D1 for f2 being Function of X2,D2
holds [:f1,f2:] = <:f1*pr1(X1,X2),f2*pr2(X1,X2):>;

theorem :: FUNCT_3:99
for f1 being Function of X,Y1 for f2 being Function of X,Y2
st (Y1 = {} implies X = {}) & (Y2 = {} implies X = {})
holds <:f1,f2:> = [:f1,f2:]*(delta X);

theorem :: FUNCT_3:100
for f1 being Function of X,D1 for f2 being Function of X,D2
holds <:f1,f2:> = [:f1,f2:]*(delta X);
```