:: Functions from a Set to a Set
:: by Czes{\l}aw Byli\'nski
::
:: Received April 6, 1989
:: Copyright (c) 1990-2026 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 RELAT_1, XBOOLE_0, PARTFUN1, FUNCT_1, TARSKI, SUBSET_1, ZFMISC_1,
RELAT_2, MCART_1, SETFAM_1, FUNCT_2, GROUP_9;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, SETFAM_1, MCART_1,
RELAT_1, RELAT_2, FUNCT_1, RELSET_1, PARTFUN1;
constructors RELAT_2, PARTFUN1, MCART_1, SETFAM_1, RELSET_1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, RELSET_1,
GRFUNC_1, ZFMISC_1;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0, PARTFUN1, FUNCT_1;
equalities PARTFUN1, SUBSET_1;
expansions TARSKI, XBOOLE_0, PARTFUN1, FUNCT_1;
theorems TARSKI, RELAT_1, FUNCT_1, ZFMISC_1, PARTFUN1, GRFUNC_1, RELSET_1,
SUBSET_1, XBOOLE_0, XBOOLE_1, RELAT_2, MCART_1, SETFAM_1, XTUPLE_0;
schemes FUNCT_1, PARTFUN1, XBOOLE_0, RELSET_1, SUBSET_1;
begin :: Function from a set into a set
reserve P,Q,X,Y,Z for set, p,x,x9,x1,x2,y,z for object;
definition
let X,Y;
let R be Relation of X,Y;
attr R is quasi_total means
:Def1:
X = dom R if Y <> {} otherwise R = {};
consistency;
end;
registration
let X,Y;
cluster quasi_total for PartFunc of X,Y;
existence
proof
per cases;
suppose
A1: Y = {};
reconsider R = {} as PartFunc of X,Y by RELSET_1:12;
take R;
thus thesis by A1,Def1;
end;
suppose
A2: Y <> {};
then consider f being Function such that
A3: X = dom f and
A4: rng f c= Y by FUNCT_1:8;
reconsider R = f as PartFunc of X,Y by A3,A4,RELSET_1:4;
take R;
thus thesis by A2,A3,Def1;
end;
end;
end;
registration
let X,Y;
cluster total -> quasi_total for Relation of X,Y;
coherence
proof
let f be Relation of X,Y;
assume
A1: dom f = X;
per cases;
case Y <> {};
thus thesis by A1;
end;
case Y = {};
hence thesis;
end;
end;
end;
definition
let X,Y;
mode Function of X,Y is quasi_total PartFunc of X,Y;
end;
registration let X be empty set, Y be set;
cluster quasi_total -> total for Relation of X,Y;
coherence;
end;
registration let X be set, Y be non empty set;
cluster quasi_total -> total for Relation of X,Y;
coherence
by Def1;
end;
registration let X be set;
cluster quasi_total -> total for Relation of X,X;
coherence
proof
per cases;
suppose X = {};
hence thesis;
end;
suppose X <> {};
hence thesis;
end;
end;
end;
registration let X be set;
cluster quasi_total -> total for Relation of [:X,X:],X;
coherence
proof
per cases;
suppose X = {};
hence thesis;
end;
suppose X <> {};
hence thesis;
end;
end;
end;
theorem
for f being Function holds f is Function of dom f, rng f
proof
let f be Function;
reconsider R = f as Relation of dom f, rng f by RELSET_1:4;
rng R <> {} or rng R = {};
hence thesis by Def1;
end;
theorem Th2:
for f being Function st rng f c= Y holds f is Function of dom f, Y
proof
let f be Function;
assume rng f c= Y;
then reconsider R = f as Relation of dom f,Y by RELSET_1:4;
Y = {} or Y <> {};
then R is quasi_total by Def1;
hence thesis;
end;
theorem
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
proof
let f be Function such that
A1: dom f = X and
A2: for x st x in X holds f.x in Y;
rng f c= Y
proof
let y be object;
assume y in rng f;
then ex x being object st x in X & y = f.x by A1,FUNCT_1:def 3;
hence thesis by A2;
end;
then reconsider R = f as Relation of dom f,Y by RELSET_1:4;
Y = {} or Y <> {};
then R is quasi_total by Def1;
hence thesis by A1;
end;
theorem Th4:
for f being Function of X,Y st Y <> {} & x in X holds f.x in rng f
proof
let f be Function of X,Y;
assume Y <> {};
then dom f = X by Def1;
hence thesis by FUNCT_1:def 3;
end;
theorem Th5:
for f being Function of X,Y st Y <> {} & x in X holds f.x in Y
proof
let f be Function of X,Y;
assume Y <> {} & x in X;
then f.x in rng f by Th4;
hence thesis;
end;
theorem
for f being Function of X,Y st (Y = {} implies X = {}) & rng f c= Z
holds f is Function of X,Z
proof
let f be Function of X,Y;
assume Y <> {} or X = {};
then
A1: dom f = X by Def1;
assume
A2: rng f c= Z;
now
assume Z = {};
then rng f = {} by A2;
hence X = {} by A1,RELAT_1:42;
end;
hence thesis by A1,A2,Def1,RELSET_1:4;
end;
theorem
for f being Function of X,Y st (Y = {} implies X = {}) & Y c= Z holds
f is Function of X,Z by RELSET_1:7;
scheme
FuncEx1{X, Y() -> set, P[object,object]}:
ex f being Function of X(),Y() st
for x being object st x in X() holds P[x,f.x]
provided
A1: for x being object st x in X() ex y being object st y in Y() & P[x,y]
proof
consider f being Function such that
A2: dom f = X() & rng f c= Y() and
A3: for x being object st x in X() holds P[x,f.x] from FUNCT_1:sch 6(A1);
reconsider f as Function of X(),Y() by A2,Th2;
take f;
thus thesis by A3;
end;
scheme
Lambda1{X, Y() -> set, F(object)->object}:
ex f being Function of X(),Y() st
for x being object st x in X() holds f.x = F(x)
provided
A1: for x being object st x in X() holds F(x) in Y()
proof
defpred P[object,object] means $2 = F($1);
A2: for x being object st x in X()
ex y being object st y in Y() & P[x,y] by A1;
thus ex f being Function of X(),Y() st
for x being object st x in X() holds P[x,f.x]
from FuncEx1(A2);
end;
definition
let X,Y;
func Funcs(X,Y) -> set means
:Def2:
x in it iff ex f being Function st x = f & dom f = X & rng f c= Y;
existence
proof
defpred P[object] means
ex f being Function st $1 = f & dom f = X & rng f c=
Y;
consider F being set such that
A1: for z being object holds z in F iff z in bool [:X,Y:] & P[z]
from XBOOLE_0:sch 1;
take F;
let z;
thus z in F implies ex f being Function st z = f & dom f = X & rng f c= Y
by A1;
given f being Function such that
A2: z = f and
A3: dom f = X & rng f c= Y;
f c= [:X,Y:]
proof
let p be object;
assume
A4: p in f;
then consider x,y being object such that
A5: p = [x,y] by RELAT_1:def 1;
reconsider y as set by TARSKI:1;
A6: x in dom f by A4,A5,XTUPLE_0:def 12;
then y = f.x by A4,A5,FUNCT_1:def 2;
then y in rng f by A6,FUNCT_1:def 3;
hence thesis by A3,A5,A6,ZFMISC_1:def 2;
end;
hence thesis by A1,A2,A3;
end;
uniqueness
proof
let F1,F2 be set such that
A7: x in F1 iff ex f being Function st x = f & dom f = X & rng f c= Y and
A8: x in F2 iff ex f being Function st x = f & dom f = X & rng f c= Y;
for x being object holds x in F1 iff x in F2
proof let x be object;
x in F1 iff ex f being Function st x = f & dom f = X & rng f c= Y by A7;
hence thesis by A8;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th8:
for f being Function of X,Y st Y = {} implies X = {} holds f in Funcs(X,Y)
proof
let f be Function of X,Y;
assume Y = {} implies X = {};
then
A1: dom f = X by Def1;
rng f c= Y;
hence thesis by A1,Def2;
end;
theorem
for f being Function of X,X holds f in Funcs(X,X) by Th8;
registration
let X be set, Y be non empty set;
cluster Funcs(X,Y) -> non empty;
coherence by Th8;
end;
registration
let X be set;
cluster Funcs(X,X) -> non empty;
coherence by Th8;
end;
registration
let X be non empty set, Y be empty set;
cluster Funcs(X,Y) -> empty;
coherence
proof
assume Funcs(X,Y) is non empty;
then consider f being Function such that
the Element of Funcs(X,Y) = f and
A1: dom f = X and
A2: rng f c= {} by Def2;
rng f = {} by A2;
hence contradiction by A1,RELAT_1:42;
end;
end;
theorem
for f being Function of X,Y st for y being object st y in Y
ex x being object st x in X & y = f.x
holds rng f = Y
proof
let f be Function of X,Y such that
A1: for y being object st y in Y ex x being object st x in X & y = f.x;
per cases;
suppose Y = {};
hence thesis;
end;
suppose A2: Y <> {};
for y being object holds y in rng f iff y in Y
proof let y be object;
dom f = X by A2,Def1;
then y in rng f iff ex x being object st x in X & y = f.x
by FUNCT_1:def 3;
hence thesis by A1;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th11:
for f being Function of X,Y st y in rng f
ex x being object st x in X & f.x = y
proof
let f be Function of X,Y;
assume
A1: y in rng f;
then dom f = X by Def1;
hence thesis by A1,FUNCT_1:def 3;
end;
theorem Th12:
for f1,f2 being Function of X,Y st
for x being object st x in X holds f1.x = f2.x
holds f1 = f2
proof
let f1,f2 be Function of X,Y;
per cases;
suppose Y = {};
hence thesis;
end;
suppose Y <> {};
then dom f1 = X & dom f2 = X by Def1;
hence thesis;
end;
end;
theorem Th13:
for f being quasi_total Relation of X,Y for g being quasi_total
Relation of Y,Z st Y = {} implies Z = {} or X = {} holds f*g is quasi_total
proof
let f be quasi_total Relation of X,Y;
let g be quasi_total Relation of Y,Z such that
A1: Y = {} implies Z = {} or X = {};
per cases;
case
A2: Z <> {};
then
A3: dom g = Y by Def1;
dom f = X & rng f c= Y by A1,A2,Def1;
hence thesis by A3,RELAT_1:27;
end;
case Z = {};
hence thesis;
end;
end;
theorem
for f being Function of X,Y for g being Function of Y,Z st Z <> {} &
rng f = Y & rng g = Z holds rng(g*f) = Z
proof
let f be Function of X,Y;
let g be Function of Y,Z;
assume Z <> {};
then dom g = Y by Def1;
hence thesis by RELAT_1:28;
end;
theorem Th15:
for x being object
for f being Function of X,Y, g being Function st Y <> {} & x in
X holds (g*f).x = g.(f.x)
proof let x be object;
let f be Function of X,Y, g be Function;
assume Y <> {};
then X = dom f by Def1;
hence thesis by FUNCT_1:13;
end;
theorem
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
proof
let f be Function of X,Y;
assume
A1: Y <> {};
thus rng f = Y implies for Z st Z <> {} for g,h being Function of Y,Z st g*f
= h*f holds g = h
proof
assume
A2: rng f = Y;
let Z such that
A3: Z <> {};
let g,h be Function of Y,Z;
dom g = Y & dom h = Y by A3,Def1;
hence thesis by A2,FUNCT_1:86;
end;
assume
A4: for Z st Z <> {} for g,h being Function of Y,Z st g*f = h*f holds g = h;
for g,h being Function st dom g = Y & dom h = Y & g*f = h*f holds g = h
proof
let g,h be Function;
assume that
A5: dom g = Y and
A6: dom h = Y;
A7: rng g <> {} by A1,A5,RELAT_1:42;
A8: g is Function of Y,rng g \/ rng h by A5,Th2,XBOOLE_1:7;
h is Function of Y,rng g \/ rng h by A6,Th2,XBOOLE_1:7;
hence thesis by A4,A7,A8;
end;
hence thesis by FUNCT_1:16;
end;
theorem
for f being Relation of X,Y holds (id X)*f = f & f*(id Y) = f
proof
let f be Relation of X,Y;
dom f c= X;
hence (id X)*f = f by RELAT_1:51;
rng f c= Y;
hence thesis by RELAT_1:53;
end;
theorem
for f being Function of X,Y for g being Function of Y,X st f*g = id Y
holds rng f = Y
proof
let f be (Function of X,Y),g be Function of Y,X;
assume f*g = id Y;
then rng(f*g) = Y;
then Y c= rng f by RELAT_1:26;
hence thesis;
end;
theorem
for f being Function of X,Y st Y = {} implies X = {} holds f is
one-to-one iff
for x1,x2 being object st x1 in X & x2 in X & f.x1 = f.x2 holds x1 = x2
proof
let f be Function of X,Y;
assume Y = {} implies X = {};
then dom f = X by Def1;
hence thesis;
end;
theorem
for f being Function of X,Y for g being Function of Y,Z st (Z = {}
implies Y = {}) & g*f is one-to-one holds f is one-to-one
proof
let f be Function of X,Y;
let g be Function of Y,Z;
assume Z <> {} or Y = {};
then
A1: Y = dom g by Def1;
rng f c= Y;
hence thesis by A1,FUNCT_1:25;
end;
theorem
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
proof
let f be Function of X,Y;
assume that
A1: X <> {} and
A2: Y <> {};
A3: dom f = X by A2,Def1;
thus f is one-to-one implies for Z for g,h being Function of Z,X st f*g = f*
h holds g = h
proof
assume
A4: f is one-to-one;
let Z;
let g,h be Function of Z,X;
A5: rng g c= X & rng h c= X;
dom g = Z & dom h = Z by A1,Def1;
hence thesis by A3,A4,A5,FUNCT_1:27;
end;
assume
A6: for Z for g,h being Function of Z,X st f*g = f*h holds g = h;
now
let g,h be Function;
assume rng g c= dom f & rng h c= dom f & dom g = dom h;
then g is Function of dom g,X & h is Function of dom g,X by A3,Th2;
hence f*g = f*h implies g = h by A6;
end;
hence thesis by FUNCT_1:27;
end;
theorem
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
proof
let f be Function of X,Y;
let g be Function of Y,Z;
assume that
A1: Z <> {} and
A2: rng(g*f) = Z and
A3: g is one-to-one;
A4: dom g = Y by A1,Def1;
rng(g*f) c= rng g by RELAT_1:26;
then rng g = rng(g*f) by A2;
then Y c= rng f by A3,A4,FUNCT_1:29;
hence thesis;
end;
definition
let Y be set;
let f be Y-valued Relation;
attr f is onto means
:Def3:
rng f = Y;
end;
theorem
for f being Function of X,Y for g being Function of Y,X st g*f = id X
holds f is one-to-one & g is onto
proof
let f be Function of X,Y;
let g be Function of Y,X;
assume that
A1: g*f = id X;
thus f is one-to-one
proof
per cases;
suppose Y = {};
hence thesis;
end;
suppose Y <> {};
then dom f = X by Def1;
hence thesis by A1,FUNCT_1:31;
end;
end;
rng(g*f) = X by A1;
then X c= rng g by RELAT_1:26;
hence rng g = X;
end;
theorem
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
proof
let f be Function of X,Y;
let g be Function of Y,Z;
assume Z <> {} or Y = {};
then Y = dom g by Def1;
hence thesis by FUNCT_1:26;
end;
theorem Th25:
for f being Function of X,Y st f is one-to-one & rng f = Y holds
f" is Function of Y,X
proof
let f be Function of X,Y;
assume that
A1: f is one-to-one and
A2: rng f = Y;
A3: rng(f") c= X
proof
let x be object;
assume x in rng(f");
then x in dom f by A1,FUNCT_1:33;
hence thesis;
end;
dom(f") = Y by A1,A2,FUNCT_1:33;
then reconsider R = f" as Relation of Y,X by A3,RELSET_1:4;
R is quasi_total
proof
per cases;
case X <> {};
thus thesis by A1,A2,FUNCT_1:33;
end;
case X = {};
then rng f = {};
then dom(f") = {} by A1,FUNCT_1:32;
hence thesis;
end;
end;
hence thesis;
end;
theorem
for f being Function of X,Y st Y <> {} & f is one-to-one & x in X
holds (f").(f.x) = x
proof
let f be Function of X,Y;
assume Y <> {};
then dom f = X by Def1;
hence thesis by FUNCT_1:34;
end;
theorem
for X be set, Y,Z be non empty set for f be Function of X,Y
for g be Function of Y,Z holds f is onto & g is onto implies g*f is onto
proof
let X be set, Y,Z be non empty set;
let f be Function of X,Y;
let g be Function of Y,Z;
assume that
A1: f is onto and
A2: g is onto;
rng f = Y by A1
.= dom g by Def1;
then rng(g*f) = rng g by RELAT_1:28
.= Z by A2;
hence thesis;
end;
theorem
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 being object holds y in Y & g.y = x iff x in X
& f.x = y holds g = f"
proof
let f be Function of X,Y;
let g be Function of Y,X;
assume X <> {} & Y <> {};
then dom f = X & dom g = Y by Def1;
hence thesis by FUNCT_1:32;
end;
theorem
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
proof
let f be Function of X,Y;
assume Y <> {};
then dom f = X by Def1;
hence thesis by FUNCT_1:39;
end;
theorem
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"
proof
let f be Function of X,Y;
let g be Function of Y,X;
assume X <> {} & Y <> {};
then dom f = X & dom g = Y by Def1;
hence thesis by FUNCT_1:41;
end;
theorem
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
proof
let f be Function of X,Y;
assume Y <> {};
then
A1: dom f = X by Def1;
given g being Function of Y,X such that
A2: g*f = id X;
thus thesis by A2,A1,FUNCT_1:31;
end;
theorem Th32:
for f being Function of X,Y st (Y = {} implies X = {}) & Z c= X
holds f|Z is Function of Z,Y
proof
let f be Function of X,Y such that
A1: Y = {} implies X = {} and
A2: Z c= X;
dom f = X by A1,Def1;
then
A3: Z = dom(f|Z) by A2,RELAT_1:62;
rng(f|Z) c= Y;
then reconsider R = f|Z as Relation of Z,Y by A3,RELSET_1:4;
R is quasi_total
proof
per cases;
case Y <> {};
dom f = X by A1,Def1;
hence thesis by A2,RELAT_1:62;
end;
case Y = {};
hence thesis;
end;
end;
hence thesis;
end;
theorem
for f being Function of X,Y st X c= Z holds f|Z = f by RELSET_1:19;
theorem
for f being Function of X,Y st Y <> {} & x in X & f.x in Z holds (Z|`f)
.x = f.x
proof
let f be Function of X,Y;
assume that
A1: Y <> {} & x in X and
A2: f.x in Z;
x in dom f by A1,Def1;
then x in dom(Z|`f) by A2,FUNCT_1:54;
hence thesis by FUNCT_1:55;
end;
theorem
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
proof
let f be Function of X,Y;
assume Y <> {};
then
A1: dom f = X by Def1;
let y;
given x such that
A2: x in X & x in P & y = f.x;
thus thesis by A1,A2,FUNCT_1:def 6;
end;
theorem
for f being Function of X,Y holds f.:P c= Y;
::$CT
theorem
for f being Function of X,Y st Y <> {} for x holds x in f"Q iff x in X
& f.x in Q
proof
let f be Function of X,Y;
assume Y <> {};
then dom f = X by Def1;
hence thesis by FUNCT_1:def 7;
end;
theorem
for f being PartFunc of X,Y holds f"Q c= X;
theorem Th39:
for f being Function of X,Y st Y = {} implies X = {} holds f"Y = X
proof
let f be Function of X,Y;
rng f /\ Y = rng f by XBOOLE_1:28;
then
A1: f"Y = f"(rng f) by RELAT_1:133;
assume Y <> {} or X = {};
then dom f = X by Def1;
hence thesis by A1,RELAT_1:134;
end;
theorem
for f being Function of X,Y holds
(for y being object st y in Y holds f"{y} <> {})
iff rng f = Y
by FUNCT_1:73,FUNCT_1:72;
theorem Th41:
for f being Function of X,Y st (Y = {} implies X = {}) & P c= X
holds P c= f"(f.:P)
proof
let f be Function of X,Y;
assume Y <> {} or X = {};
then dom f = X by Def1;
hence thesis by FUNCT_1:76;
end;
theorem
for f being Function of X,Y st Y = {} implies X = {} holds f"(f.:X) = X
proof
let f be Function of X,Y;
assume Y <> {} or X = {};
then
A1: dom f = X by Def1;
then f"(rng f) = X by RELAT_1:134;
hence thesis by A1,RELAT_1:113;
end;
theorem
for f being Function of X,Y for g being Function of Y,Z st (Z = {}
implies Y = {}) holds f"Q c= (g*f)"(g.:Q)
proof
let f be Function of X,Y;
let g be Function of Y,Z;
assume Z <> {} or Y = {};
then
A1: dom g = Y by Def1;
rng f c= Y;
hence thesis by A1,FUNCT_1:90;
end;
theorem
for f being Function of {},Y holds f.:P = {};
theorem
for f being Function of {},Y holds f"Q = {};
theorem
for x being object
for f being Function of {x},Y st Y <> {} holds f.x in Y
proof let x be object;
let f be Function of {x},Y;
assume Y <> {};
then
A1: dom f = {x} by Def1;
rng f c= Y;
then {f.x} c= Y by A1,FUNCT_1:4;
hence thesis by ZFMISC_1:31;
end;
theorem Th47:
for x being object
for f being Function of {x},Y st Y <> {} holds rng f = {f.x}
proof let x be object;
let f be Function of {x},Y;
assume Y <> {};
then dom f = {x} by Def1;
hence thesis by FUNCT_1:4;
end;
theorem
for x being object
for f being Function of {x},Y st Y <> {} holds f.:P c= {f.x}
proof let x be object;
let f be Function of {x},Y;
f.:P c= rng f by RELAT_1:111;
hence thesis by Th47;
end;
theorem Th49:
for y being object
for f being Function of X,{y} st x in X holds f.x = y
proof let y be object;
let f be Function of X,{y};
x in X implies f.x in {y} by Th5;
hence thesis by TARSKI:def 1;
end;
theorem Th50:
for y being object
for f1,f2 being Function of X,{y} holds f1 = f2
proof let y be object;
let f1,f2 be Function of X,{y};
for x being object holds x in X implies f1.x = f2.x
proof let x be object;
assume
A1: x in X;
then f1.x = y by Th49;
hence thesis by A1,Th49;
end;
hence thesis by Th12;
end;
theorem Th51:
for f being Function of X,X holds dom f = X
proof
X = {} implies X = {};
hence thesis by Def1;
end;
registration
let X,Y be set;
let f be quasi_total PartFunc of X,Y;
let g be quasi_total PartFunc of X,X;
cluster f*g -> quasi_total for PartFunc of X,Y;
coherence
proof
per cases;
suppose
Y = {};
hence thesis;
end;
suppose
A1: Y <> {};
then dom f = X by Def1;
then dom(f*g) = g"X by RELAT_1:147
.= dom g by RELSET_1:22
.= X by Th51;
hence thesis by A1,Def1;
end;
end;
end;
registration
let X,Y be set;
let f be quasi_total PartFunc of Y,Y;
let g be quasi_total PartFunc of X,Y;
cluster f*g -> quasi_total for PartFunc of X,Y;
coherence
proof
per cases;
suppose
Y = {};
hence thesis;
end;
suppose
A1: Y <> {};
dom f = Y by Th51;
then dom(f*g) = g"Y by RELAT_1:147
.= dom g by RELSET_1:22
.= X by A1,Def1;
hence thesis by A1,Def1;
end;
end;
end;
theorem Th52:
for f,g being Relation of X,X st rng f = X & rng g = X holds rng (g*f) = X
proof
let f,g be Relation of X,X;
assume that
A1: rng f = X and
A2: rng g = X;
thus rng(g*f) = f.:X by A2,RELAT_1:127
.= X by A1,RELSET_1:22;
end;
theorem
for f,g being Function of X,X st g*f = f & rng f = X holds g = id X
proof
let f,g be Function of X,X;
dom g = X by Th51;
hence thesis by FUNCT_1:23;
end;
theorem
for f,g being Function of X,X st f*g = f & f is one-to-one holds g = id X
proof
let f,g be Function of X,X;
A1: rng g c= X;
dom f = X & dom g = X by Th51;
hence thesis by A1,FUNCT_1:28;
end;
theorem Th55:
for f being Function of X,X holds f is one-to-one iff
for x1,x2 being object
st x1 in X & x2 in X & f.x1 = f.x2 holds x1 = x2
proof
let f be Function of X,X;
dom f = X by Th51;
hence thesis;
end;
definition
let X, Y;
let f be X-defined Y-valued Function;
attr f is bijective means
f is one-to-one onto;
end;
registration
let X, Y be set;
cluster bijective -> one-to-one onto for PartFunc of X,Y;
coherence;
cluster one-to-one onto -> bijective for PartFunc of X,Y;
coherence;
end;
registration
let X;
cluster bijective for Function of X,X;
existence
proof
take id X;
thus id X is one-to-one & rng id X = X;
end;
end;
definition
let X;
mode Permutation of X is bijective Function of X,X;
end;
theorem Th56:
for f being Function of X, X st f is one-to-one & rng f = X
holds f is Permutation of X
proof
let f be Function of X, X;
assume that
A1: f is one-to-one and
A2: rng f = X;
f is onto by A2;
hence thesis by A1;
end;
theorem
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 by Th55;
registration
let X;
let f,g be onto PartFunc of X,X;
cluster f*g -> onto for PartFunc of X,X;
coherence
proof
rng f = X & rng g = X by Def3;
then rng(f*g) = X by Th52;
hence thesis;
end;
end;
registration
let X;
let f,g be bijective Function of X,X;
cluster g*f -> bijective for Function of X,X;
coherence;
end;
registration
let X;
cluster reflexive total -> bijective for Function of X,X;
coherence
proof
let f be Function of X,X;
assume
A1: f is reflexive total;
A2: field f = dom f \/ rng f by RELAT_1:def 6;
thus f is one-to-one
proof
let x1,x2 be object such that
A3: x1 in dom f and
A4: x2 in dom f and
A5: f.x1 = f.x2;
x1 in field f by A2,A3,XBOOLE_0:def 3;
then [x1,x1] in f by A1,RELAT_2:def 1,def 9;
then
A6: x1 = f.x1 by A3,FUNCT_1:def 2;
x2 in field f by A2,A4,XBOOLE_0:def 3;
then [x2,x2] in f by A1,RELAT_2:def 1,def 9;
hence thesis by A4,A5,A6,FUNCT_1:def 2;
end;
thus rng f c= X;
let x be object;
assume x in X;
then x in dom f by PARTFUN1:def 2;
then x in field f by A2,XBOOLE_0:def 3;
then [x,x] in f by A1,RELAT_2:def 1,def 9;
hence thesis by XTUPLE_0:def 13;
end;
end;
definition
let X;
let f be Permutation of X;
redefine func f" -> Permutation of X; :: redefines " (FUNCT_1, definition)
coherence
proof
dom f = X by Th51;
then
A1: rng(f") = X by FUNCT_1:33;
rng f = X by Def3;
then f" is Function of X,X by Th25;
hence thesis by A1,Th56;
end;
end;
theorem
for f,g being Permutation of X st g*f = g holds f = id X
proof
let f,g be Permutation of X;
A1: rng f c= X;
dom f = X & dom g = X by Th51;
hence thesis by A1,FUNCT_1:28;
end;
theorem
for f,g being Permutation of X st g*f = id X holds g = f"
proof
let f,g be Permutation of X;
A1: dom f = X by Th51;
rng f= X & dom g = X by Def3,Th51;
hence thesis by A1,FUNCT_1:41;
end;
theorem
for f being Permutation of X holds (f")*f =id X & f*(f") = id X
proof
let f be Permutation of X;
dom f = X & rng f = X by Def3,Th51;
hence thesis by FUNCT_1:39;
end;
theorem Th61:
for f being Permutation of X st P c= X holds f.:(f"P) = P & f"(f .:P) = P
proof
let f be Permutation of X such that
A1: P c= X;
dom f = X by Th51;
then
A2: P c= f"(f.:P) by A1,FUNCT_1:76;
f"(f.:P) c= P & rng f = X by Def3,FUNCT_1:82;
hence thesis by A1,A2,FUNCT_1:77;
end;
reserve D for non empty set;
registration
let X,D,Z;
let f be Function of X,D;
let g be Function of D,Z;
cluster g*f -> quasi_total for PartFunc of X,Z;
coherence by Th13;
end;
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; :: redefines . (FUNCT_1, definition)
coherence
proof
D is non empty or D is empty;
hence thesis by Th5,SUBSET_1:def 1;
end;
end;
scheme
FuncExD{C, D() -> non empty set, P[object,object]}:
ex f being Function of C(),D()
st for x being Element of C() holds P[x,f.x]
provided
A1: for x being Element of C() ex y being Element of D() st P[x,y]
proof
defpred R[object,object] means $1 in C() & $2 in D() & P[ $1,$2];
A2: for x being object st x in C() ex y being object st y in D() & R[x,y]
proof
let x be object;
assume
A3: x in C();
then ex y being Element of D() st P[x,y] by A1;
hence thesis by A3;
end;
consider f being Function of C(),D() such that
A4: for x being object st x in C() holds R[x,f.x] from FuncEx1(A2);
take f;
let x be Element of C();
thus thesis by A4;
end;
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)
proof
defpred P[Element of C(),set] means $2 = F($1);
A1: for x being Element of C() ex y being Element of D() st P[x,y];
thus ex f being Function of C(),D() st for x being Element of C() holds P[x,
f.x] from FuncExD(A1);
end;
theorem Th62:
for f1,f2 being Function of X,Y st for x being Element of X
holds f1.x = f2.x holds f1 = f2
proof
let f1,f2 be Function of X,Y;
assume for x being Element of X holds f1.x = f2.x;
then for x being object st x in X holds f1.x = f2.x;
hence thesis by Th12;
end;
theorem Th63:
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
proof
let P be set;
let f be Function of X,Y;
let y;
assume y in f.:P;
then consider x being object such that
A1: x in dom f and
A2: x in P & y = f.x by FUNCT_1:def 6;
reconsider x as set by TARSKI:1;
take x;
thus x in X by A1;
thus thesis by A2;
end;
theorem
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
proof
let f be Function of X,Y;
let y;
assume y in f.:P;
then consider x such that
A1: x in X and
A2: x in P & y = f.x by Th63;
reconsider c = x as Element of X by A1;
take c;
thus thesis by A2;
end;
begin :: PARTFUN1
theorem Th65:
for f being set st f in Funcs(X,Y) holds f is Function of X,Y
proof
let f be set;
assume f in Funcs(X,Y);
then
( not(Y = {} & X <> {}))& ex f9 being Function st f9 = f & dom f9 = X &
rng f9 c= Y by Def2;
hence thesis by Def1,RELSET_1:4;
end;
scheme
Lambda1C{A, B() -> set, C[object], F, G(object)->object}:
ex f being Function of A(),B() st
for x being object st x in A() holds (C[ x] implies f.x = F(x)) & (
not C[ x] implies f.x = G(x))
provided
A1: for x being object st x in A()
holds (C[ x] implies F(x) in B()) & (not C[ x] implies G(x) in B())
proof
A2: now
set x = the Element of A();
assume
A3: B() = {};
assume
A4: A() <> {};
then C[ x] implies F(x) in B() by A1;
hence contradiction by A1,A3,A4;
end;
consider f being Function such that
A5: dom f = A() and
A6: for x being object st x in A() holds (C[ x] implies f.x = F(x)) &
(not C[ x]
implies f.x = G(x)) from PARTFUN1:sch 1;
rng f c= B()
proof
let y be object;
assume y in rng f;
then consider x being object such that
A7: x in dom f and
A8: y = f.x by FUNCT_1:def 3;
A9: not C[ x] implies f.x = G(x) by A5,A6,A7;
C[ x] implies f.x = F(x) by A5,A6,A7;
hence thesis by A1,A5,A7,A8,A9;
end;
then f is Function of A(),B() by A5,A2,Def1,RELSET_1:4;
hence thesis by A6;
end;
theorem
for f being PartFunc of X,Y st dom f = X holds f is Function of X,Y
proof
let f be PartFunc of X,Y;
rng f c= Y;
hence thesis by Th2;
end;
theorem
for f being PartFunc of X,Y st f is total holds f is Function of X,Y;
theorem
for f being PartFunc of X,Y st (Y = {} implies X = {}) & f is Function
of X,Y holds f is total;
theorem
for f being Function of X,Y st (Y = {} implies X = {}) holds
<:f,X,Y:> is total;
registration
let X; let f be Function of X,X;
cluster <:f,X,X:> -> total;
coherence;
end;
theorem Th70:
for f being PartFunc of X,Y st Y = {} implies X = {} ex g being
Function of X,Y st for x being object st x in dom f holds g.x = f.x
proof
let f be PartFunc of X,Y such that
A1: Y = {} implies X = {};
per cases;
suppose Y = {};
then reconsider g = f as Function of X,Y by A1;
take g;
thus thesis;
end;
suppose
A2: Y <> {};
deffunc F(object) = f.$1;
defpred P[object] means $1 in dom f;
set y = the Element of Y;
deffunc G(object) = y;
A3: for x being object st x in X
holds (P[ x] implies F(x) in Y) & (not P[ x] implies G
(x) in Y) by A2,PARTFUN1:4;
consider g being Function of X,Y such that
A4: for x being object st x in X holds (P[ x] implies g.x = F(x)) & (not P[ x]
implies g.x = G(x)) from Lambda1C(A3);
take g;
thus thesis by A4;
end;
end;
theorem
Funcs(X,Y) c= PFuncs(X,Y)
proof
let x be object;
assume x in Funcs(X,Y);
then ex f being Function st x = f & dom f = X & rng f c= Y by Def2;
hence thesis by PARTFUN1:def 3;
end;
theorem
for f,g being Function of X,Y st (Y = {} implies X = {}) & f
tolerates g holds f = g by PARTFUN1:66;
theorem
for f,g being Function of X,X st f tolerates g holds f = g by PARTFUN1:66;
theorem Th74:
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 being object st x in dom f holds f.x = g.x
proof
let f be PartFunc of X,Y;
let g be Function of X,Y;
assume Y = {} implies X = {};
then dom g = X by Def1;
hence thesis by PARTFUN1:53;
end;
theorem
for f being PartFunc of X,X for g being Function of X,X holds f
tolerates g iff for x being object st x in dom f holds f.x = g.x
proof
let f be PartFunc of X,X;
let g be Function of X,X;
X = {} implies X = {};
hence thesis by Th74;
end;
theorem Th76:
for f being PartFunc of X,Y st Y = {} implies X = {} ex g being
Function of X,Y st f tolerates g
proof
let f be PartFunc of X,Y;
assume
A1: Y = {} implies X = {};
then consider g being Function of X,Y such that
A2: for x being object st x in dom f holds g.x = f.x by Th70;
take g;
thus thesis by A1,A2,Th74;
end;
theorem
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 by PARTFUN1:67;
theorem
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
proof
let f,g be PartFunc of X,Y;
assume ( Y = {} implies X = {})& f tolerates g;
then
ex h being PartFunc of X,Y st h is total & f tolerates h & g tolerates h
by PARTFUN1:68;
hence thesis;
end;
theorem
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 by PARTFUN1:def 5;
theorem
for f being PartFunc of X,X for g being Function of X,X st f tolerates
g holds g in TotFuncs f by PARTFUN1:def 5;
theorem Th81:
for f being PartFunc of X,Y for g being set st g in TotFuncs(f)
holds g is Function of X,Y
proof
let f be PartFunc of X,Y;
let g be set;
assume g in TotFuncs(f);
then
ex g9 being PartFunc of X,Y st g9 = g & g9 is total & f tolerates g9 by
PARTFUN1:def 5;
hence thesis;
end;
theorem
for f being PartFunc of X,Y holds TotFuncs f c= Funcs(X,Y)
proof
let f be PartFunc of X,Y;
per cases;
suppose Y = {} & X <> {};
hence thesis;
end;
suppose
A1: Y <> {} or X = {};
let g be object;
assume g in TotFuncs f;
then g is Function of X,Y by Th81;
hence thesis by A1,Th8;
end;
end;
theorem
TotFuncs <:{},X,Y:> = Funcs(X,Y)
proof
per cases;
suppose
A1: Y = {} & X <> {};
then TotFuncs <:{},X,Y:> = {};
hence thesis by A1;
end;
suppose
A2: Y = {} implies X = {};
for g being object holds g in TotFuncs <:{},X,Y:> iff g in Funcs(X,Y)
proof
let g be object;
thus g in TotFuncs <:{},X,Y:> implies g in Funcs(X,Y)
proof
assume g in TotFuncs <:{},X,Y:>;
then g is Function of X,Y by Th81;
hence thesis by A2,Th8;
end;
assume
A3: g in Funcs(X,Y);
then reconsider g9 = g as PartFunc of X,Y by Th65;
A4: <:{},X,Y:> tolerates g9 by PARTFUN1:60;
g is Function of X,Y by A3,Th65;
hence thesis by A2,A4,PARTFUN1:def 5;
end;
hence thesis by TARSKI:2;
end;
end;
theorem
for f being Function of X,Y st Y = {} implies X = {} holds
TotFuncs <:f,X,Y:> = {f} by PARTFUN1:72;
theorem
for f being Function of X,X holds TotFuncs <:f,X,X:> = {f} by PARTFUN1:72;
theorem
for f being PartFunc of X,{y} for g being Function of X,{y} holds
TotFuncs f = {g}
proof
let f be PartFunc of X,{y};
let g be Function of X,{y};
for h being object holds h in TotFuncs f iff h = g
proof
let h be object;
thus h in TotFuncs f implies h = g
proof
assume h in TotFuncs f;
then h is Function of X,{y} by Th81;
hence thesis by Th50;
end;
f tolerates g by PARTFUN1:61;
hence thesis by PARTFUN1:def 5;
end;
hence thesis by TARSKI:def 1;
end;
theorem
for f,g being PartFunc of X,Y st g c= f holds TotFuncs f c= TotFuncs g
proof
let f,g be PartFunc of X,Y such that
A1: g c= f;
let h be object;
assume
A2: h in TotFuncs f;
then reconsider h9=h as PartFunc of X,Y by PARTFUN1:69;
A3: h9 is total by A2,PARTFUN1:70;
g tolerates h9 by A1,A2,PARTFUN1:58,71;
hence thesis by A3,PARTFUN1:def 5;
end;
theorem Th88:
for f,g being PartFunc of X,Y st dom g c= dom f & TotFuncs f c=
TotFuncs g holds g c= f
proof
let f,g be PartFunc of X,Y such that
A1: dom g c= dom f;
now
per cases;
suppose Y = {} & X <> {};
hence thesis;
end;
suppose
A2: Y = {} implies X = {};
thus TotFuncs f c= TotFuncs g implies g c= f
proof
assume
A3: TotFuncs f c= TotFuncs g;
for x being object st x in dom g holds g.x = f.x
proof
let x be object;
consider h being Function of X,Y such that
A4: f tolerates h by A2,Th76;
h in TotFuncs f by A2,A4,PARTFUN1:def 5;
then
A5: g tolerates h by A3,PARTFUN1:71;
assume x in dom g;
then x in dom f /\ dom g by A1,XBOOLE_0:def 4;
hence thesis by A5,A2,A4,PARTFUN1:67,def 4;
end;
hence thesis by A1,GRFUNC_1:2;
end;
end;
end;
hence thesis;
end;
theorem Th89:
for f,g being PartFunc of X,Y st TotFuncs f c= TotFuncs g & (
for y holds Y <> {y}) holds g c= f
proof
let f,g be PartFunc of X,Y such that
A1: TotFuncs f c= TotFuncs g and
A2: for y holds Y <> {y};
now
per cases;
suppose Y = {};
hence dom g c= dom f;
end;
suppose
A3: Y <> {};
thus dom g c= dom f
proof
deffunc F(object) = f.$1;
defpred P[object] means $1 in dom f;
let x be object such that
A4: x in dom g and
A5: not x in dom f;
A6: Y <> {g.x} by A2;
g.x in Y by A4,PARTFUN1:4;
then consider y being object such that
A7: y in Y and
A8: y <> g.x by A6,ZFMISC_1:35;
deffunc G(object) = y;
A9: for x9 being object st x9 in X
holds (P[ x9] implies F(x9) in Y) & (not P[ x9]
implies G(x9) in Y) by A7,PARTFUN1:4;
consider h being Function of X,Y such that
A10: for x9 being object st x9 in X
holds (P[ x9] implies h.x9 = F(x9)) & (not
P[ x9] implies h.x9 = G(x9)) from Lambda1C(A9);
f tolerates h
proof
let x9 be object;
assume x9 in dom f /\ dom h;
then x9 in dom f by XBOOLE_0:def 4;
hence thesis by A10;
end;
then
A11: h in TotFuncs f by A3,PARTFUN1:def 5;
x in X by A4;
then x in dom h by A3,Def1;
then
A12: x in dom g /\ dom h by A4,XBOOLE_0:def 4;
h.x = y by A4,A5,A10;
hence contradiction by A8,A11,A12,A1,PARTFUN1:71,def 4;
end;
end;
end;
hence thesis by A1,Th88;
end;
theorem
for f,g being PartFunc of X,Y st (for y holds Y <> {y}) & TotFuncs f =
TotFuncs g holds f = g
by Th89;
:: from WAYBEL_1
registration
let A,B be non empty set;
cluster -> non empty for Function of A,B;
coherence by Def1,RELAT_1:38;
end;
begin :: Addenda
:: from RLVECT_2
scheme
LambdaSep1{D, R() -> non empty set, A() -> Element of D(),
B() -> Element of R(), F(object) -> Element of R()}:
ex f being Function of D(),R() st f.A() = B() &
for x being Element of D() st x <> A() holds f.x = F(x) proof
defpred P[set,set] means ($1 = A() implies $2 = B()) & ($1 <> A() implies $2
= F($1));
A1: for x being Element of D() ex y being Element of R() st P[x,y]
proof
let x be Element of D();
x = A() implies thesis;
hence thesis;
end;
consider f being Function of D(),R() such that
A2: for x being Element of D() holds P[x,f.x] from FuncExD(A1);
take f;
thus thesis by A2;
end;
scheme
LambdaSep2{D, R() -> non empty set, A1, A2() -> Element of D(),
B1, B2() -> Element of R(), F(object) -> Element of R()}:
ex f being Function of D(),R() st f.A1() = B1() & f.A2() = B2() &
for x being Element of D() st x <> A1() & x <> A2 () holds f.x = F(x)
provided
A1: A1() <> A2()
proof
defpred P[set,set] means ($1 = A1() implies $2 = B1()) & ($1 = A2() implies
$2 = B2()) & ($1 <> A1() & $1 <> A2() implies $2 = F($1));
A2: for x being Element of D() ex y being Element of R() st P[x,y]
proof
let x be Element of D();
A3: x = A2() implies thesis by A1;
x = A1() implies thesis by A1;
hence thesis by A3;
end;
consider f being Function of D(),R() such that
A4: for x being Element of D() holds P[x,f.x] from FuncExD(A2);
take f;
thus thesis by A4;
end;
:: from ALTCAT_1, PRALG_3
theorem
for A,B being set for f being Function st f in Funcs(A,B) holds dom f
= A & rng f c= B
proof
let A,B be set;
let f be Function;
assume f in Funcs(A,B);
then ex g being Function st f = g & dom g = A & rng g c= B by Def2;
hence thesis;
end;
:: from SUPINF_2
scheme
FunctRealEx{X()->non empty set,Y()->set,F(object)->object}:
ex f being Function of
X(),Y() st for x being Element of X() holds f.x = F(x)
provided
A1: for x being Element of X() holds F(x) in Y()
proof
defpred P[object,object] means $2 = F($1);
A2: for x being object st x in X()
ex y being object st y in Y() & P[x,y] by A1;
ex f being Function of X(),Y() st
for x being object st x in X() holds P[x,f.x] from FuncEx1(A2);
then consider f being Function of X(),Y() such that
A3: for x being object st x in X() holds f.x = F(x);
for x being Element of X() holds f.x = F (x) by A3;
hence thesis;
end;
:: from YELLOW_2
scheme
KappaMD{X, Y() -> non empty set, F(object) -> object}:
ex f being Function of X(),Y() st
for x being Element of X() holds f.x = F(x)
provided
A1: for x being Element of X() holds F(x) is Element of Y()
proof
A2: now
let x be Element of X();
F(x) is Element of Y() by A1;
hence F(x) in Y();
end;
consider f being Function of X(), Y() such that
A3: for x being Element of X() holds f.x = F(x) from FunctRealEx(A2);
take f;
thus thesis by A3;
end;
definition
let A,B,C be non empty set;
let f be Function of A, [:B,C:];
redefine func pr1 f -> Function of A,B means :: redefines pr1 (MCART_1, definition)
:Def5:
for x being Element of A holds it.x = (f.x)`1;
coherence
proof
A1: dom pr1 f = dom f by MCART_1:def 12;
A2: rng pr1 f c= B
proof
let x be object;
assume x in rng pr1 f;
then consider y being object such that
A3: y in dom pr1 f & x = (pr1 f).y by FUNCT_1:def 3;
x = (f.y)`1 & f.y in [:B,C:] by A1,A3,Th5,MCART_1:def 12;
hence thesis by MCART_1:10;
end;
dom pr1 f = A by A1,Def1;
hence thesis by A2,Th2;
end;
compatibility
proof
let IT be Function of A,B;
A4: dom pr1 f = dom f by MCART_1:def 12;
then
A5: dom pr1 f = A by Def1;
hence IT = pr1 f implies for x being Element of A holds IT.x = (f.x)`1 by
A4,MCART_1:def 12;
assume for x being Element of A holds IT.x = (f.x)`1;
then
A6: for x being object st x in dom f holds IT.x = (f.x)`1;
dom IT = dom f by A4,A5,Def1;
hence thesis by A6,MCART_1:def 12;
end;
redefine func pr2 f -> Function of A,C means :: redefines pr2 (MCART_1, definition)
:Def6:
for x being Element of A holds it .x = (f.x)`2;
coherence
proof
A7: dom pr2 f = dom f by MCART_1:def 13;
A8: rng pr2 f c= C
proof
let x be object;
assume x in rng pr2 f;
then consider y being object such that
A9: y in dom pr2 f & x = (pr2 f).y by FUNCT_1:def 3;
x = (f.y)`2 & f.y in [:B,C:] by A7,A9,Th5,MCART_1:def 13;
hence thesis by MCART_1:10;
end;
dom pr2 f = A by A7,Def1;
hence thesis by A8,Th2;
end;
compatibility
proof
let IT be Function of A,C;
A10: dom pr2 f = dom f by MCART_1:def 13;
then
A11: dom pr2 f = A by Def1;
hence IT = pr2 f implies for x being Element of A holds IT.x = (f.x)`2 by
A10,MCART_1:def 13;
assume for x being Element of A holds IT.x = (f.x)`2;
then
A12: for x being object st x in dom f holds IT.x = (f.x)`2;
dom IT = dom f by A10,A11,Def1;
hence thesis by A12,MCART_1:def 13;
end;
end;
definition
let A1 be set, B1 be non empty set, A2 be set, B2 be non empty set, f1 be
Function of A1,B1, f2 be Function of A2,B2;
redefine pred f1 = f2 means :: redefines = (FUNCT_1, redefinition) → = (RELAT_1, redefinition) → = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
A1 = A2 & for a being Element of A1 holds f1.a = f2.a;
compatibility
proof
A1: dom f1 = A1 by Def1;
hence
f1 = f2 implies A1 = A2 & for a being Element of A1 holds f1.a = f2.a
by Def1;
assume that
A2: A1 = A2 and
A3: for a being Element of A1 holds f1.a = f2.a;
A4: dom f2 = A2 by Def1;
for a being object st a in A1 holds f1.a = f2.a by A3;
hence thesis by A1,A4,A2;
end;
end;
definition
let A,B be set, f1,f2 be Function of A,B;
redefine pred f1 = f2 means :: redefines = (FUNCT_1, redefinition) → = (RELAT_1, redefinition) → = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
for a being Element of A holds f1.a = f2.a;
compatibility by Th62;
end;
:: missing, 2006.11.05, A.T.
theorem
for N being set, f being Function of N, bool N ex R being Relation of
N st for i being set st i in N holds Im(R,i) = f.i
proof
let N be set, f be Function of N, bool N;
deffunc F(set) = f.$1;
A1: for i being Element of N st i in [#]N holds F(i) c= [#]N
proof
let i be Element of N;
assume i in [#]N;
then f.i in bool N by Th5;
hence thesis;
end;
consider R being Relation of [#]N such that
A2: for i being Element of N st i in [#]N holds Im(R,i) = F(i) from
RELSET_1:sch 3(A1);
reconsider R as Relation of N;
take R;
thus thesis by A2;
end;
:: Moved from BORSUK_1 by AK on 27.12.2006
theorem Th93:
for A being Subset of X holds (id X)"A = A
proof
let A be Subset of X;
thus A = (id X)"((id X).:A) by Th61
.= (id X)"A by FUNCT_1:92;
end;
:: Moved from TMAP_1 by AK on 27.12.2006
reserve A,B for non empty set;
theorem
for f being Function of A,B, A0 being Subset of A, B0 being Subset of
B holds f.:A0 c= B0 iff A0 c= f"B0
proof
let f be Function of A,B, A0 be Subset of A, B0 be Subset of B;
thus f.:A0 c= B0 implies A0 c= f"B0
proof
assume f.:A0 c= B0;
then
A1: f"(f.:A0) c= f"B0 by RELAT_1:143;
A0 c= f"(f.:A0) by Th41;
hence thesis by A1;
end;
thus A0 c= f"B0 implies f.:A0 c= B0
proof
assume A0 c= f"B0;
then
A2: f.:A0 c= f.:f"B0 by RELAT_1:123;
f.:f"B0 c= B0 by FUNCT_1:75;
hence thesis by A2;
end;
end;
theorem
for f being Function of A,B, A0 being non empty Subset of A, f0 being
Function of A0,B st for c being Element of A st c in A0 holds f.c = f0.c holds
f|A0 = f0
proof
let f be Function of A,B, A0 be non empty Subset of A, f0 be Function of A0,
B such that
A1: for c being Element of A st c in A0 holds f.c = f0.c;
reconsider g = f|A0 as Function of A0,B by Th32;
for c being Element of A0 holds g.c = f0.c
proof
let c be Element of A0;
thus g.c = f.c by FUNCT_1:49
.= f0.c by A1;
end;
hence thesis by Th62;
end;
theorem
for f being Function, A0, C being set st C c= A0 holds f.:C = (f|A0).: C
proof
let f be Function, A0, C be set;
assume
A1: C c= A0;
thus (f|A0).:C = (f*(id A0)).:C by RELAT_1:65
.= f.:((id A0).:C) by RELAT_1:126
.= f.:C by A1,FUNCT_1:92;
end;
theorem
for f being Function, A0, D being set st f"D c= A0 holds f"D = (f|A0)" D
proof
let f be Function, A0, D be set;
assume
A1: f"D c= A0;
thus (f|A0)"D = (f*(id A0))"D by RELAT_1:65
.= (id A0)"(f"D) by RELAT_1:146
.= f"D by A1,Th93;
end;
scheme
MChoice{A()-> non empty set, B()-> non empty set, F(object) -> set}:
ex t being Function of A(),B() st for a being Element of A() holds t.a in F(a)
provided
A1: for a being Element of A() holds B() meets F(a)
proof
defpred P[object,object] means $2 in F($1);
A2: for e being object st e in A()
ex u being object st u in B() & P[e,u]
by A1,XBOOLE_0:3;
consider t being Function such that
A3: dom t = A() & rng t c= B() and
A4: for e being object st e in A() holds P[e,t.e] from FUNCT_1:sch 6(A2);
reconsider t as Function of A(),B() by A3,Def1,RELSET_1:4;
take t;
let a be Element of A();
thus thesis by A4;
end;
:: Moved from FINSEQ_4 by AK on 2007.10.09
theorem Th98:
for X, D be non empty set, p be Function of X,D, i be Element
of X holds p/.i = p.i
proof
let X, D be non empty set, p be Function of X,D, i be Element of X;
i in X;
then i in dom p by Def1;
hence thesis by PARTFUN1:def 6;
end;
registration
let X, D be non empty set, p be Function of X,D, i be Element of X;
identify p/.i with p.i;
correctness by Th98;
end;
:: from JCT_MISC, 2008.06.01, A.T.
theorem
for S,X being set, f being Function of S,X, A being Subset of X st X =
{} implies S = {} holds (f"A)` = f"(A`)
proof
let S,X be set, f be Function of S,X, A be Subset of X such that
A1: X = {} implies S = {};
A /\ A` = {} by XBOOLE_0:def 7,XBOOLE_1:79;
then f"A /\ f"(A`) = f"({}X) by FUNCT_1:68
.= {};
then
A2: f"A misses f"(A`);
f"A \/ f"(A`) = f"(A \/ A`) by RELAT_1:140
.= f"[#]X by SUBSET_1:10
.= [#]S by A1,Th39;
then (f"A)` /\ (f"(A`))` = ([#]S)` by XBOOLE_1:53
.= {}S by XBOOLE_1:37;
then (f"A)` misses (f"(A`))`;
hence thesis by A2,SUBSET_1:25;
end;
:: from CAT_1, 2008.07.01, A.T.
theorem
for X,Y,Z being set, D being non empty set, f being Function of X,D st
Y c= X & f.:Y c= Z holds f|Y is Function of Y,Z
proof
let X,Y,Z be set, D be non empty set, f be Function of X,D;
assume that
A1: Y c= X and
A2: f.:Y c= Z;
dom f = X by Def1;
then
A3: dom(f|Y) = Y by A1,RELAT_1:62;
A4: now
assume Z = {};
then rng(f|Y) = {} by A2,RELAT_1:115;
hence Y = {} by A3,RELAT_1:42;
end;
rng(f|Y) c= Z by A2,RELAT_1:115;
hence thesis by A3,A4,Def1,RELSET_1:4;
end;
:: from WEIERSTR, 2008.07.07, A.T.
definition
let T,S be non empty set;
let f be Function of T,S;
let G be Subset-Family of S;
func f"G -> Subset-Family of T means
:Def9:
for A being Subset of T holds A
in it iff ex B being Subset of S st B in G & A = f"B;
existence
proof
defpred P[Subset of T] means ex B being Subset of S st B in G & $1 = f"B;
ex R being Subset-Family of T st for A being Subset of T holds A in R
iff P[A] from SUBSET_1:sch 3;
hence thesis;
end;
uniqueness
proof
let R1,R2 be Subset-Family of T such that
A1: for A being Subset of T holds A in R1 iff ex B being Subset of S
st B in G & A = f"B and
A2: for A being Subset of T holds A in R2 iff ex B being Subset of S
st B in G & A = f"B;
for x being object holds (x in R1 iff x in R2)
proof
let x be object;
thus x in R1 implies x in R2
proof
assume
A3: x in R1;
then reconsider x as Subset of T;
ex B being Subset of S st B in G & x = f"B by A1,A3;
hence thesis by A2;
end;
assume
A4: x in R2;
then reconsider x as Subset of T;
ex B being Subset of S st B in G & x = f"B by A2,A4;
hence thesis by A1;
end;
hence thesis by TARSKI:2;
end;
end;
theorem
for T,S being non empty set, f being Function of T,S, A,B being
Subset-Family of S st A c= B holds f"A c= f"B
proof
let T,S be non empty set;
let f be Function of T,S;
let A,B be Subset-Family of S;
assume
A1: A c= B;
let x be object;
assume
A2: x in f"A;
then reconsider x as Subset of T;
ex C being Subset of S st C in B & x = f"C
proof
consider C being Subset of S such that
A3: C in A & x = f"C by A2,Def9;
take C;
thus thesis by A1,A3;
end;
hence thesis by Def9;
end;
definition
let T,S be set;
let f be Function of T,S;
let G be Subset-Family of T;
func f.:G -> Subset-Family of S means
:Def10:
for A being Subset of S holds
A in it iff ex B being Subset of T st B in G & A = f.:B;
existence
proof
thus ex R being Subset-Family of S st for A being Subset of S holds A in R
iff ex B being Subset of T st B in G & A = f.:B
proof
defpred P[Subset of S] means ex B being Subset of T st B in G & $1 = f.:
B;
ex R being Subset-Family of S st for A being Subset of S holds A in
R iff P[A] from SUBSET_1:sch 3;
hence thesis;
end;
end;
uniqueness
proof
let R1,R2 be Subset-Family of S such that
A1: for A being Subset of S holds A in R1 iff ex B being Subset of T
st B in G & A = f.:B and
A2: for A being Subset of S holds A in R2 iff ex B being Subset of T
st B in G & A = f.:B;
for x being object holds (x in R1 iff x in R2)
proof
let x be object;
thus x in R1 implies x in R2
proof
assume
A3: x in R1;
then reconsider x as Subset of S;
ex B being Subset of T st B in G & x = f.:B by A1,A3;
hence thesis by A2;
end;
assume
A4: x in R2;
then reconsider x as Subset of S;
ex B being Subset of T st B in G & x = f.:B by A2,A4;
hence thesis by A1;
end;
hence thesis by TARSKI:2;
end;
end;
theorem
for T,S being set, f being Function of T,S, A,B being Subset-Family of T
st A c= B holds f.:A c= f.:B
proof
let T,S be set;
let f be Function of T,S;
let A,B be Subset-Family of T;
assume
A1: A c= B;
let x be object;
assume
A2: x in f.:A;
then reconsider x as Subset of S;
ex C being Subset of T st C in B & x = f.:C
proof
consider C being Subset of T such that
A3: C in A & x = f.:C by A2,Def10;
take C;
thus thesis by A1,A3;
end;
hence thesis by Def10;
end;
theorem
for T,S being non empty set, f being Function of T,S, B being
Subset-Family of S, P being Subset of S st f.:(f"B) is Cover of P holds B is
Cover of P
proof
let T,S be non empty set;
let f be Function of T,S;
let B be Subset-Family of S;
let P be Subset of S;
assume f.:(f"B) is Cover of P;
then
A1: P c= union (f.:(f"B)) by SETFAM_1:def 11;
P c= union B
proof
let x be object;
assume x in P;
then consider Y being set such that
A2: x in Y and
A3: Y in f.:(f"(B)) by A1,TARSKI:def 4;
ex Z being set st x in Z & Z in B
proof
reconsider Y as Subset of S by A3;
consider Y1 being Subset of T such that
A4: Y1 in f"(B) and
A5: Y = f.:Y1 by A3,Def10;
consider Y2 being Subset of S such that
A6: Y2 in B & Y1 = f"(Y2) by A4,Def9;
A7: f.:(f"Y2) c= Y2 by FUNCT_1:75;
reconsider Y2 as set;
take Y2;
thus thesis by A2,A5,A6,A7;
end;
hence thesis by TARSKI:def 4;
end;
hence thesis by SETFAM_1:def 11;
end;
theorem
for T,S being non empty set, f being Function of T,S, B being
Subset-Family of T, P being Subset of T st B is Cover of P holds f"(f.:B) is
Cover of P
proof
let T,S be non empty set;
let f be Function of T,S;
let B be Subset-Family of T;
let P be Subset of T;
assume B is Cover of P;
then
A1: P c= union B by SETFAM_1:def 11;
P c= union(f"(f.:B))
proof
let x be object;
assume x in P;
then consider Y being set such that
A2: x in Y and
A3: Y in B by A1,TARSKI:def 4;
ex Z being set st x in Z & Z in f"(f.:B)
proof
reconsider Y as Subset of T by A3;
set Z = f"(f.:Y);
take Z;
dom f = T by Def1;
then
A4: Y c= f"(f.:Y) by FUNCT_1:76;
f.:Y in f.:B by A3,Def10;
hence thesis by A2,A4,Def9;
end;
hence thesis by TARSKI:def 4;
end;
hence thesis by SETFAM_1:def 11;
end;
theorem
for T,S being non empty set, f being Function of T,S, Q being
Subset-Family of S holds union(f.:(f"(Q))) c= union Q
proof
let T,S be non empty set;
let f be Function of T,S;
let Q be Subset-Family of S;
let x be object;
thus x in union(f.:(f"(Q))) implies x in union Q
proof
assume x in union(f.:(f"Q));
then consider A being set such that
A1: x in A and
A2: A in f.:(f"Q) by TARSKI:def 4;
reconsider A as Subset of S by A2;
consider A1 being Subset of T such that
A3: A1 in f"Q and
A4: A = f.:A1 by A2,Def10;
consider A2 being Subset of S such that
A5: A2 in Q & A1 = f"A2 by A3,Def9;
f.:(f"A2) c= A2 by FUNCT_1:75;
hence thesis by A1,A4,A5,TARSKI:def 4;
end;
end;
theorem
for T,S being non empty set, f being Function of T,S, P being
Subset-Family of T holds union P c= union(f"(f.:P))
proof
let T,S be non empty set;
let f be Function of T,S;
let P be Subset-Family of T;
let x be object;
assume x in union P;
then consider A being set such that
A1: x in A and
A2: A in P by TARSKI:def 4;
A3: A c= T by A2;
reconsider A as Subset of T by A2;
reconsider A1 = f.:A as Subset of S;
reconsider A2 = f"A1 as Subset of T;
A c= dom f by A3,Def1;
then
A4: A c= A2 by FUNCT_1:76;
A1 in f.:P by A2,Def10;
then A2 in f"(f.:P) by Def9;
hence thesis by A1,A4,TARSKI:def 4;
end;
:: Generalized RFUNCT_2:def 1,CFCONT_1:def 1,NFCONT_1:def 7,def 8
:: NCFCONT1:def 9,def 10,def 11,def 12,def 13,def 14
:: 2008.08.15, A.T.
definition
let X,Z be set, Y be non empty set;
let f be Function of X,Y;
let p be Z-valued Function;
assume
A1: rng f c= dom p;
func p/*f -> Function of X,Z equals
:Def11:
p*f;
coherence
proof
dom f = X by Def1;
then
dom(p*f) = X by A1,RELAT_1:27;
then
A2: p*f is total;
rng(p*f) c= Z;
hence thesis by A2,RELSET_1:4;
end;
end;
reserve Y for non empty set,
f for Function of X,Y,
p for PartFunc of Y,Z,
x for Element of X;
theorem Th107:
X <> {} & rng f c= dom p implies (p/*f).x = p.(f.x)
proof
assume that
A1: X <> {} and
A2: rng f c= dom p;
p/*f = p*f by A2,Def11;
hence thesis by A1,Th15;
end;
theorem Th108:
X <> {} & rng f c= dom p implies (p/*f).x = p/.(f.x)
proof
assume that
A1: X <> {} and
A2: rng f c= dom p;
A3: f.x in rng f by A1,Th4;
thus (p/*f).x = p.(f.x) by A1,A2,Th107
.= p/.(f.x) by A2,A3,PARTFUN1:def 6;
end;
reserve g for Function of X,X;
theorem
rng f c= dom p implies (p/*f)*g = p/*(f*g)
proof
A1: rng(f*g) c= rng f by RELAT_1:26;
assume
A2: rng f c= dom p;
hence (p/*f)*g = p*f*g by Def11
.= p*(f*g) by RELAT_1:36
.= p /* (f*g) by A2,A1,Def11,XBOOLE_1:1;
end;
:: from RAMSEY_1, 2008.09.12,A.T.
theorem
for X,Y being non empty set, f being Function of X,Y holds f is
constant iff ex y being Element of Y st rng f = {y}
proof
let X,Y be non empty set;
let f be Function of X,Y;
hereby
consider x be object such that
A1: x in dom f by XBOOLE_0:def 1;
set y = f.x;
reconsider y as Element of Y by A1,Th5;
assume
A2: f is constant;
take y;
for y9 being object holds y9 in rng f iff y9 = y
proof
let y9 be object;
hereby
assume y9 in rng f;
then ex x9 be object st x9 in dom f & y9 = f.x9 by FUNCT_1:def 3;
hence y9 = y by A2,A1;
end;
assume y9 = y;
hence thesis by A1,Th4;
end;
hence rng f = {y} by TARSKI:def 1;
end;
given y be Element of Y such that
A3: rng f = {y};
let x,x9 be object;
assume x in dom f;
then
A4: f.x in rng f by Th4;
assume x9 in dom f;
then
A5: f.x9 in rng f by Th4;
thus f.x = y by A3,A4,TARSKI:def 1
.= f.x9 by A3,A5,TARSKI:def 1;
end;
:: from ISOCAT_2, 2008.09.14, A.T.
theorem
for A,B being non empty set, x being Element of A, f being Function of
A,B holds f.x in rng f
proof
let A,B be non empty set, x be Element of A, f be Function of A,B;
dom f = A by Def1;
hence thesis by FUNCT_1:def 3;
end;
:: missing, 2008.09.14, A.T.
theorem Th112:
for A,B being set, f being Function of A,B st y in rng f ex x
being Element of A st y = f.x
proof
let A,B be set, f be Function of A,B;
assume y in rng f;
then consider x being object such that
A1: x in A and
A2: f.x = y by Th11;
reconsider x as Element of A by A1;
take x;
thus thesis by A2;
end;
:: from RFUNCT_2, 2008.09.14, A.T.
theorem
for A,B being non empty set, f being Function of A,B st for x being
Element of A holds f.x in Z holds rng f c= Z
proof
let A,B be non empty set, f be Function of A,B such that
A1: for x being Element of A holds f.x in Z;
let y be object;
assume y in rng f;
then ex x being Element of A st f.x=y by Th112;
hence thesis by A1;
end;
reserve X,Y for non empty set,
Z,S,T for set,
f for Function of X,Y,
g for PartFunc of Y,Z,
x for Element of X;
theorem
g is total implies (g/*f).x = g.(f.x)
proof
assume g is total;
then dom g = Y;
then rng f c= dom g;
hence thesis by Th107;
end;
theorem
g is total implies (g/*f).x = g/.(f.x)
proof
assume g is total;
then dom g = Y;
then rng f c= dom g;
hence thesis by Th108;
end;
theorem Th116:
rng f c= dom (g|S) implies (g|S)/*f = g/*f
proof
assume
A1: rng f c= dom (g|S);
let x be Element of X;
A2: dom (g|S) c= dom g by RELAT_1:60;
A3: f.x in rng f by Th4;
thus ((g|S)/*f).x = (g|S).(f.x) by A1,Th107
.= g.(f.x) by A1,A3,FUNCT_1:47
.= (g/*f).x by A1,A2,Th107,XBOOLE_1:1;
end;
theorem
rng f c= dom (g|S) & S c= T implies (g|S)/*f = (g|T)/*f
proof
assume
A1: rng f c= dom (g|S);
assume S c= T;
then g|S c= g|T by RELAT_1:75;
then
A2: dom (g|S) c= dom (g|T) by RELAT_1:11;
thus (g|S)/*f = g/*f by A1,Th116
.= (g|T)/*f by A1,A2,Th116,XBOOLE_1:1;
end;
:: missing, 2009.01.09, A.T.
theorem
for H being Function of D, [:A,B:], d being Element of D holds H.d = [
pr1 H.d,pr2 H.d]
proof
let H be Function of D, [:A,B:], d be Element of D;
thus H.d = [(H.d)`1,(H.d)`2] by MCART_1:21
.= [(H.d)`1,pr2 H.d] by Def6
.= [pr1 H.d,pr2 H.d] by Def5;
end;
:: from YELLOW20, 2009.01.21, A.T.
theorem
for A1,A2, B1,B2 being set for f being Function of A1,A2, g being
Function of B1,B2 st f tolerates g holds f /\ g is Function of A1 /\ B1, A2 /\
B2
proof
let A1,A2, B1,B2 be set;
let f be Function of A1,A2, g be Function of B1,B2 such that
A1: f tolerates g;
A2: dom (f/\g) c= dom f /\ dom g & dom f /\ dom g c= A1/\B1 by XBOOLE_1:27
,XTUPLE_0:24;
A3: now
set a = the Element of A1 /\ B1;
assume that
A4: dom f = A1 and
A1 <> {} and
A5: dom g = B1 and
B1 <> {};
hereby
assume
A6: A1 /\ B1 <> {};
then a in A1 by XBOOLE_0:def 4;
then
A7: f.a in rng f by A4,FUNCT_1:def 3;
f.a = g.a & a in B1 by A1,A4,A5,A6,XBOOLE_0:def 4;
then f.a in rng g by A5,FUNCT_1:def 3;
hence A2 /\ B2 <> {} by A7,XBOOLE_0:def 4;
end;
thus dom (f /\ g) = A1 /\ B1
proof
thus dom (f /\ g) c= A1 /\ B1 by A2;
let a be object;
assume
A8: a in A1 /\ B1;
then a in A1 by XBOOLE_0:def 4;
then
A9: [a,f.a] in f by A4,FUNCT_1:def 2;
f.a = g.a & a in B1 by A1,A4,A5,A8,XBOOLE_0:def 4;
then [a,f.a] in g by A5,FUNCT_1:def 2;
then [a,f.a] in f /\ g by A9,XBOOLE_0:def 4;
hence thesis by XTUPLE_0:def 12;
end;
end;
rng (f/\g) c= rng f /\ rng g & rng f /\ rng g c= A2/\B2 by RELAT_1:13
,XBOOLE_1:27;
then
A10: rng (f/\g) c= A2/\B2;
A11: A2 = {} or A2 <> {};
A12: B2 = {} or B2 <> {};
A13: now
per cases;
case A2 /\ B2 <> {};
hence dom (f /\ g) = A1 /\ B1 by A12,A3,Def1,A11;
end;
case A1 /\ B1 = {};
hence dom (f /\ g) = A1 /\ B1 by A2;
end;
case A2 /\ B2 = {} & A1 /\ B1 <> {};
hence f /\ g = {} by A12,A3,Def1,A11;
end;
end;
thus thesis by A10,A13,Def1,RELSET_1:4;
end;
:: from FRAENKEL, 2009.05.06, A.K.
registration
let A, B be set;
cluster Funcs(A,B) -> functional;
coherence
proof
let x be object;
assume x in Funcs(A,B);
then ex f being Function st x = f & dom f = A & rng f c= B by Def2;
hence thesis;
end;
end;
definition
let A, B be set;
mode FUNCTION_DOMAIN of A,B -> non empty set means
:Def12:
for x being Element of it holds x is Function of A,B;
existence
proof
take IT = {the Function of A,B};
let g be Element of IT;
thus thesis by TARSKI:def 1;
end;
end;
registration
let A, B be set;
cluster -> functional for FUNCTION_DOMAIN of A,B;
coherence
by Def12;
end;
theorem
for f being Function of P,Q holds { f } is FUNCTION_DOMAIN of P,Q
proof
let f be Function of P,Q;
for g be Element of { f } holds g is Function of P,Q by TARSKI:def 1;
hence thesis by Def12;
end;
theorem Th121:
Funcs(P,B) is FUNCTION_DOMAIN of P,B
proof
for f be Element of Funcs(P,B) holds f is Function of P,B by Th65;
hence thesis by Def12;
end;
definition
let A be set, B be non empty set;
redefine func Funcs(A,B) -> FUNCTION_DOMAIN of A,B; :: redefines Funcs (FUNCT_2, definition)
coherence by Th121;
let F be FUNCTION_DOMAIN of A,B;
redefine mode Element of F -> Function of A,B; :: redefines Element (SUBSET_1, definition)
coherence by Def12;
end;
registration
let I be set;
cluster id I -> total for I-defined Function;
coherence;
end;
:: from CAT_3, 2009.09.14
definition
let X,A;
let F be Function of X,A;
let x be set;
assume
A1: x in X;
redefine func F/.x equals :: redefines /. (PARTFUN1, definition)
F.x;
compatibility
proof
let a be Element of A;
x in dom F by A1,Def1;
hence thesis by PARTFUN1:def 6;
end;
end;
theorem
for X being set, Y being non empty set
for f being Function of X, Y, g being X-valued Function
holds dom(f*g) = dom g
proof
let X be set, Y be non empty set;
let f be Function of X, Y;
let g be X-valued Function;
dom f = X by Def1;
then rng g c= dom f;
hence thesis by RELAT_1:27;
end;
theorem
for X being non empty set, f being Function of X,X st for x being
Element of X holds f.x = x holds f = id X;
:: Moved from GROUP_9, AK
definition
let O,E be set;
mode Action of O,E is Function of O, Funcs(E,E);
end;
theorem
for x being set, A being set
for f,g being Function of {x}, A st f.x = g.x
holds f = g
proof
let x be set, A be set;
let f,g be Function of {x}, A such that
A1: f.x = g.x;
now
let y be object;
assume y in {x};
then y = x by TARSKI:def 1;
hence f.y = g.y by A1;
end;
hence thesis;
end;
theorem Th125:
for A being set holds id A in Funcs(A,A)
proof
let A be set;
dom id A = A & rng id A = A;
hence thesis by Def2;
end;
theorem
Funcs({},{}) = { id {} }
proof
hereby
let f be object;
assume f in Funcs({},{});
then reconsider f9 = f as Function of {},{} by Th65;
f9 = id {};
hence f in { id {} } by TARSKI:def 1;
end;
thus thesis by Th125,ZFMISC_1:31;
end;
theorem Th127:
for A,B,C being set, f,g being Function st f in Funcs(A,B) & g in
Funcs(B,C) holds g*f in Funcs(A,C)
proof
let A,B,C be set, f,g be Function;
assume that
A1: f in Funcs(A,B) and
A2: g in Funcs(B,C);
A3: ex g9 being Function st g9 = g & dom g9 = B & rng g9 c= C by A2,Def2;
rng(g*f) c= rng g by RELAT_1:26;
then
A4: rng(g*f) c= C by A3;
ex f9 being Function st f9 = f & dom f9 = A & rng f9 c= B by A1,Def2;
then dom(g*f) = A by A3,RELAT_1:27;
hence thesis by A4,Def2;
end;
theorem
for A,B,C being set st Funcs(A,B) <> {} & Funcs(B,C) <> {} holds
Funcs(A,C) <> {}
proof
let A,B,C be set such that
A1: Funcs(A,B) <> {} and
A2: Funcs(B,C) <> {};
consider g being object such that
A3: g in Funcs(B,C) by A2,XBOOLE_0:def 1;
ex f being object st f in Funcs(A,B) by A1,XBOOLE_0:def 1;
hence thesis by A3,Th127;
end;
theorem
for A being set holds {} is Function of A,{} by Def1,RELSET_1:12;
scheme
Lambda1{X, Y() -> set, F(object)->object}:
ex f being Function of X(),Y() st
for x being set st x in X() holds f.x = F(x)
provided
A1: for x being set st x in X() holds F(x) in Y();
defpred P[object,object] means $2 = F($1);
A2: for x being object st x in X()
ex y being object st y in Y() & P[x,y] by A1;
consider f being Function of X(),Y() such that
A3: for x being object st x in X() holds P[x,f.x] from FuncEx1(A2);
take f;
thus thesis by A3;
end;