The abstract of the Mizar article:

Basic Functions and Operations on Functions

by

Czeslaw Bylinski

Received May 9, 1989

MML identifier: FUNCT_3

[ Mizar article, MML identifier index ]

environ

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


begin

  reserve p,q,x,x1,x2,y,y1,y2,z,z1,z2 for set;
  reserve A,B,V,X,X1,X2,Y,Y1,Y2,Z for set;
  reserve C,C1,C2,D,D1,D2 for non empty set;

:: Additional propositions about functions

theorem :: FUNCT_3:1
   A c= Y implies id A = (id Y)|A;

theorem :: FUNCT_3:2
   for f,g being Function st X c= dom(g*f) holds f.:X c= dom g;

theorem :: FUNCT_3:3
   for f,g being Function st X c= dom f & f.:X c= dom g holds X c= dom(g*f);

theorem :: FUNCT_3:4
   for f,g being Function
     st Y c= rng(g*f) & g is one-to-one holds g"Y c= rng f;

theorem :: FUNCT_3:5
   for f,g being Function st Y c= rng g & g"Y c= rng f holds Y c= rng(g*f);

scheme FuncEx_3{A()->set,B()-> set,P[set,set,set]}:
   ex f being Function st dom f = [:A(),B():] &
       for x,y st x in A() & y in B() holds P[x,y,f.[x,y]]
provided
 for x,y,z1,z2 st x in A() & y in
 B() & P[x,y,z1] & P[x,y,z2] holds z1 = z2 and
 for x,y st x in A() & y in B() ex z st P[x,y,z];

scheme Lambda_3{A()->set,B()->set,F(set,set)->set}:
 ex f being Function st dom f = [:A(),B():] &
   for x,y st x in A() & y in B() holds f.[x,y] = F(x,y);

theorem :: FUNCT_3:6
   for f,g being Function st dom f = [:X,Y:] & dom g = [:X,Y:] &
     for x,y st x in X & y in Y holds f.[x,y] = g.[x,y]
    holds f = g;

:: Function indicated by the image under a function

definition let f be Function;
  func .:f -> Function means
:: FUNCT_3:def 1
 dom it = bool dom f & for X st X c= dom f holds it.X = f.:X;
end;

canceled;

theorem :: FUNCT_3:8
   for f being Function st X in dom(.:f) holds (.:f).X = f.:X;

theorem :: FUNCT_3:9
     for f being Function holds (.:f).{} = {};

theorem :: FUNCT_3:10
   for f being Function holds rng(.:f) c= bool rng f;

canceled;

theorem :: FUNCT_3:12
     for f being Function holds (.:f).:A c= bool rng f;

theorem :: FUNCT_3:13
   for f being Function holds (.:f)"B c= bool dom f;

theorem :: FUNCT_3:14
     for f being Function of X,D holds (.:f)"B c= bool X;

theorem :: FUNCT_3:15
   for f being Function holds union((.:f).:A) c= f.:(union A);

theorem :: FUNCT_3:16
   for f being Function st A c= bool dom f holds f.:(union A) = union((.:f).:A)
;

theorem :: FUNCT_3:17
     for f being Function of X,D st A c= bool X
    holds f.:(union A) = union((.:f).:A);

theorem :: FUNCT_3:18
   for f being Function holds union((.:f)"B) c= f"(union B);

theorem :: FUNCT_3:19
     for f being Function st B c= bool rng f holds f"(union B) = union((.:f)"B)
;

theorem :: FUNCT_3:20
     for f,g being Function holds .:(g*f) = .:g*.:f;

theorem :: FUNCT_3:21
   for f being Function holds .:f is Function of bool dom f, bool rng f;

theorem :: FUNCT_3:22
   for f being Function of X,Y st Y = {} implies X = {}
    holds .:f is Function of bool X, bool Y;

definition let X,D; let f be Function of X,D;
  redefine func .:f -> Function of bool X, bool D;
end;

:: Function indicated by the inverse image under a function

definition let f be Function;
  func "f -> Function means
:: FUNCT_3:def 2
 dom it = bool rng f & for Y st Y c= rng f holds it.Y = f"Y;
end;

canceled;

theorem :: FUNCT_3:24
   for f being Function st Y in dom("f) holds ("f).Y = f"Y;

theorem :: FUNCT_3:25
   for f being Function holds rng("f) c= bool dom f;

canceled;

theorem :: FUNCT_3:27
     for f being Function holds ("f).:B c= bool dom f;

theorem :: FUNCT_3:28
     for f being Function holds ("f)"A c= bool rng f;

theorem :: FUNCT_3:29
   for f being Function holds union(("f).:B) c= f"(union B);

theorem :: FUNCT_3:30
     for f being Function st B c= bool rng f holds union(("f).:B) = f"(union B)
;

theorem :: FUNCT_3:31
   for f being Function holds union(("f)"A) c= f.:(union A);

theorem :: FUNCT_3:32
     for f being Function st A c= bool dom f & f is one-to-one
    holds union(("f)"A) = f.:(union A);

theorem :: FUNCT_3:33
   for f being Function holds ("f).:B c= (.:f)"B;

theorem :: FUNCT_3:34
     for f being Function st f is one-to-one holds ("f).:B = (.:f)"B;

theorem :: FUNCT_3:35
   for f being Function,A be set st A c= bool dom f holds ("f)"A c= (.:f).:A;

theorem :: FUNCT_3:36
   for f being Function,A be set st f is one-to-one holds (.:f).:A c= ("f)"A;

theorem :: FUNCT_3:37
     for f being Function,A be set st f is one-to-one & A c= bool dom f
     holds ("f)"A = (.:f).:A;

theorem :: FUNCT_3:38
     for f,g being Function st g is one-to-one holds "(g*f) = "f*"g;

theorem :: FUNCT_3:39
     for f being Function holds "f is Function of bool rng f, bool dom f;

:: Characteristic function

definition let A,X;
  func chi(A,X) -> Function means
:: FUNCT_3:def 3
 dom it = X &
   for x st x in X
     holds (x in A implies it.x = 1) & (not x in A implies it.x = 0);
end;

canceled 2;

theorem :: FUNCT_3:42
  chi(A,X).x = 1 implies x in A;

theorem :: FUNCT_3:43
     x in X \ A implies chi(A,X).x = 0;

canceled 3;

theorem :: FUNCT_3:47
     A c= X & B c= X & chi(A,X) = chi(B,X) implies A = B;

theorem :: FUNCT_3:48
   rng chi(A,X) c= {0,1};

theorem :: FUNCT_3:49
     for f being Function of X,{0,1} holds f = chi(f"{1},X);

definition let A,X;
 redefine func chi(A,X) -> Function of X,{0,1};
end;

definition
  let Y; let A be Subset of Y;
func incl(A) -> Function of A,Y equals
:: FUNCT_3:def 4
 id A;
end;

canceled 3;

theorem :: FUNCT_3:53
     for A being Subset of Y holds incl A = (id Y)|A;

theorem :: FUNCT_3:54
   for A being Subset of Y holds dom incl A = A & rng incl A = A;

theorem :: FUNCT_3:55
     for A being Subset of Y st x in A holds (incl A).x = x;

theorem :: FUNCT_3:56
     for A being Subset of Y st x in A holds incl(A).x in Y;

:: Projections

definition let X,Y;
  func pr1(X,Y) -> Function means
:: FUNCT_3:def 5
 dom it = [:X,Y:] & for x,y st x in X & y in Y holds it.[x,y] = x;
  func pr2(X,Y) -> Function means
:: FUNCT_3:def 6
 dom it = [:X,Y:] & for x,y st x in X & y in Y holds it.[x,y] = y;
end;

canceled 2;

theorem :: FUNCT_3:59
   rng pr1(X,Y) c= X;

theorem :: FUNCT_3:60
     Y <> {} implies rng pr1(X,Y) = X;

theorem :: FUNCT_3:61
   rng pr2(X,Y) c= Y;

theorem :: FUNCT_3:62
     X <> {} implies rng pr2(X,Y) = Y;

definition let X,Y; redefine
 func pr1(X,Y) -> Function of [:X,Y:],X;
 func pr2(X,Y) -> Function of [:X,Y:],Y;
end;

definition let X;
 func delta(X) -> Function means
:: FUNCT_3:def 7
 dom it = X & for x st x in X holds it.x = [x,x];
end;

canceled 3;

theorem :: FUNCT_3:66
   rng delta X c= [:X,X:];

definition let X;
redefine func delta(X) -> Function of X,[:X,X:];
end;

:: Complex functions

definition let f,g be Function;
  func <:f,g:> -> Function means
:: FUNCT_3:def 8
 dom it = dom f /\ dom g & for x st x in dom it holds it.x = [f.x,g.x];
end;

canceled;

theorem :: FUNCT_3:68
   for f,g being Function
     st x in dom f /\ dom g holds <:f,g:>.x = [f.x,g.x];

theorem :: FUNCT_3:69
   for f,g being Function
    st dom f = X & dom g = X & x in X holds <:f,g:>.x = [f.x,g.x];

theorem :: FUNCT_3:70
   for f,g being Function st dom f = X & dom g = X holds dom <:f,g:> = X;

theorem :: FUNCT_3:71
   for f,g being Function holds rng <:f,g:> c= [:rng f,rng g:];

theorem :: FUNCT_3:72
   for f,g being Function st dom f = dom g & rng f c= Y & rng g c= Z
    holds pr1(Y,Z)*<:f,g:> = f & pr2(Y,Z)*<:f,g:> = g;

theorem :: FUNCT_3:73
   <:pr1(X,Y),pr2(X,Y):> = id [:X,Y:];

theorem :: FUNCT_3:74
   for f,g,h,k being Function
     st dom f = dom g & dom k = dom h & <:f,g:> = <:k,h:> holds f = k & g = h;

theorem :: FUNCT_3:75
     for f,g,h being Function holds <:f*h,g*h:> = <:f,g:>*h;

theorem :: FUNCT_3:76
     for f,g being Function holds <:f,g:>.:A c= [:f.:A,g.:A:];

theorem :: FUNCT_3:77
     for f,g being Function holds <:f,g:>"[:B,C:] = f"B /\ g"C;

theorem :: FUNCT_3:78
   for f being Function of X,Y for g being Function of X,Z
     st (Y = {} implies X = {}) & (Z = {} implies X = {})
    holds <:f,g:> is Function of X,[:Y,Z:];

definition let X,D1,D2;
  let f1 be Function of X,D1; let f2 be Function of X,D2;
redefine func <:f1,f2:> -> Function of X,[:D1,D2:];
end;

theorem :: FUNCT_3:79
     for f1 being Function of C,D1 for f2 being Function of C,D2
    for c being Element of C holds <:f1,f2:>.c = [f1.c,f2.c];

theorem :: FUNCT_3:80
     for f being Function of X,Y for g being Function of X,Z
    holds rng <:f,g:> c= [:Y,Z:];

theorem :: FUNCT_3:81
   for f being Function of X,Y for g being Function of X,Z
     st (Y = {} implies X = {}) & (Z = {} implies X = {})
    holds pr1(Y,Z)*<:f,g:> = f & pr2(Y,Z)*<:f,g:> = g;

theorem :: FUNCT_3:82
     for f being Function of X,D1 for g being Function of X,D2
    holds pr1(D1,D2)*<:f,g:> = f & pr2(D1,D2)*<:f,g:> = g;

theorem :: FUNCT_3:83
     for f1,f2 being Function of X,Y for g1,g2 being Function of X,Z
     st (Y = {} implies X = {}) & (Z = {} implies X = {}) &
      <:f1,g1:> = <:f2,g2:> holds f1 = f2 & g1 = g2;

theorem :: FUNCT_3:84
     for f1,f2 being Function of X,D1 for g1,g2 being Function of X,D2
     st <:f1,g1:> = <:f2,g2:> holds f1 = f2 & g1 = g2;

:: Product-functions

 definition let f,g be Function;
  func [:f,g:] -> Function means
:: FUNCT_3:def 9
 dom it = [:dom f, dom g:] &
    for x,y st x in dom f & y in dom g holds it.[x,y] = [f.x,g.y];
 end;

canceled;

theorem :: FUNCT_3:86
   for f,g being Function, x,y
    st [x,y] in [:dom f,dom g:] holds [:f,g:].[x,y] = [f.x,g.y];

theorem :: FUNCT_3:87
   for f,g being Function holds
    [:f,g:] = <:f*pr1(dom f,dom g),g*pr2(dom f,dom g):>;

theorem :: FUNCT_3:88
   for f,g being Function holds rng [:f,g:] = [:rng f,rng g:];

theorem :: FUNCT_3:89
   for f,g being Function st dom f = X & dom g = X
     holds <:f,g:> = [:f,g:]*(delta X);

theorem :: FUNCT_3:90
     [:id X, id Y:] = id [:X,Y:];

theorem :: FUNCT_3:91
     for f,g,h,k being Function holds [:f,h:]*<:g,k:> = <:f*g,h*k:>;

theorem :: FUNCT_3:92
     for f,g,h,k being Function holds [:f,h:]*[:g,k:] = [:f*g,h*k:];

theorem :: FUNCT_3:93
     for f,g being Function holds [:f,g:].:[:B,A:] = [:f.:B,g.:A:];

theorem :: FUNCT_3:94
     for f,g being Function holds [:f,g:]"[:B,A:] = [:f"B,g"A:];

theorem :: FUNCT_3:95
   for f being Function of X,Y for g being Function of V,Z
    holds [:f,g:] is Function of [:X,V:],[:Y,Z:];

definition let X1,X2,Y1,Y2;
  let f1 be Function of X1,Y1; let f2 be Function of X2,Y2;
redefine func [:f1,f2:] -> Function of [:X1,X2:],[:Y1,Y2:];
end;

theorem :: FUNCT_3:96
     for f1 being Function of C1,D1 for f2 being Function of C2,D2
    for c1 being Element of C1 for c2 being Element of C2
     holds [:f1,f2:].[c1,c2] = [f1.c1,f2.c2];

theorem :: FUNCT_3:97
     for f1 being Function of X1,Y1 for f2 being Function of X2,Y2
     st (Y1 = {} implies X1 = {}) & (Y2 = {} implies X2 = {})
    holds [:f1,f2:] = <:f1*pr1(X1,X2),f2*pr2(X1,X2):>;

theorem :: FUNCT_3:98
     for f1 being Function of X1,D1 for f2 being Function of X2,D2
    holds [:f1,f2:] = <:f1*pr1(X1,X2),f2*pr2(X1,X2):>;

theorem :: FUNCT_3:99
     for f1 being Function of X,Y1 for f2 being Function of X,Y2
     st (Y1 = {} implies X = {}) & (Y2 = {} implies X = {})
    holds <:f1,f2:> = [:f1,f2:]*(delta X);

theorem :: FUNCT_3:100
     for f1 being Function of X,D1 for f2 being Function of X,D2
    holds <:f1,f2:> = [:f1,f2:]*(delta X);