Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Functions from a Set to a Set

**by****Czeslaw Bylinski**- Received April 6, 1989
- MML identifier: FUNCT_2

- [ Mizar article, MML identifier index ]

environ vocabulary RELAT_1, BOOLE, FUNCT_1, PARTFUN1, FUNCT_2, SGRAPH1, RELAT_2; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, RELSET_1, FUNCT_1, PARTFUN1; constructors TARSKI, PARTFUN1, RELAT_2, XBOOLE_0; clusters FUNCT_1, RELAT_1, RELSET_1, SUBSET_1, XBOOLE_0, ZFMISC_1, PARTFUN1; requirements SUBSET, BOOLE; begin reserve P,Q,X,Y,Z,p,x,x',x1,x2,y,y1,y2,z for set; :::::::::::::::::::::::::::::::::::: :: function from a set into a set :: :::::::::::::::::::::::::::::::::::: definition let X,Y; let R be Relation of X,Y; attr R is quasi_total means :: FUNCT_2:def 1 X = dom R if Y = {} implies X = {} otherwise R = {}; end; definition let X,Y; cluster quasi_total Function-like Relation of X,Y; end; definition let X,Y; cluster total -> quasi_total PartFunc of X,Y; end; definition let X,Y; mode Function of X,Y is quasi_total Function-like Relation of X,Y; end; canceled 2; theorem :: FUNCT_2:3 for f being Function holds f is Function of dom f, rng f; theorem :: FUNCT_2:4 for f being Function st rng f c= Y holds f is Function of dom f, Y; theorem :: FUNCT_2:5 for f being Function st dom f = X & for x st x in X holds f.x in Y holds f is Function of X,Y; theorem :: FUNCT_2:6 for f being Function of X,Y st Y <> {} & x in X holds f.x in rng f; theorem :: FUNCT_2:7 for f being Function of X,Y st Y <> {} & x in X holds f.x in Y; theorem :: FUNCT_2:8 for f being Function of X,Y st (Y = {} implies X = {}) & rng f c= Z holds f is Function of X,Z; theorem :: FUNCT_2:9 for f being Function of X,Y st (Y = {} implies X = {}) & Y c= Z holds f is Function of X,Z; scheme FuncEx1{X, Y() -> set, P[set,set]}: ex f being Function of X(),Y() st for x st x in X() holds P[x,f.x] provided for x st x in X() ex y st y in Y() & P[x,y]; scheme Lambda1{X, Y() -> set, F(set)->set}: ex f being Function of X(),Y() st for x st x in X() holds f.x = F(x) provided for x st x in X() holds F(x) in Y(); :::::::::::::::::::::::::::::::::::::::::::: :: set of functions from a set into a set :: :::::::::::::::::::::::::::::::::::::::::::: definition let X,Y; func Funcs(X,Y) -> set means :: FUNCT_2:def 2 x in it iff ex f being Function st x = f & dom f = X & rng f c= Y; end; canceled; theorem :: FUNCT_2:11 for f being Function of X,Y st Y = {} implies X = {} holds f in Funcs(X,Y); theorem :: FUNCT_2:12 for f being Function of X,X holds f in Funcs(X,X); definition let X be set, Y be non empty set; cluster Funcs(X,Y) -> non empty; end; definition let X be set; cluster Funcs(X,X) -> non empty; end; canceled; theorem :: FUNCT_2:14 X <> {} implies Funcs(X,{}) = {}; canceled; theorem :: FUNCT_2:16 for f being Function of X,Y st Y <> {} & for y st y in Y ex x st x in X & y = f.x holds rng f = Y; theorem :: FUNCT_2:17 for f being Function of X,Y st y in Y & rng f = Y ex x st x in X & f.x = y ; theorem :: FUNCT_2:18 for f1,f2 being Function of X,Y st for x st x in X holds f1.x = f2.x holds f1 = f2; theorem :: FUNCT_2:19 for f being Function of X,Y for g being Function of Y,Z st Y = {} implies Z = {} or X = {} holds g*f is Function of X,Z; theorem :: FUNCT_2:20 for f being Function of X,Y for g being Function of Y,Z st Y <> {} & Z <> {} & rng f = Y & rng g = Z holds rng(g*f) = Z; theorem :: FUNCT_2:21 for f being Function of X,Y, g being Function st Y <> {} & x in X holds (g*f).x = g.(f.x); theorem :: FUNCT_2:22 for f being Function of X,Y st Y <> {} holds rng f = Y iff for Z st Z <> {} for g,h being Function of Y,Z st g*f = h*f holds g = h; theorem :: FUNCT_2:23 for f being Function of X,Y st Y = {} implies X = {} holds f*(id X) = f & (id Y)*f = f; theorem :: FUNCT_2:24 for f being Function of X,Y for g being Function of Y,X st f*g = id Y holds rng f = Y; theorem :: FUNCT_2:25 for f being Function of X,Y st Y = {} implies X = {} holds f is one-to-one iff for x1,x2 st x1 in X & x2 in X & f.x1 = f.x2 holds x1 = x2; theorem :: FUNCT_2:26 for f being Function of X,Y for g being Function of Y,Z st (Z = {} implies Y = {}) & (Y = {} implies X = {}) & g*f is one-to-one holds f is one-to-one; theorem :: FUNCT_2:27 for f being Function of X,Y st X <> {} & Y <> {} holds f is one-to-one iff for Z for g,h being Function of Z,X st f*g = f*h holds g = h; theorem :: FUNCT_2:28 for f being Function of X,Y for g being Function of Y,Z st Z <> {} & rng(g*f) = Z & g is one-to-one holds rng f = Y; theorem :: FUNCT_2:29 for f being Function of X,Y for g being Function of Y,X st Y <> {} & g*f = id X holds f is one-to-one & rng g = X; theorem :: FUNCT_2:30 for f being Function of X,Y for g being Function of Y,Z st (Z = {} implies Y = {}) & g*f is one-to-one & rng f = Y holds f is one-to-one & g is one-to-one; theorem :: FUNCT_2:31 for f being Function of X,Y st f is one-to-one & rng f = Y holds f" is Function of Y,X; theorem :: FUNCT_2:32 for f being Function of X,Y st Y <> {} & f is one-to-one & x in X holds (f").(f.x) = x; canceled; theorem :: FUNCT_2:34 for f being Function of X,Y for g being Function of Y,X st X <> {} & Y <> {} & rng f = Y & f is one-to-one & for y,x holds y in Y & g.y = x iff x in X & f.x = y holds g = f"; theorem :: FUNCT_2:35 for f being Function of X,Y st Y <> {} & rng f = Y & f is one-to-one holds f"*f = id X & f*f" = id Y; theorem :: FUNCT_2:36 for f being Function of X,Y for g being Function of Y,X st X <> {} & Y <> {} & rng f = Y & g*f = id X & f is one-to-one holds g = f"; theorem :: FUNCT_2:37 for f being Function of X,Y st Y <> {} & ex g being Function of Y,X st g*f = id X holds f is one-to-one; theorem :: FUNCT_2:38 for f being Function of X,Y st (Y = {} implies X = {}) & Z c= X holds f|Z is Function of Z,Y; canceled; theorem :: FUNCT_2:40 for f being Function of X,Y st X c= Z holds f|Z = f; theorem :: FUNCT_2:41 for f being Function of X,Y st Y <> {} & x in X & f.x in Z holds (Z|f).x = f.x; canceled; theorem :: FUNCT_2:43 for f being Function of X,Y st Y <> {} for y holds (ex x st x in X & x in P & y = f.x) implies y in f.:P; theorem :: FUNCT_2:44 for f being Function of X,Y holds f.:P c= Y; definition let X,Y; let f be Function of X,Y; let P; redefine func f.:P -> Subset of Y; end; theorem :: FUNCT_2:45 for f being Function of X,Y st Y = {} implies X = {} holds f.:X = rng f; theorem :: FUNCT_2:46 for f being Function of X,Y st Y <> {} for x holds x in f"Q iff x in X & f.x in Q; theorem :: FUNCT_2:47 for f being PartFunc of X,Y holds f"Q c= X; definition let X,Y; let f be PartFunc of X,Y; let Q; redefine func f"Q -> Subset of X; end; theorem :: FUNCT_2:48 for f being Function of X,Y st Y = {} implies X = {} holds f"Y = X; theorem :: FUNCT_2:49 for f being Function of X,Y holds (for y st y in Y holds f"{y} <> {}) iff rng f = Y; theorem :: FUNCT_2:50 for f being Function of X,Y st (Y = {} implies X = {}) & P c= X holds P c= f"(f.:P); theorem :: FUNCT_2:51 for f being Function of X,Y st Y = {} implies X = {} holds f"(f.:X) = X; canceled; theorem :: FUNCT_2:53 for f being Function of X,Y for g being Function of Y,Z st (Z = {} implies Y = {}) & (Y = {} implies X = {}) holds f"Q c= (g*f)"(g.:Q); :::::::::::::::::::: :: Empty Function :: :::::::::::::::::::: canceled; theorem :: FUNCT_2:55 for f being Function st dom f = {} holds f is Function of {},Y; canceled 3; theorem :: FUNCT_2:59 for f being Function of {},Y holds f.:P = {}; theorem :: FUNCT_2:60 for f being Function of {},Y holds f"Q = {}; ::::::::::::::::::::::::::::::::::::::: :: Function from a singelton into set:: ::::::::::::::::::::::::::::::::::::::: theorem :: FUNCT_2:61 for f being Function of {x},Y st Y <> {} holds f.x in Y; theorem :: FUNCT_2:62 for f being Function of {x},Y st Y <> {} holds rng f = {f.x}; canceled; theorem :: FUNCT_2:64 for f being Function of {x},Y st Y <> {} holds f.:P c= {f.x}; :::::::::::::::::::::::::::::::::::::::::: :: Function from a set into a singelton :: :::::::::::::::::::::::::::::::::::::::::: theorem :: FUNCT_2:65 for f being Function of X,{y} st x in X holds f.x = y; theorem :: FUNCT_2:66 for f1,f2 being Function of X,{y} holds f1 = f2; :::::::::::::::::::::::::::: :: Function from X into X :: :::::::::::::::::::::::::::: definition let X; let f,g be Function of X,X; redefine func g*f -> Function of X,X; end; theorem :: FUNCT_2:67 for f being Function of X,X holds dom f = X & rng f c= X; canceled 2; theorem :: FUNCT_2:70 for f being Function of X,X, g being Function st x in X holds (g*f).x = g.(f.x); canceled 2; theorem :: FUNCT_2:73 for f,g being Function of X,X st rng f = X & rng g = X holds rng(g*f) = X; theorem :: FUNCT_2:74 for f being Function of X,X holds f*(id X) = f & (id X)*f = f; theorem :: FUNCT_2:75 for f,g being Function of X,X st g*f = f & rng f = X holds g = id X; theorem :: FUNCT_2:76 for f,g being Function of X,X st f*g = f & f is one-to-one holds g = id X; theorem :: FUNCT_2:77 for f being Function of X,X holds f is one-to-one iff for x1,x2 st x1 in X & x2 in X & f.x1 = f.x2 holds x1 = x2; canceled; theorem :: FUNCT_2:79 for f being Function of X,X holds f.:X = rng f ; canceled 2; theorem :: FUNCT_2:82 for f being Function of X,X holds f"(f.:X) = X ; :::::::::::::::::::::::::: :: Permutation of a set :: :::::::::::::::::::::::::: definition let X, Y be set; let f be Function of X, Y; attr f is onto means :: FUNCT_2:def 3 rng f = Y; end; definition let X, Y; let f be Function of X,Y; attr f is bijective means :: FUNCT_2:def 4 f is one-to-one onto; end; definition let X, Y be set; cluster bijective -> one-to-one onto Function of X,Y; cluster one-to-one onto -> bijective Function of X,Y; end; definition let X; cluster bijective Function of X,X; end; definition let X; mode Permutation of X is bijective Function of X,X; end; theorem :: FUNCT_2:83 for f being Function of X, X st f is one-to-one & rng f = X holds f is Permutation of X; canceled; theorem :: FUNCT_2:85 for f being Function of X,X st f is one-to-one holds for x1,x2 st x1 in X & x2 in X & f.x1 = f.x2 holds x1 = x2; definition let X; let f,g be Permutation of X; redefine func g*f -> Permutation of X; end; definition let X; cluster reflexive total -> bijective Function of X,X; end; definition let X; let f be Permutation of X; redefine func f" -> Permutation of X; end; theorem :: FUNCT_2:86 for f,g being Permutation of X st g*f = g holds f = id X; theorem :: FUNCT_2:87 for f,g being Permutation of X st g*f = id X holds g = f"; theorem :: FUNCT_2:88 for f being Permutation of X holds (f")*f =id X & f*(f") = id X; canceled 3; theorem :: FUNCT_2:92 for f being Permutation of X st P c= X holds f.:(f"P) = P & f"(f.:P) = P; :::::::::::::::::::::::::::::::::::::::::::: :: Function from a set into a nonempty set :::::::::::::::::::::::::::::::::::::::::::: reserve C,D,E for non empty set; definition let X,D; cluster quasi_total -> total PartFunc of X,D; end; definition let X,D,Z; let f be Function of X,D; let g be Function of D,Z; redefine func g*f -> Function of X,Z; end; reserve c for Element of C; reserve d for Element of D; definition let C be non empty set, D be set; let f be Function of C,D; let c be Element of C; redefine func f.c -> Element of D; end; scheme FuncExD{C, D() -> non empty set, P[set,set]}: ex f being Function of C(),D() st for x being Element of C() holds P[x,f.x] provided for x being Element of C() ex y being Element of D() st P[x,y]; scheme LambdaD{C, D() -> non empty set, F(Element of C()) -> Element of D()}: ex f being Function of C(),D() st for x being Element of C() holds f.x = F(x); canceled 20; theorem :: FUNCT_2:113 for f1,f2 being Function of X,Y st for x being Element of X holds f1.x = f2.x holds f1 = f2; canceled; theorem :: FUNCT_2:115 for P being set for f being Function of X,Y for y holds y in f.:P implies ex x st x in X & x in P & y = f.x; theorem :: FUNCT_2:116 for f being Function of X,Y for y st y in f.:P ex c being Element of X st c in P & y = f.c; canceled; theorem :: FUNCT_2:118 for f1,f2 being Function of [:X,Y:],Z st for x,y st x in X & y in Y holds f1.[x,y] = f2.[x,y] holds f1 = f2; theorem :: FUNCT_2:119 for f being Function of [:X,Y:],Z st x in X & y in Y & Z <> {} holds f.[x,y] in Z; scheme FuncEx2{X, Y, Z() -> set, P[set,set,set]}: ex f being Function of [:X(),Y():],Z() st for x,y st x in X() & y in Y() holds P[x,y,f.[x,y]] provided for x,y st x in X() & y in Y() ex z st z in Z() & P[x,y,z]; scheme Lambda2{X, Y, Z() -> set, F(set,set)->set}: ex f being Function of [:X(),Y():],Z() st for x,y st x in X() & y in Y() holds f.[x,y] = F(x,y) provided for x,y st x in X() & y in Y() holds F(x,y) in Z(); theorem :: FUNCT_2:120 for f1,f2 being Function of [:C,D:],E st for c,d holds f1.[c,d] = f2.[c,d] holds f1 = f2; scheme FuncEx2D{X, Y, Z() -> non empty set, P[set,set,set]}: ex f being Function of [:X(),Y():],Z() st for x being Element of X() for y being Element of Y() holds P[x,y,f.[x,y]] provided for x being Element of X() for y being Element of Y() ex z being Element of Z() st P[x,y,z]; scheme Lambda2D{X, Y, Z() -> non empty set, F(Element of X(),Element of Y()) -> Element of Z()}: ex f being Function of [:X(),Y():],Z() st for x being Element of X() for y being Element of Y() holds f.[x,y]=F(x,y) ; begin :: PARTFUN1 theorem :: FUNCT_2:121 for f being set st f in Funcs(X,Y) holds f is Function of X,Y; scheme Lambda1C{A, B() -> set, C[set], F(set)->set, G(set)->set}: ex f being Function of A(),B() st for x st x in A() holds (C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x)) provided for x st x in A() holds (C[x] implies F(x) in B()) & (not C[x] implies G(x) in B()); canceled 8; theorem :: FUNCT_2:130 for f being PartFunc of X,Y st dom f = X holds f is Function of X,Y; theorem :: FUNCT_2:131 for f being PartFunc of X,Y st f is total holds f is Function of X,Y; theorem :: FUNCT_2:132 for f being PartFunc of X,Y st (Y = {} implies X = {}) & f is Function of X,Y holds f is total; theorem :: FUNCT_2:133 for f being Function of X,Y st (Y = {} implies X = {}) holds <:f,X,Y:> is total; theorem :: FUNCT_2:134 for f being Function of X,X holds <:f,X,X:> is total; canceled; theorem :: FUNCT_2:136 for f being PartFunc of X,Y st Y = {} implies X = {} ex g being Function of X,Y st for x st x in dom f holds g.x = f.x; canceled 4; theorem :: FUNCT_2:141 Funcs(X,Y) c= PFuncs(X,Y); theorem :: FUNCT_2:142 for f,g being Function of X,Y st (Y = {} implies X = {}) & f tolerates g holds f = g; theorem :: FUNCT_2:143 for f,g being Function of X,X st f tolerates g holds f = g; canceled; theorem :: FUNCT_2:145 for f being PartFunc of X,Y for g being Function of X,Y st Y = {} implies X = {} holds f tolerates g iff for x st x in dom f holds f.x = g.x; theorem :: FUNCT_2:146 for f being PartFunc of X,X for g being Function of X,X holds f tolerates g iff for x st x in dom f holds f.x = g.x; canceled; theorem :: FUNCT_2:148 for f being PartFunc of X,Y st Y = {} implies X = {} ex g being Function of X,Y st f tolerates g; theorem :: FUNCT_2:149 for f being PartFunc of X,X ex g being Function of X,X st f tolerates g; canceled; theorem :: FUNCT_2:151 for f,g being PartFunc of X,Y for h being Function of X,Y st (Y = {} implies X = {}) & f tolerates h & g tolerates h holds f tolerates g; theorem :: FUNCT_2:152 for f,g being PartFunc of X,X for h being Function of X,X st f tolerates h & g tolerates h holds f tolerates g; canceled; theorem :: FUNCT_2:154 for f,g being PartFunc of X,Y st (Y = {} implies X = {}) & f tolerates g ex h being Function of X,Y st f tolerates h & g tolerates h; theorem :: FUNCT_2:155 for f being PartFunc of X,Y for g being Function of X,Y st (Y = {} implies X = {}) & f tolerates g holds g in TotFuncs f; theorem :: FUNCT_2:156 for f being PartFunc of X,X for g being Function of X,X st f tolerates g holds g in TotFuncs f; canceled; theorem :: FUNCT_2:158 for f being PartFunc of X,Y for g being set st g in TotFuncs(f) holds g is Function of X,Y; theorem :: FUNCT_2:159 for f being PartFunc of X,Y holds TotFuncs f c= Funcs(X,Y); theorem :: FUNCT_2:160 TotFuncs <:{},X,Y:> = Funcs(X,Y); theorem :: FUNCT_2:161 for f being Function of X,Y st Y = {} implies X = {} holds TotFuncs <:f,X,Y:> = {f}; theorem :: FUNCT_2:162 for f being Function of X,X holds TotFuncs <:f,X,X:> = {f}; canceled; theorem :: FUNCT_2:164 for f being PartFunc of X,{y} for g being Function of X,{y} holds TotFuncs f = {g}; theorem :: FUNCT_2:165 for f,g being PartFunc of X,Y st g c= f holds TotFuncs f c= TotFuncs g; theorem :: FUNCT_2:166 for f,g being PartFunc of X,Y st dom g c= dom f & TotFuncs f c= TotFuncs g holds g c= f; theorem :: FUNCT_2:167 for f,g being PartFunc of X,Y st TotFuncs f c= TotFuncs g & (for y holds Y <> {y}) holds g c= f; theorem :: FUNCT_2:168 for f,g being PartFunc of X,Y st (for y holds Y <> {y}) & TotFuncs f = TotFuncs g holds f = g; :: from WAYBEL_1 definition let A,B be non empty set; cluster -> non empty Function of A,B; end;

Back to top