The abstract of the Mizar article:

Functions and Their Basic Properties

by

Czeslaw Bylinski

Received March 3, 1989

MML identifier: FUNCT_1

[ Mizar article, MML identifier index ]

environ

 vocabulary RELAT_1, BOOLE, FUNCT_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1;
 constructors TARSKI, RELAT_1, SUBSET_1, XBOOLE_0;
 clusters SUBSET_1, RELAT_1, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

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

definition let X be set;
 attr X is Function-like means
:: FUNCT_1:def 1
 for x,y1,y2 st [x,y1] in X & [x,y2] in X holds y1 = y2;
end;

definition
 cluster Relation-like Function-like set;
end;

definition
 mode Function is Function-like Relation-like set;
end;

definition
 cluster empty -> Function-like set;
end;

reserve f,g,g1,g2,h for Function,
        R,S for Relation;

canceled;

theorem :: FUNCT_1: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;

definition let f,x;
 canceled 2;

  func f.x -> set means
:: FUNCT_1:def 4
 [x,it] in f if x in dom f otherwise it = {};
end;

canceled 5;

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

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

definition let f;
 redefine func rng f means
:: FUNCT_1:def 5
 for y holds y in it iff ex x st x in dom f & y = f.x;
end;

canceled 2;

theorem :: FUNCT_1:12
     x in dom f implies f.x in rng f;

canceled;

theorem :: FUNCT_1: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);

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

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

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

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

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

definition let f,g;
 redefine func f*g;
 synonym g*f;
end;

definition let f,g;
 cluster g*f -> Function-like;
end;

theorem :: FUNCT_1: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;

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

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

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

canceled;

theorem :: FUNCT_1:25
     z in rng(g*f) implies z in rng g;

canceled;

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

canceled 5;

theorem :: FUNCT_1: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;

definition let X;
 cluster id X -> Function-like;
end;

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

theorem :: FUNCT_1:35
     x in X implies (id X).x = x;

canceled;

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

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

canceled;

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

canceled;

theorem :: FUNCT_1:42
      f*(id dom f) = f & (id rng f)*f = f;

theorem :: FUNCT_1:43
     (id X)*(id Y) = id(X /\ Y);

theorem :: FUNCT_1:44
   rng f = dom g & g*f = f implies g = id dom g;

definition let f;
 canceled 2;

 attr f is one-to-one means
:: FUNCT_1:def 8
 for x1,x2 st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds x1 = x2;
end;

canceled;

theorem :: FUNCT_1:46
   f is one-to-one & g is one-to-one implies g*f is one-to-one;

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

theorem :: FUNCT_1:48
     g*f is one-to-one & rng f = dom g implies f is one-to-one & g is
one-to-one;

theorem :: FUNCT_1: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);

theorem :: FUNCT_1:50
     dom f = X & dom g = X & rng g c= X & f is one-to-one & f*g = f
     implies g = id X;

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

theorem :: FUNCT_1:52
   id X is one-to-one;

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

definition
  cluster empty Function;
end;

definition
 cluster empty -> one-to-one Function;
end;

definition
 cluster one-to-one Function;
end;

definition let f be one-to-one Function;
 cluster f~ -> Function-like;
end;

definition let f;
 assume
  f is one-to-one;
 func f" -> Function equals
:: FUNCT_1:def 9
 f~;
end;

theorem :: FUNCT_1: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;

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

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

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

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

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

theorem :: FUNCT_1: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";

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

theorem :: FUNCT_1:62
   f is one-to-one implies f" is one-to-one;

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

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

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

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

theorem :: FUNCT_1:67
     (id X)" = (id X);

definition let f,X;
 cluster f|X -> Function-like;
end;

theorem :: FUNCT_1:68
   g = f|X iff dom g = dom f /\ X & for x st x in dom g holds g.x = f.x;

canceled;

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

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

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

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

canceled 2;

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

canceled 5;

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

canceled;

theorem :: FUNCT_1:84
     f is one-to-one implies f|X is one-to-one;

definition let Y,f;
 cluster Y|f -> Function-like;
end;

theorem :: FUNCT_1: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);

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

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

canceled;

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

canceled 7;

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

canceled;

theorem :: FUNCT_1:99
     f is one-to-one implies Y|f is one-to-one;

definition let f,X;
 redefine
 canceled 2;

  func f.:X means
:: FUNCT_1:def 12
 for y holds y in it iff ex x st x in dom f & x in X & y = f.x;
end;

canceled 17;

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

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

canceled;

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

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

theorem :: FUNCT_1:122
     (for X1,X2 holds f.:(X1 /\ X2) = f.:X1 /\ f.:X2) implies f is one-to-one;

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

theorem :: FUNCT_1:124
     (for X1,X2 holds f.:(X1 \ X2) = f.:X1 \ f.:X2) implies f is one-to-one;

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

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

definition let f,Y;
 redefine func f"Y means
:: FUNCT_1:def 13
 for x holds x in it iff x in dom f & f.x in Y;
end;

canceled 10;

theorem :: FUNCT_1:137
     f"(Y1 /\ Y2) = f"Y1 /\ f"Y2;

theorem :: FUNCT_1:138
     f"(Y1 \ Y2) = f"Y1 \ f"Y2;

theorem :: FUNCT_1:139
     (R|X)"Y = X /\ (R"Y);

canceled 2;

theorem :: FUNCT_1:142
   y in rng R iff R"{y} <> {};

theorem :: FUNCT_1:143
     (for y st y in Y holds R"{y} <> {}) implies Y c= rng R;

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

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

theorem :: FUNCT_1:146
    X c= dom R implies X c= R"(R.:X);

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

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

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

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

theorem :: FUNCT_1:151
     X /\ R"Y c= R"(R.:X /\ Y);

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

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

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

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


:: SUPLEMENT

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

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

theorem :: FUNCT_1:158
     f"Y1 c= f"Y2 & Y1 c= rng f implies Y1 c= Y2;

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

theorem :: FUNCT_1:160
    rng R c= dom S implies R"X c= (R*S)"(S.:X);