B.8 FUNCT_1

Functions and Their Basic Properties by Czeslaw Bylinski

reserve X,X1,X2,Y,Y1,Y2 for set,

p,x,x1,x2,y,y1,y2,z,z1,z2 for set;

def 1 attr X is Function-like means

for x,y1,y2 st [x,y1] in X & [x,y2] in X holds
y1 = y2;

cluster Relation-like Function-like set;

mode Function is Function-like Relation-like set;

cluster empty -> Function-like set;

reserve f,f1,f2,g,g1,g2,h for Function;

2 for F being set st

(for p st p in F ex x,y st [x,y] = p) &

(for x,y1,y2 st [x,y1] in F & [x,y2] in F holds y1 =
y2)

holds F is Function;

scheme GraphFunc{A()->set,P[set,set]}:

ex f st for x,y holds [x,y] in f iff x in A() & P[x,y]

provided

for x,y1,y2 st P[x,y1] & P[x,y2] holds y1 = y2;

def 4 func f.x -> set means

[x,it] in f if x in dom f otherwise it = {};

8 [x,y] in f iff x in dom f & y = f.x;

9 dom f = dom g & (for x st x in dom f holds f.x = g.x) implies f = g;

def 5 redefine func rng f means

for y holds y in it iff ex x st x in dom f & y
= f.x;

12 x in dom f implies f.x in rng f;

14 dom f = {x} implies rng f = {f.x};

scheme FuncEx{A()->set,P[set,set]}:

ex f st dom f = A() & for x st x in A() holds P[x,f.x]

provided

for x,y1,y2 st x in A() & P[x,y1] & P[x,y2] holds y1 = y2 and

for x st x in A() ex y st P[x,y];

scheme Lambda{A()->set,F(set)->set}:

ex f being Function st dom f = A() & for x st x in A()

holds f.x = F(x);

15 X <> {} implies for y ex f st dom f = X & rng f = {y};

16 (for f,g st dom f = X & dom g = X holds f = g) implies X = {};

17 dom f = dom g & rng f = {y} & rng g = {y} implies f = g;

18 Y <> {} or X = {} implies ex f st X = dom f & rng f c= Y;

19 (for y st y in Y ex x st x in dom f & y = f.x) implies Y c= rng f;

redefine func f*g;

synonym g*f;

cluster g*f -> Function-like;

20 for h st

(for x holds x in dom h iff x in dom f & f.x in dom g)
&

(for x st x in dom h holds h.x = g.(f.x))

holds h = g*f;

21 x in dom(g*f) iff x in dom f & f.x in dom g;

22 x in dom(g*f) implies (g*f).x = g.(f.x);

23 x in dom f implies (g*f).x = g.(f.x);

25 z in rng(g*f) implies z in rng g;

27 dom(g*f) = dom f implies rng f c= dom g;

33 rng f c= Y & (for g,h st dom g = Y & dom h = Y & g*f = h*f

holds g = h) implies Y = rng f;

redefine func diagonal X;

synonym id X;

cluster id X -> Function-like;

34 f = id X iff dom f = X & for x st x in X holds f.x = x;

35 x in X implies (id X).x = x;

37 dom(f*(id X)) = dom f /\ X;

38 x in dom f /\ X implies f.x = (f*(id X)).x;

40 x in dom((id Y)*f) iff x in dom f & f.x in Y;

42 f*(id dom f) = f & (id rng f)*f = f;

43 (id X)*(id Y) = id(X /\ Y);

44 rng f = dom g & g*f = f implies g = id dom g;

def 8 attr f is one-to-one means

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

46 f is one-to-one & g is one-to-one implies g*f is one-to-one;

47 g*f is one-to-one & rng f c= dom g implies f is one-to-one;

48 g*f is one-to-one & rng f = dom g implies f is one-to-one &

g is one-to-one;

49 f is one-to-one iff

(for g,h st rng g c= dom f & rng h c= dom f &
dom g = dom h &

f*g = f*h holds g = h);

50 dom f = X & dom g = X & rng g c= X & f is one-to-one & f*g = f

implies g = id X;

51 rng(g*f) = rng g & g is one-to-one implies dom g c= rng f;

52 id X is one-to-one;

53 (ex g st g*f = id dom f) implies f is one-to-one;

cluster empty Function;

cluster empty -> one-to-one Function;

cluster one-to-one Function;

cluster f~ -> Function-like;

def 9 func f" -> Function equals f~;

54 f is one-to-one implies for g being Function holds g=f" iff

dom g = rng f &for y,x holds y in rng f & x = g.y

iff x in dom f & y = f.x;

55 f is one-to-one implies rng f = dom(f") & dom f = rng(f");

56 f is one-to-one & x in dom f implies x = (f").(f.x) & x = (f"*f).x;

57 f is one-to-one & y in rng f implies y = f.((f").y) & y = (f*f").y;

58 f is one-to-one implies dom(f"*f) = dom f & rng(f"*f) = dom f;

59 f is one-to-one implies dom(f*f") = rng f & rng(f*f") = rng f;

60 f is one-to-one & dom f = rng g & rng f = dom g &

(for x,y st x in dom f & y in dom g holds f.x = y iff
g.y = x)

implies g = f";

61 f is one-to-one implies f"*f = id dom f & f*f" = id rng f;

62 f is one-to-one implies f" is one-to-one;

63 f is one-to-one & rng f = dom g & g*f = id dom f implies g = f";

64 f is one-to-one & rng g = dom f & f*g = id rng f implies g = f";

65 f is one-to-one implies (f")" = f;

66 f is one-to-one & g is one-to-one implies (g*f)" = f"*g";

67 (id X)" = (id X);

cluster f|X -> Function-like;

68 g = f|X iff dom g = dom f /\ X & for x st x in dom g

holds g.x = f.x;

70 x in dom(f|X) implies (f|X).x = f.x;

71 x in dom f /\ X implies (f|X).x = f.x;

72 x in X implies (f|X).x = f.x;

73 x in dom f & x in X implies f.x in rng(f|X);

74 X c= dom f implies dom(f|X) = X;

76 dom(f|X) c= dom f & rng(f|X) c= rng f;

82 X c= Y implies (f|X)|Y = f|X & (f|Y)|X = f|X;

84 f is one-to-one implies f|X is one-to-one;

cluster Y|f -> Function-like;

85 g = Y|f iff (for x holds x in dom g iff x in dom f & f.x in Y) &

(for x st x in dom g holds g.x = f.x);

86 x in dom(Y|f) iff x in dom f & f.x in Y;

87 x in dom(Y|f) implies (Y|f).x = f.x;

89 dom(Y|f) c= dom f & rng(Y|f) c= rng f;

97 X c= Y implies Y|(X|f) = X|f & X|(Y|f) = X|f;

99 f is one-to-one implies Y|f is one-to-one;

def 12 func f.:X means

for y holds y in it iff ex x st x in dom f & x
in X & y = f.x;

117 x in dom f implies f.:{x} = {f.x};

118 x1 in dom f & x2 in dom f implies f.:{x1,x2} = {f.x1,f.x2};

120 (Y|f).:X c= f.:X;

121 f is one-to-one implies f.:(X1 /\ X2) = f.:X1 /\ f.:X2;

122 (for X1,X2 holds f.:(X1 /\ X2) = f.:X1 /\ f.:X2)

implies f is one-to-one;

123 f is one-to-one implies f.:(X1 \ X2) = f.:X1 \ f.:X2;

124 (for X1,X2 holds f.:(X1 \ X2) = f.:X1 \ f.:X2)

implies f is one-to-one;

125 X misses Y & f is one-to-one implies f.:X misses f.:Y;

126 (Y|f).:X = Y /\ f.:X;

def 13 redefine func f"Y means

for x holds x in it iff x in dom f & f.x in Y;

137 f"(Y1 /\ Y2) = f"Y1 /\ f"Y2;

138 f"(Y1 \ Y2) = f"Y1 \ f"Y2;

139 (f|X)"Y = X /\ (f"Y);

142 y in rng f iff f"{y} <> {};

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

144 (for y st y in rng f ex x st f"{y} = {x}) iff f is one-to-one;

145 f.:(f"Y) c= Y;

146 X c= dom f implies X c= f"(f.:X);

147 Y c= rng f implies f.:(f"Y) = Y;

148 f.:(f"Y) = Y /\ f.:(dom f);

149 f.:(X /\ f"Y) c= (f.:X) /\ Y;

150 f.:(X /\ f"Y) = (f.:X) /\ Y;

151 X /\ f"Y c= f"(f.:X /\ Y);

152 f is one-to-one implies f"(f.:X) c= X;

153 (for X holds f"(f.:X) c= X) implies f is one-to-one;

154 f is one-to-one implies f.:X = (f")"X;

155 f is one-to-one implies f"Y = (f").:Y;

156 Y = rng f & dom g = Y & dom h = Y & g*f = h*f implies g = h;

157 f.:X1 c= f.:X2 & X1 c= dom f & f is one-to-one implies X1 c= X2;

158 f"Y1 c= f"Y2 & Y1 c= rng f implies Y1 c= Y2;

159 f is one-to-one iff for y ex x st f"{y} c= {x};

160 rng f c= dom g implies f"X c= (g*f)"(g.:X);