B.11 FUNCT_2

Functions from a Set to a Set by Czeslaw Bylinski

reserve P,Q,X,Y,Y1,Y2,Z,p,x,x',x1,x2,y,y1,y2,z for set;

def 1 attr R is quasi_total means X = dom R if Y = {} implies X = {}

otherwise R = {};

cluster quasi_total Function-like Relation of X,Y;

cluster total -> quasi_total PartFunc of X,Y;

mode Function of X,Y is quasi_total Function-like Relation of X,Y;

3 for f being Function holds f is Function of dom f, rng f;

4 for f being Function st rng f c= Y holds f is Function of dom f, Y;

5 for f being Function st dom f = X & for x st x in X

holds f.x in Y holds f is Function of X,Y;

6 for f being Function of X,Y st Y <> {} & x in X holds f.x in rng f;

7 for f being Function of X,Y st Y <> {} & x in X holds f.x in Y;

8 for f being Function of X,Y st (Y = {} implies X = {}) & rng f c=
Z

holds f is Function of X,Z;

9 for f being Function of X,Y

st (Y = {} implies X = {}) & Y c= Z holds f is Function of X,Z;

scheme FuncEx1{X, Y() -> set, P[set,set]}:

ex f being Function of X(),Y() st for x st x in X() holds P[x,f.x]

provided

for x st x in X() ex y st y in Y() & P[x,y];

scheme Lambda1{X, Y() -> set, F(set)->set}:

ex f being Function of X(),Y() st for x st x in X() holds f.x = F(x)

provided

for x st x in X() holds F(x) in Y();

def 2 func Funcs(X,Y) -> set means

x in it iff ex f being Function st x = f & dom
f = X & rng f c= Y;

11 for f being Function of X,Y st Y = {} implies X = {}

holds f in Funcs(X,Y);

12 for f being Function of X,X holds f in Funcs(X,X);

14 X <> {} implies Funcs(X,{}) = {};

16 for f being Function of X,Y

st Y <> {} & for y st y in Y ex x st x in
X & y = f.x

holds rng f = Y;

17 for f being Function of X,Y st y in Y &

rng f = Y ex x st x in X & f.x = y;

18 for f1,f2 being Function of X,Y

st for x st x in X holds f1.x = f2.x

holds f1 = f2;

19 for f being Function of X,Y for g being Function of Y,Z

st Y = {} implies Z = {} or X = {}

holds g*f is Function of X,Z;

20 for f being Function of X,Y for g being Function of Y,Z

st Y <> {} & Z <> {} & rng f =
Y & rng g = Z holds rng(g*f) = Z;

21 for f being Function of X,Y, g being Function

st Y <> {} & x in X holds (g*f).x = g.(f.x);

22 for f being Function of X,Y st Y <> {} holds rng f = Y iff

for Z st Z <> {} for g,h being Function of Y,Z
st g*f = h*f

holds g = h;

23 for f being Function of X,Y

st Y = {} implies X = {} holds f*(id X) = f & (id
Y)*f = f;

24 for f being Function of X,Y for g being Function of Y,X

st f*g = id Y holds rng f = Y;

25 for f being Function of X,Y st Y = {} implies X = {}

holds f is one-to-one iff

for x1,x2 st x1 in X & x2 in X & f.x1 = f.x2
holds x1 = x2;

for f being Function of X,Y for g being Function of
Y,Z

st (Z = {} implies Y = {}) & (Y = {}

implies X = {}) & g*f is one-to-one

holds f is one-to-one;

27 for f being Function of X,Y st X <> {} & Y <> {}

holds f is one-to-one iff

for Z for g,h being Function of Z,X st f*g = f*h holds
g = h;

28 for f being Function of X,Y for g being Function of Y,Z

st Z <> {} & rng(g*f) = Z & g is one-to-one
holds rng f = Y;

29 for f being Function of X,Y for g being Function of Y,X

st Y <> {} & g*f = id X holds f is one-to-one
& rng g = X;

30 for f being Function of X,Y for g being Function of Y,Z

st (Z = {} implies Y = {}) & g*f is one-to-one
& rng f = Y

holds f is one-to-one & g is one-to-one;

31 for f being Function of X,Y st f is one-to-one & rng f = Y

holds f" is Function of Y,X;

32 for f being Function of X,Y

st Y <> {} & f is one-to-one & x in X
holds (f").(f.x) = x;

34 for f being Function of X,Y for g being Function of Y,X

st X <> {} & Y <> {} & rng f =
Y & f is one-to-one &

for y,x holds y in Y & g.y = x iff x in X &
f.x = y

holds g = f";

35 for f being Function of X,Y

st Y <> {} & rng f = Y & f is one-to-one

holds f"*f = id X & f*f" = id Y;

36 for f being Function of X,Y for g being Function of Y,X

st X <> {} & Y <> {} & rng f =
Y & g*f = id X & f is one-to-one

holds g = f";

37 for f being Function of X,Y st Y <> {}

& ex g being Function of Y,X st g*f = id X

holds f is one-to-one;

38 for f being Function of X,Y

st (Y = {} implies X = {}) & Z c= X holds f|Z
is Function of Z,Y;

40 for f being Function of X,Y st X c= Z holds f|Z = f;

41 for f being Function of X,Y st Y <> {} & x in X & f.x in

Z holds (Z|f).x = f.x;

42 for f being Function of X,Y st (Y = {} implies X = {}) & Y c= Z
holds Z|f = f;

43 for f being Function of X,Y st Y <> {}

for y holds y in f.:P iff ex x st x in X & x in
P & y = f.x;

44 for f being Function of X,Y holds f.:P c= Y;

redefine func f.:P -> Subset of Y;

45 for f being Function of X,Y st Y = {} implies X = {}

holds f.:X = rng f;

46 for f being Function of X,Y

st Y <> {} for x holds x in f"Q iff x in X & f.x in Q;

47 for f being PartFunc of X,Y holds f"Q c= X;

redefine func f"Q -> Subset of X;

48 for f being Function of X,Y st Y = {} implies X = {}

holds f"Y = X;

49 for f being Function of X,Y

holds (for y st y in Y holds f"{y} <> {})
iff rng f = Y;

50 for f being Function of X,Y

st (Y = {} implies X = {}) & P c= X holds P c=
f"(f.:P);

51 for f being Function of X,Y st Y = {} implies X = {}

holds f"(f.:X) = X;

53 for f being Function of X,Y for g being Function of Y,Z

st (Z = {} implies Y = {}) & (Y = {} implies X
= {})

holds f"Q c= (g*f)"(g.:Q);

54 for f being Function of {},Y holds dom f = {} & rng f = {};

55 for f being Function st dom f = {} holds f is Function of {},Y;

56 for f1 being Function of {},Y1 for f2 being Function of {},Y2

holds f1 = f2;

58 for f being Function of {},Y holds f is one-to-one;

59 for f being Function of {},Y holds f.:P = {};

60 for f being Function of {},Y holds f"Q = {};

61 for f being Function of {x},Y st Y <> {} holds f.x in Y;

62 for f being Function of {x},Y st Y <> {} holds rng f = {f.x};

63 for f being Function of {x},Y st Y <> {} holds f is one-to-one;

64 for f being Function of {x},Y st Y <> {} holds f.:P c= {f.x};

65 for f being Function of X,{y} st x in X holds f.x = y;

66 for f1,f2 being Function of X,{y} holds f1 = f2;

redefine func g*f -> Function of X,X;

redefine func id X -> Function of X,X;

67 for f being Function of X,X holds dom f = X & rng f c= X;

70 for f being Function of X,X, g being Function

st x in X holds (g*f).x = g.(f.x);

73 for f,g being Function of X,X st rng f = X & rng g = X

holds rng(g*f) = X;

74 for f being Function of X,X holds f*(id X) = f & (id X)*f = f;

75 for f,g being Function of X,X st g*f = f & rng f = X

holds g = id X;

76 for f,g being Function of X,X st f*g = f & f is one-to-one

holds g = id X;

77 for f being Function of X,X holds f is one-to-one iff

for x1,x2 st x1 in X & x2 in X & f.x1 = f.x2
holds x1 = x2;

79 for f being Function of X,X holds f.:X = rng f;

82 for f being Function of X,X holds f"(f.:X) = X;

def 3 attr f is onto means rng f = Y;

def 4 attr f is bijective means f is one-to-one onto;

cluster bijective -> one-to-one onto Function of X,Y;

cluster one-to-one onto -> bijective Function of X,Y;

cluster bijective Function of X,X;

mode Permutation of X is bijective Function of X,X;

83 for f being Function of X, X holds

f is Permutation of X iff f is one-to-one & rng
f = X;

85 for f being Function of X,X st f is one-to-one holds

for x1,x2 st x1 in X & x2 in X & f.x1 = f.x2
holds x1 = x2;

redefine func g*f -> Permutation of X;

redefine func id X -> Permutation of X;

redefine func f" -> Permutation of X;

86 for f,g being Permutation of X st g*f = g holds f = id X;

87 for f,g being Permutation of X st g*f = id X holds g = f";

88 for f being Permutation of X holds (f")*f =id X & f*(f") = id X;

92 for f being Permutation of X st P c= X

holds f.:(f"P) = P & f"(f.:P) = P;

93 for f being Function of X,X st f is one-to-one

holds f.:P = (f")"P & f"P = (f").:P;

reserve C,D,E for non empty set;

cluster quasi_total -> total PartFunc of X,D;

redefine func g*f -> Function of X,Z;

reserve c for Element of C;

reserve d for Element of D;

redefine func f.c -> Element of D;

scheme FuncExD{C, D() -> non empty set, P[set,set]}:

ex f being Function of C(),D() st for x being Element of C()

holds P[x,f.x]

provided

for x being Element of C() ex y being Element of D() st P[x,y];

scheme LambdaD{C, D() -> non empty set,

F(Element of C()) -> Element of D()}:

ex f being Function of C(),D() st

for x being Element of C() holds f.x = F(x);

113 for f1,f2 being Function of X,Y st

for x being Element of X holds f1.x = f2.x holds f1 = f2;

116 for f being Function of C,D for d

holds d in f.:P iff ex c st c in P & d =
f.c;

118 for f1,f2 being Function of [:X,Y:],Z

st for x,y st x in X & y in Y holds f1.[x,y]
= f2.[x,y]

holds f1 = f2;

119 for f being Function of [:X,Y:],Z st x in X & y in Y & Z <> {}

holds f.[x,y] in Z;

scheme FuncEx2{X, Y, Z() -> set, P[set,set,set]}:

ex f being Function of [:X(),Y():],Z() st

for x,y st x in X() & y in Y() holds P[x,y,f.[x,y]]

provided

for x,y st x in X() & y in Y() ex z st z in Z() & P[x,y,z];

scheme Lambda2{X, Y, Z() -> set, F(set,set)->set}:

ex f being Function of [:X(),Y():],Z()

st for x,y st x in X() & y in Y() holds f.[x,y] = F(x,y)

provided

for x,y st x in X() & y in Y() holds F(x,y) in Z();

120 for f1,f2 being Function of [:C,D:],E st for c,d

holds f1.[c,d] = f2.[c,d] holds f1 = f2;

scheme FuncEx2D{X, Y, Z() -> non empty set, P[set,set,set]}:

ex f being Function of [:X(),Y():],Z() st

for x being Element of X() for y being Element of Y() holds P[x,y,f.[x,y]]

provided

for x being Element of X() for y being Element of Y()

ex z being Element of Z() st P[x,y,z];

scheme Lambda2D{X, Y, Z() -> non empty set,

F(Element of X(),Element of Y()) -> Element of Z()}:

ex f being Function of [:X(),Y():],Z()

st for x being Element of X() for y being Element of Y()

holds f.[x,y]=F(x,y);

121 for f being set st f in Funcs(X,Y) holds f is Function of X,Y;

scheme Lambda1C{A, B() -> set, C[set], F(set)->set, G(set)->set}:

ex f being Function of A(),B() st

for x st x in A() holds

(C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x))

provided

for x st x in A() holds

(C[x] implies F(x) in B()) & (not C[x] implies G(x) in B());

123 for f being Function of {},Y holds f = {};

124 for f being Function of X,Y st f is one-to-one

holds f" is PartFunc of Y,X;

125 for f being Function of X,X st f is one-to-one

holds f" is PartFunc of X,X;

127 for f being Function of X,Y st Y = {}

implies X = {} holds <:f,X,Y:> = f;

128 for f being Function of X,X holds <:f,X,X:> = f;

130 for f being PartFunc of X,Y st dom f = X

holds f is Function of X,Y;

131 for f being PartFunc of X,Y st f is total

holds f is Function of X,Y;

132 for f being PartFunc of X,Y st (Y = {}

implies X = {}) & f is Function of X,Y holds
f is total;

133 for f being Function of X,Y

st (Y = {} implies X = {}) holds <:f,X,Y:> is total;

134 for f being Function of X,X holds <:f,X,X:> is total;

136 for f being PartFunc of X,Y st Y = {} implies X = {}

ex g being Function of X,Y st for x st x in dom f

holds g.x = f.x;

141 Funcs(X,Y) c= PFuncs(X,Y);

142 for f,g being Function of X,Y st (Y = {}

implies X = {}) & f tolerates g holds f =
g;

143 for f,g being Function of X,X st f tolerates g holds f = g;

145 for f being PartFunc of X,Y for g being Function of X,Y

st Y = {} implies X = {}

holds f tolerates g iff for x st x in dom f holds
f.x = g.x;

146 for f being PartFunc of X,X for g being Function of X,X

holds f tolerates g iff for x st x in dom f holds f.x = g.x;

148 for f being PartFunc of X,Y st Y = {} implies X = {}

ex g being Function of X,Y st f tolerates g;

149 for f being PartFunc of X,X ex g being Function of X,X st

f tolerates g;

151 for f,g being PartFunc of X,Y for h being Function of X,Y

st (Y = {} implies X = {}) & f tolerates h & g tolerates h

holds f tolerates g;

152 for f,g being PartFunc of X,X for h being Function of X,X

st f tolerates h & g tolerates h holds f
tolerates g;

154 for f,g being PartFunc of X,Y st (Y = {}

implies X = {}) & f tolerates g

ex h being Function of X,Y st f tolerates h &
g tolerates h;

155 for f being PartFunc of X,Y for g being Function of X,Y

st (Y = {} implies X = {}) & f tolerates
g

holds g in TotFuncs f;

156 for f being PartFunc of X,X for g being Function of X,X

st f tolerates g holds g in TotFuncs f;

158 for f being PartFunc of X,Y for g being set

st g in TotFuncs(f) holds g is Function of X,Y;

159 for f being PartFunc of X,Y holds TotFuncs f c= Funcs(X,Y);

160 TotFuncs <:{},X,Y:> = Funcs(X,Y);

161 for f being Function of X,Y st Y = {} implies X = {}

holds TotFuncs <:f,X,Y:> = {f};

162 for f being Function of X,X holds TotFuncs <:f,X,X:> = {f};

164 for f being PartFunc of X,{y} for g being Function of X,{y}

holds TotFuncs f = {g};

165 for f,g being PartFunc of X,Y

st g c= f holds TotFuncs f c= TotFuncs g;

166 for f,g being PartFunc of X,Y

st dom g c= dom f & TotFuncs f c= TotFuncs g holds g c= f;

167 for f,g being PartFunc of X,Y

st TotFuncs f c= TotFuncs g & (for y holds
Y <> {y})

holds g c= f;

168 for f,g being PartFunc of X,Y

st (for y holds Y <> {y}) & TotFuncs f =
TotFuncs g holds f = g;