Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### The Modification of a Function by a Function and the Iteration of the Composition of a Function

by
Czeslaw Bylinski

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

```environ

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

begin

reserve a,b,p,x,x',x1,x1',x2,y,y',y1,y1',y2,z,z',z1,z2,X,X',Y,Y',Z,Z'
for set;
reserve A,D,D' for non empty set;
reserve f,g,h for Function;

theorem :: FUNCT_4:1
(for z st z in Z holds ex x,y st z = [x,y]) implies ex X,Y st Z c= [:X,Y:];

theorem :: FUNCT_4:2
g*f = (g|rng f)*f;

theorem :: FUNCT_4:3
{} = {} --> a;

theorem :: FUNCT_4:4
id X c= id Y iff X c= Y;

theorem :: FUNCT_4:5
X c= Y implies X --> a c= Y --> a;

theorem :: FUNCT_4:6
X --> a c= Y --> b implies X c= Y;

theorem :: FUNCT_4:7
X <> {} & X --> a c= Y --> b implies a = b;

theorem :: FUNCT_4:8
x in dom f implies {x} --> f.x c= f;

:: Natural order on functions

definition let f,g;
redefine pred f c= g;
synonym f <= g;
end;

theorem :: FUNCT_4:9
Y|f|X <= f;

theorem :: FUNCT_4:10
f <= g implies Y|f|X <= Y|g|X;

definition let f,g;
func f +* g -> Function means
:: FUNCT_4:def 1
dom it = dom f \/ dom g &
for x st x in dom f \/ dom g
holds (x in dom g implies it.x = g.x) & (not x in dom g implies it.x = f.x);
idempotence;
end;

theorem :: FUNCT_4:11
dom f c= dom(f+*g) & dom g c= dom(f+*g);

theorem :: FUNCT_4:12
not x in dom g implies (f +* g).x = f.x;

theorem :: FUNCT_4:13
x in dom(f +* g) iff x in dom f or x in dom g;

theorem :: FUNCT_4:14
x in dom g implies (f+*g).x = g.x;

theorem :: FUNCT_4:15
f +* g +* h = f +* (g +* h);

theorem :: FUNCT_4:16
f tolerates g & x in dom f implies (f+*g).x = f.x;

theorem :: FUNCT_4:17
dom f misses dom g & x in dom f implies (f +* g).x = f.x;

theorem :: FUNCT_4:18
rng(f +* g) c= rng f \/ rng g;

theorem :: FUNCT_4:19
rng g c= rng(f +* g);

theorem :: FUNCT_4:20
dom f c= dom g implies f +* g = g;

theorem :: FUNCT_4:21
{} +* f = f;

theorem :: FUNCT_4:22
f +* {} = f;

theorem :: FUNCT_4:23
id(X) +* id(Y) = id(X \/ Y);

theorem :: FUNCT_4:24
(f +* g)|(dom g) = g;

theorem :: FUNCT_4:25
((f +* g)|(dom f \ dom g)) c= f;

theorem :: FUNCT_4:26
g c= (f +* g);

theorem :: FUNCT_4:27
f tolerates g +* h implies f|(dom f \ dom h) tolerates g;

theorem :: FUNCT_4:28
f tolerates g +* h implies f tolerates h;

theorem :: FUNCT_4:29
f tolerates g iff f c= f +* g;

theorem :: FUNCT_4:30
f +* g c= f \/ g;

theorem :: FUNCT_4:31
f tolerates g iff f \/ g = f +* g;

theorem :: FUNCT_4:32
dom f misses dom g implies f \/ g = f +* g;

theorem :: FUNCT_4:33
dom f misses dom g implies f c= f +* g;

theorem :: FUNCT_4:34
dom f misses dom g implies (f +* g)|(dom f) = f;

theorem :: FUNCT_4:35
f tolerates g iff f +* g = g +* f;

theorem :: FUNCT_4:36
dom f misses dom g implies f +* g = g +* f;

theorem :: FUNCT_4:37
for f,g being PartFunc of X,Y st g is total holds f +* g = g;

theorem :: FUNCT_4:38
for f,g being Function of X,Y st Y = {} implies X = {} holds f +* g = g;

theorem :: FUNCT_4:39
for f,g being Function of X,X holds f +* g = g;

theorem :: FUNCT_4:40
for f,g being Function of X,D holds f +* g = g;

theorem :: FUNCT_4:41
for f,g being PartFunc of X,Y holds f +* g is PartFunc of X,Y;

:: The converse function whenever domain

definition let f;
func ~f -> Function means
:: FUNCT_4:def 2
(for x holds x in dom it iff ex y,z st x = [z,y] & [y,z] in dom f) &
(for y,z st [y,z] in dom f holds it.[z,y] = f.[y,z]);
end;

theorem :: FUNCT_4:42
rng ~f c= rng f;

theorem :: FUNCT_4:43
[x,y] in dom f iff [y,x] in dom ~f;

theorem :: FUNCT_4:44
[y,x] in dom ~f implies (~f).[y,x] = f.[x,y];

theorem :: FUNCT_4:45
ex X,Y st dom ~f c= [:X,Y:];

theorem :: FUNCT_4:46
dom f c= [:X,Y:] implies dom ~f c= [:Y,X:];

theorem :: FUNCT_4:47
dom f = [:X,Y:] implies dom ~f = [:Y,X:];

theorem :: FUNCT_4:48
dom f c= [:X,Y:] implies rng ~f = rng f;

theorem :: FUNCT_4:49
for f being PartFunc of [:X,Y:],Z holds ~f is PartFunc of [:Y,X:],Z;

theorem :: FUNCT_4:50
for f being Function of [:X,Y:],Z st Z<>{} holds ~f is Function of [:Y,X:],Z
;

theorem :: FUNCT_4:51
for f being Function of [:X,Y:],D holds ~f is Function of [:Y,X:],D
;

theorem :: FUNCT_4:52
~~f c= f;

theorem :: FUNCT_4:53
dom f c= [:X,Y:] implies ~~f = f;

theorem :: FUNCT_4:54
for f being PartFunc of [:X,Y:],Z holds ~~f = f;

theorem :: FUNCT_4:55
for f being Function of [:X,Y:],Z st Z <> {} holds ~~f = f;

theorem :: FUNCT_4:56
for f being Function of [:X,Y:],D holds ~~f = f;

:: Product of 2'ary functions

definition let f,g;
func |:f,g:| -> Function means
:: FUNCT_4:def 3

(for z holds z in dom it iff
ex x,y,x',y' st z = [[x,x'],[y,y']] & [x,y] in dom f & [x',y'] in dom g) &
(for x,y,x',y' st [x,y] in dom f & [x',y'] in dom g
holds it.[[x,x'],[y,y']] = [f.[x,y],g.[x',y']]);
end;

theorem :: FUNCT_4:57
[[x,x'],[y,y']] in dom |:f,g:| iff [x,y] in dom f & [x',y'] in dom g;

theorem :: FUNCT_4:58
[[x,x'],[y,y']] in dom |:f,g:|
implies |:f,g:|.[[x,x'],[y,y']] = [f.[x,y],g.[x',y']];

theorem :: FUNCT_4:59
rng |:f,g:| c= [:rng f,rng g:];

theorem :: FUNCT_4:60
dom f c= [:X,Y:] & dom g c= [:X',Y':]
implies dom|:f,g:| c= [:[:X,X':],[:Y,Y':]:];

theorem :: FUNCT_4:61
dom f = [:X,Y:] & dom g = [:X',Y':]
implies dom|:f,g:| = [:[:X,X':],[:Y,Y':]:];

theorem :: FUNCT_4:62
for f being PartFunc of [:X,Y:],Z for g being PartFunc of [:X',Y':],Z'
holds |:f,g:| is PartFunc of [:[:X,X':],[:Y,Y':]:],[:Z,Z':];

theorem :: FUNCT_4:63
for f being Function of [:X,Y:],Z for g being Function of [:X',Y':],Z'
st Z <> {} & Z' <> {}
holds |:f,g:| is Function of [:[:X,X':],[:Y,Y':]:],[:Z,Z':];

theorem :: FUNCT_4:64
for f being Function of [:X,Y:],D for g being Function of [:X',Y':],D'
holds |:f,g:| is Function of [:[:X,X':],[:Y,Y':]:],[:D,D':];

definition let x,y,a,b be set;
func (x,y) --> (a,b) -> set equals
:: FUNCT_4:def 4
({x} --> a) +* ({y} --> b);
end;

definition let x,y,a,b be set;
cluster (x,y) --> (a,b) -> Function-like Relation-like;
end;

theorem :: FUNCT_4:65
dom((x1,x2) --> (y1,y2)) = {x1,x2} & rng((x1,x2) --> (y1,y2)) c= {y1,y2};

theorem :: FUNCT_4:66
x1 <> x2 implies
((x1,x2) --> (y1,y2)).x1 = y1 & ((x1,x2) --> (y1,y2)).x2 = y2;

theorem :: FUNCT_4:67
x1 <> x2 implies rng((x1,x2) --> (y1,y2)) = {y1,y2};

theorem :: FUNCT_4:68
(x1,x2) --> (y,y) = {x1,x2} --> y;

definition let A,x1,x2; let y1,y2 be Element of A;
redefine func (x1,x2) --> (y1,y2) -> Function of {x1,x2},A;
end;

theorem :: FUNCT_4:69
for a,b,c,d being set,
g being Function st dom g = {a,b} & g.a = c & g.b = d holds
g = (a,b) --> (c,d);

theorem :: FUNCT_4:70
for x,y being set holds {x} --> y = {[x,y]};

theorem :: FUNCT_4:71
for a,b,c,d being set st a <> c
holds (a,c) --> (b,d) = { [a,b], [c,d] };

theorem :: FUNCT_4:72
for a,b,x,y,x',y' being set
st a <> b & (a,b) --> (x,y) = (a,b) --> (x',y')
holds x = x' & y = y';

```