B.6 FUNCT_1

FUNCT_1.ABS (Digest)
Functions and Their Basic Properties, by Czes{1}aw Byli'nski.

reserve X,X1,X2,Y,Y1,Y2 for set, p,x,x1,x2,y,y1,y2,z,z1,z2 for Any;

def 1 pred X is Function-like means

        for x,y1,y2 st [x,y] C X & [x,y2] C X

          holds y1 = y2;

cluster Relation-like Function-like set;

mode Function is Function-like Relation-like Any;

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 C F ex x,y st [x,y] = p) &

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

     holds F is Function;

3 p C f implies ex x,y st [x,y] = p;

4 [x,y1] C f & [x,y2] C f implies y1 = y2;


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

  ex f st for x,y holds [x,y] C f iff xCA( ) & P[x,y]

  provided

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


def 4 func f.x -> Any means [x,it] C f if x C dom f

       otherwise it = 0;


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

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


def 5 func rng f means

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


11 y C rng f iff ex x st x C dom f & y = f.x;

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

13 dom f =  iff rng f = ;

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


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

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

  provided

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

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


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

  ex f being Function st dom f = A( ) & for x st x C 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 C Y ex x st x C dom f & y = f.x) implies Y c= rng f;


cluster gf -> Function-like;


20 for h holds h = gf

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

21 x C dom(gf) iff x C dom f & f.x C dom g;

22 x C dom(gf) implies (gf).x = g.(f.x);

23 x C dom f implies (gf).x = g.(f.x);

24 dom(gf) c= dom f;

25 z C rng(gf) implies z C rng g;

27 rng f c= dom g iff dom(gf) = dom f;

29 rng f = dom g implies don(gf) = dom f & rng(gf) = rng g;

33 rng f c= Y & (for g,h st dom g = Y & dom h = Y & gf = hf holds g = h)
 implies Y = rng f ;

cluster id X -> Function-like;

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

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

37 dom(f(id X)) = dom f  X;

38 xC dom f  X implies f.x = (f(id X)).x;

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

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

43 (id X)(id Y) = (id(X  Y);

44 dom f = X & rng f = X & dom g = X & gf = f implies g = id X;


def 8 pred f is one-to-one means

      for x1,x2 st x1 C dom f & x2 C dom f & f.x1 = f.x2

        holds x1 = x2;



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

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

48 gf 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 & fh

      holds g = h);

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

   implies g = id X;

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

52 id X is one-to-one;

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



def 9 func f" -> Function means don it = rng f &

         for y,x holds y C rng f & x = it.y iff x C 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 C dom f implies x = (f").(f.x) & x = (f".f).x;

57 f is one-to-one & y C rng f implies y = f.((f").y) & y = (ff").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 don(ff") = rng f & rng(ff") = rng f;



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

    & ( for x,y st x C dom f & y C 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 & ff" = 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 & gf = id dom f implies g = f";

64 f is one-to-one & rng g = dom f & fg = 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 (gf)" = f"g";

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

cluster fX -> Function-like;

68 g = fX iff dom g = dom f  X & for x st x C dom g holds g.x = f.x;

69 dom(fX) = dom f  X;

70 x C dom(fX) implies (fX).x = f.x;

71 x C dom f  X implies (fX).x = f.x;

72 x C X implies (fX).x = f.x;

73 x C dom f & x C X implies f.x C rng(fX);

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

76 dom(fX) c= dom f & rng(fX) c= rng f;

79 f(dom f) = f;

82 X c= Y implies (fX)Y = fX & (fY)X = fX;

84 f is one-to-one implies fX is one-to-one;

cluster Yf -> Function-like;

85 g = Yf iff (for x holds x C dom g iff x C dom f & f.x C Y) & (for x st x C dom g 

holds g.x = f.x);

86 x C dom(Yf) iff x C dom f & f.x C Y;

87 x C dom(Yf) implies (Yf).x = f.x;

89 dom(Yf) c= dom f & rng(Yf) c= rng f;

94 (rng f)f = f;

97 X c= Y implies Y(Xf) = Xf & X(Yf) = Xf;

99 f is one-to-one implies Yf is one-to-one;

def 12 func fX means for y holds y C it

        iff ex x st x C dom f & x C X & y = f.x;

102 y C fX iff ex x st x C dom f & x C X & y = f.x;

117 x C dom f implies f{x}

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

120 (Yf)X c= fX;

121 f is one-to-one implies f(X1  X2) = fX1  fX2;

122 (for X1,X2 holds f(X1  X2) = fX1  fX2) implies f is one-to-one;

123 f is one-to-one implies f(X1  X2) = fX1  fX2;

124 (for X1,X2 holds f(X1 X2) = fX1  fX2) implies f is one-to-one;

125 X  Y =  & f is one-to-one implies fX  fY = ;

126 (Yf)X = Y  fX;

def 13 redefine func f"Y means for x holds x C it 

          iff x C dom f & f.x C Y;

128 x C f"Y iff x C dom f & f.x C Y;

134 Y c= rng f implies (f"Y =   iff Y = );

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

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

139 (fX)"Y = X  (f"Y);

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

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

144 (for y st y C 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"(fX);

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

148 f (f"Y) = Y  f(dom f);

149 f(X  f"Y) c= (fX)Y;

150 f(X  f"Y) =(fX) Y;

151 x  f"Y c= f"(fX  Y);

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

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

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

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

156 Y = rng f & dom g = Y & dom h = Y & gf = hf implies g = h;

157 fX1 c= fX2 & 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= (gf)"(gX);

目次に戻る


前のページに戻る


次のページに進む