:: Basic Functions and Operations on Functions
::  by Czes{\l}aw Byli\'nski
::
:: Received May 9, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, TARSKI, RELAT_1, FUNCT_1, ZFMISC_1, SUBSET_1, MCART_1,
      PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1, CARD_1, ORDINAL1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, ORDINAL1, SUBSET_1, MCART_1,
      RELSET_1, FUNCT_1, FUNCT_2, BINOP_1;
 constructors BINOP_1, RELSET_1, ORDINAL1;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1;
 requirements SUBSET, BOOLE, NUMERALS;


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 :: FUNCT_3:sch 1
  FuncEx3{A()->set,B()-> set,P[object,object,object]}:
 ex f being Function st dom f = [:A(),B():] &
 for x,y being object st x in A() & y in B() holds P[x,y,f.(x,y)]
provided
 for x,y,z1,z2 being object
   st x in A() & y in B() & P[x,y,z1] & P[x,y,z2] holds z1 = z2 and
 for x,y being object st x in A() & y in B()
   ex z being object st P[x,y,z];

scheme :: FUNCT_3:sch 2
  Lambda3{A()->set,B()->set,F(object,object)->object}:
 ex f being Function st dom f = [:A(),B():] &
  for x,y being object 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 being object 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;

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem :: FUNCT_3:20
  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;

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

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

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

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

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

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

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

theorem :: FUNCT_3:28
  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:29
  for f being Function holds ("f).:B c= (.:f)"B;

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

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

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

theorem :: FUNCT_3:33
  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:34
  for f,g being Function st g is one-to-one holds "(g*f) = "f*"g;

theorem :: FUNCT_3:35
  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 being object st x in X holds
  (x in A implies it.x = 1) & (not x in A implies it.x = 0);
end;

theorem :: FUNCT_3:36
 for x being object holds chi(A,X).x = 1 implies x in A;

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

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

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

theorem :: FUNCT_3:40
  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;

notation
  let Y;
  let A be Subset of Y;
  synonym incl A for id A;
end;

definition
  let Y;
  let A be Subset of Y;
  redefine func incl A -> Function of A,Y;
end;

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

theorem :: FUNCT_3:42
  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 4
 dom it = [:X,Y:] &
   for x,y being object st x in X & y in Y holds it.(x,y) = x;
  func pr2(X,Y) -> Function means
:: FUNCT_3:def 5
 dom it = [:X,Y:] &
   for x,y being object st x in X & y in Y holds it.(x,y) = y;
end;

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

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

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

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

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

definition
  let X;
  func delta(X) -> Function means
:: FUNCT_3:def 6

  dom it = X & for x being object st x in X holds it .x = [x,x];
end;

theorem :: FUNCT_3:47
  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 7

  dom it = dom f /\ dom g &
  for x being object st x in dom it holds it.x = [f.x,g.x];
end;

registration
  let f be empty Function, g be Function;
  cluster <:f,g:> -> empty;
  cluster <:g,f:> -> empty;
end;

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

theorem :: FUNCT_3:49
  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:50
  for f,g being Function st dom f = X & dom g = X holds dom <:f,g :> = X;

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

theorem :: FUNCT_3:52
  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:53
  <:pr1(X,Y),pr2(X,Y):> = id [:X,Y:];

theorem :: FUNCT_3:54
  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:55
  for f,g,h being Function holds <:f*h,g*h:> = <:f,g:>*h;

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

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

theorem :: FUNCT_3:58
  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:59
  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:60
  for f being Function of X,Y for g being Function of X,Z holds rng <:f,
  g:> c= [:Y,Z:];

theorem :: FUNCT_3:61
  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:62
  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:63
  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:64
  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 8

  dom it = [:dom f, dom g:] & for x,y being object st
  x in dom f & y in dom g holds it.(x,y) = [f.x,g.y];
end;

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

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

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

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

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

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

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

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

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

theorem :: FUNCT_3:74
  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:75
  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:76
  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:77
  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:78
  for f1 being Function of X,Y1 for f2 being Function of X,Y2 holds <:f1
  ,f2:> = [:f1,f2:]*(delta X);

begin :: Addenda
:: from AMI_1

theorem :: FUNCT_3:79
  for f being Function holds pr1(dom f,rng f).:f = dom f;

theorem :: FUNCT_3:80
  for A,B,C being non empty set, f,g being Function of A,[:B,C:] st
  pr1(B,C)*f = pr1(B,C)*g & pr2(B,C)*f = pr2(B,C)*g holds f = g;

registration
  let F,G be one-to-one Function;
  cluster [:F,G:] -> one-to-one;
end;

registration let A be set;
 cluster idempotent for BinOp of A;
end;

registration let A be set, b be idempotent BinOp of A;
 let a be Element of A;
 reduce b.(a,a) to a;
end;

reserve A1,A2,B1,B2 for non empty set,
  f for Function of A1,B1,
  g for Function of A2,B2,
  Y1 for non empty Subset of A1,
  Y2 for non empty Subset of A2;

definition
  let A1 be set, B1 be non empty set, f be Function of A1, B1, Y1 be Subset of
  A1;
  redefine func f|Y1 -> Function of Y1,B1;
end;

theorem :: FUNCT_3:81
  [:f,g:]|([:Y1,Y2:] qua Subset of [:A1,A2:])
qua Function of [:Y1,Y2:],[:B1,B2:]
= [:f|Y1,g|Y2:] qua Function of [:Y1,Y2:],[:B1,B2:];