:: Binary Operations Applied to Functions
:: by Andrzej Trybulec
::
:: Received September 4, 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 FUNCT_1, FUNCT_3, PARTFUN1, RELAT_1, ZFMISC_1, XBOOLE_0, TARSKI,
SUBSET_1, BINOP_1, MCART_1, FUNCOP_1, WELLORD1, MSUALG_4, FUNCT_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, MCART_1, RELAT_1,
FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1, WELLORD1;
constructors PARTFUN1, BINOP_1, FUNCT_3, RELSET_1, WELLORD1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, RELSET_1;
requirements SUBSET, BOOLE;
definitions TARSKI, RELAT_1, FUNCT_1, WELLORD1, PARTFUN1;
equalities BINOP_1;
expansions TARSKI, RELAT_1, BINOP_1, FUNCT_1;
theorems ZFMISC_1, RELAT_1, RELSET_1, FUNCT_1, FUNCT_2, FUNCT_3, TARSKI,
MCART_1, XBOOLE_0, XBOOLE_1, GRFUNC_1, XTUPLE_0;
schemes FUNCT_1;
begin
reserve f,g,h for Function,
A for set;
theorem Th1:
delta A = <:id A, id A:>
proof
thus delta A = id [:A,A:]*delta A by FUNCT_2:17
.= [:id A, id A:]*delta A by FUNCT_3:69
.= <:id A, id A:> by FUNCT_3:78;
end;
reserve F for Function,
B,x,y,y1,y2,z for set;
definition
let f;
func f~ -> Function means
:Def1:
dom it = dom f & for x being object st x in dom f holds
(for y,z being object st f.x = [y,z] holds it.x = [z,y]) &
(f.x = it.x or ex y,z being object st f.x =[y,z]);
existence
proof
defpred P[object,object] means
(for y,z being object st f.$1 = [y,z] holds $2 = [z,y]) & (f.
$1 = $2 or ex y,z being object st f.$1 = [y,z]);
A1: now
let x be object such that
x in dom f;
now
per cases;
case
A2: ex y,z being object st f.x = [y,z];
then consider y,z being object such that
A3: f.x = [y,z];
take y1 = [z,y];
thus for y,z being object st f.x = [y,z] holds y1 = [z,y]
proof
let y9,z9 be object;
assume
A4: f.x = [y9,z9];
then z = z9 by A3,XTUPLE_0:1;
hence thesis by A3,A4,XTUPLE_0:1;
end;
thus f.x = y1 or ex y,z being object st f.x = [y,z] by A2;
end;
case
A5: not ex y,z being object st f.x = [y,z];
reconsider y1 = f.x as set;
take y1;
thus (for y,z being object st f.x = [y,z] holds y1 = [z,y]) &
(f.x = y1 or ex y,z being object st f.x = [y,z]) by A5;
end;
end;
hence ex y being object st P[x,y];
end;
A6: now
let x,y1,y2 be object such that
x in dom f;
assume that
A7: P[x,y1] and
A8: P[x,y2];
now
per cases;
suppose
ex y,z being object st f.x = [y,z];
then consider y,z being object such that
A9: f.x = [y,z];
y1 = [z,y] by A7,A9;
hence y1 = y2 by A8,A9;
end;
suppose
not ex y,z being object st f.x = [y,z];
hence y1 = y2 by A7,A8;
end;
end;
hence y1 = y2;
end;
thus ex g st dom g = dom f &
for x being object st x in dom f holds P[x,g.x] from
FUNCT_1:sch 2(A6,A1);
end;
uniqueness
proof
defpred P[Function] means
for x being object st x in dom f holds
(for y,z being object st f.x = [y,z
] holds $1.x = [z,y]) & (f.x = $1.x or ex y,z being object st f.x =[y,z]);
let g1,g2 be Function such that
A10: dom g1 = dom f and
A11: P[g1] and
A12: dom g2 = dom f and
A13: P[g2];
now
let x be object;
assume
A14: x in dom f;
now
per cases;
suppose
ex y,z being object st f.x = [y,z];
then consider y,z being object such that
A15: f.x = [y,z];
g1.x = [z,y] by A11,A14,A15;
hence g1.x = g2.x by A13,A14,A15;
end;
suppose
A16: not ex y,z being object st f.x = [y,z];
then g1.x = f.x by A11,A14;
hence g1.x = g2.x by A13,A14,A16;
end;
end;
hence g1.x = g2.x;
end;
hence thesis by A10,A12;
end;
involutiveness
proof
let g,f be Function;
assume that
A17: dom g = dom f and
A18: for x being object st x in dom f
holds (for y,z being object st f.x = [y,z] holds g.x = [z,
y]) & (f.x = g.x or ex y,z being object st f.x =[y,z]);
thus dom f = dom g by A17;
let x be object;
assume
A19: x in dom g;
thus for y,z being object st g.x = [y,z] holds f.x = [z,y]
proof
let y,z being object such that
A20: g.x = [y,z];
per cases;
suppose
ex z,y being object st f.x =[z,y];
then consider y1,y2 being object such that
A21: f.x = [y1,y2];
A22: g.x = [y2,y1] by A17,A18,A19,A21;
then y = y2 by A20,XTUPLE_0:1;
hence thesis by A20,A21,A22,XTUPLE_0:1;
end;
suppose
not ex z,y being object st f.x =[z,y];
then f.x = g.x by A17,A18,A19;
hence thesis by A17,A18,A19,A20;
end;
end;
assume g.x <> f.x;
then consider y,z being object such that
A23: f.x = [y,z] by A17,A18,A19;
take z,y;
thus thesis by A17,A18,A19,A23;
end;
end;
theorem Th2:
<:f,g:> = <:g,f:>~
proof
A1: dom <:f,g:> = dom g /\ dom f by FUNCT_3:def 7
.= dom <:g,f:> by FUNCT_3:def 7;
A2: now
let x be object;
assume
A3: x in dom <:f,g:>;
then
A4: <:g,f:>.x = [g.x, f.x] by A1,FUNCT_3:def 7;
thus <:f,g:>.x = [f.x, g.x] by A3,FUNCT_3:def 7
.= <:g,f:>~.x by A1,A3,A4,Def1;
end;
dom <:f,g:> = dom (<:g,f:>~) by A1,Def1;
hence thesis by A2;
end;
theorem Th3:
(f|A)~ = f~|A
proof
A1: dom (f|A) = dom f /\ A by RELAT_1:61
.= dom (f~) /\ A by Def1
.= dom (f~|A) by RELAT_1:61;
A2: now
let x be object such that
A3: x in dom(f~|A);
A4: dom (f|A) c= dom f by RELAT_1:60;
now
per cases;
suppose
ex y,z being object st (f|A).x = [y,z];
then consider y,z being object such that
A5: (f|A).x = [y,z];
A6: f.x = [y,z] by A1,A3,A5,FUNCT_1:47;
thus (f|A)~.x = [z,y] by A1,A3,A5,Def1
.= f~.x by A1,A3,A4,A6,Def1
.= (f~|A).x by A3,FUNCT_1:47;
end;
suppose
A7: not ex y,z being object st (f|A).x = [y,z];
A8: (f|A).x = f.x by A1,A3,FUNCT_1:47;
(f|A)~.x = (f|A).x by A1,A3,A7,Def1;
hence (f|A)~.x = f~.x by A1,A3,A4,A7,A8,Def1
.= (f~|A).x by A3,FUNCT_1:47;
end;
end;
hence (f|A)~.x = (f~|A).x;
end;
dom ((f|A)~) = dom (f|A) by Def1;
hence thesis by A1,A2;
end;
theorem
(delta A)~ = delta A
proof
thus (delta A)~ = <:id A, id A:>~ by Th1
.= <:id A, id A:> by Th2
.= delta A by Th1;
end;
theorem Th5:
<:f,g:>|A = <:f|A,g:>
proof
A1: dom (<:f,g:>|A) = dom <:f,g:> /\ A by RELAT_1:61
.= dom f /\ dom g /\ A by FUNCT_3:def 7
.= dom f /\ A /\ dom g by XBOOLE_1:16
.= dom (f|A) /\ dom g by RELAT_1:61;
now
A2: dom (<:f,g:>|A) c= dom <:f,g:> by RELAT_1:60;
let x be object such that
A3: x in dom (<:f,g:>|A);
A4: x in dom (f|A) by A1,A3,XBOOLE_0:def 4;
thus (<:f,g:>|A).x = <:f,g:>.x by A3,FUNCT_1:47
.= [f.x, g.x] by A3,A2,FUNCT_3:def 7
.= [(f|A).x, g.x] by A4,FUNCT_1:47;
end;
hence thesis by A1,FUNCT_3:def 7;
end;
theorem Th6:
<:f,g:>|A = <:f,g|A:>
proof
thus <:f,g:>|A = <:g,f:>~|A by Th2
.= (<:g,f:>|A)~ by Th3
.= <:g|A,f:>~ by Th5
.= <:f,g|A:> by Th2;
end;
definition
let A be set, z be object;
func A --> z -> set equals
[:A, {z}:];
coherence;
end;
registration
let A be set, z be object;
cluster A --> z -> Function-like Relation-like;
coherence
proof
thus A --> z is Function-like
proof
let x,y1,y2 be object;
assume that
A1: [x,y1] in A --> z and
A2: [x,y2] in A --> z;
y1 in {z} by A1,ZFMISC_1:87;
then
A3: y1 = z by TARSKI:def 1;
y2 in {z} by A2,ZFMISC_1:87;
hence thesis by A3,TARSKI:def 1;
end;
thus for x being object st x in A --> z
ex y1,y2 being object st [y1,y2] =x
by RELAT_1:def 1;
end;
end;
reserve x,z for object;
theorem Th7:
x in A implies (A --> z).x = z
proof
assume
A1: x in A;
z in {z} by TARSKI:def 1;
then [x,z] in (A --> z) by A1,ZFMISC_1:87;
hence thesis by FUNCT_1:1;
end;
registration
let A be non empty set, x be object, a be Element of A;
reduce (A --> x).a to x;
reducibility by Th7;
end;
theorem
A <> {} implies rng (A --> x) = {x} by RELAT_1:160;
theorem Th9:
rng f = {x} implies f = (dom f) --> x
proof
assume
A1: rng f = {x};
then dom f <> {} by RELAT_1:42;
then dom((dom f) --> x) = dom f & rng((dom f) -->x) = {x} by RELAT_1:160;
hence thesis by A1,FUNCT_1:7;
end;
registration
let x be object;
cluster {} --> x -> empty;
coherence by ZFMISC_1:90;
end;
registration
let x be object;
let A be empty set;
cluster A --> x -> empty;
coherence;
end;
registration
let x be object;
let A be non empty set;
cluster A --> x -> non empty;
coherence;
end;
theorem
dom ({} --> x) = {} & rng ({} --> x) = {};
theorem Th11:
(for z st z in dom f holds f.z = x) implies f = dom f --> x
proof
assume
A1: for z st z in dom f holds f.z = x;
now
per cases;
suppose
A2: dom f = {};
thus thesis by A2;
end;
suppose
A3: dom f <> {};
set z = the Element of dom f;
now
let y be object;
thus y in {x} implies ex y1 being object st y1 in dom f & y = f.y1
proof
assume y in {x};
then y = x by TARSKI:def 1;
then f.z = y by A1,A3;
hence thesis by A3;
end;
assume ex y1 being object st y1 in dom f & y = f.y1;
then y = x by A1;
hence y in {x} by TARSKI:def 1;
end;
then rng f = {x} by FUNCT_1:def 3;
hence thesis by Th9;
end;
end;
hence thesis;
end;
theorem Th12:
(A --> x)|B = A /\ B --> x
proof
A1: A = {} or A <> {};
A2: A /\ B = {} or A /\ B <> {};
A3: dom ((A --> x)|B) = dom (A --> x) /\ B by RELAT_1:61
.= A /\ B by A1,RELAT_1:160
.= dom (A /\ B --> x) by A2,RELAT_1:160;
now
let z be object such that
A4: z in dom (A /\ B --> x);
A /\ B = {} or A /\ B <> {};
then
A5: z in A /\ B by A4,RELAT_1:160;
then
A6: z in A by XBOOLE_0:def 4;
thus ((A --> x)|B).z = (A --> x).z by A3,A4,FUNCT_1:47
.= x by A6,Th7
.= (A /\ B --> x).z by A5,Th7;
end;
hence thesis by A3;
end;
theorem Th13:
dom (A --> x) = A & rng (A --> x) c= {x}
proof
now
per cases;
suppose
A1: A = {};
thus thesis by A1;
end;
suppose
A <> {};
hence thesis by RELAT_1:160;
end;
end;
hence thesis;
end;
registration
let X be set, a be object;
reduce dom (X --> a) to X;
reducibility by Th13;
end;
registration let D be set;
cluster D --> {} -> empty-yielding;
coherence by Th13;
end;
theorem Th14:
x in B implies (A --> x)"B = A
proof
assume
A1: x in B;
now
per cases;
suppose A = {};
hence thesis;
end;
suppose
A <> {};
then
A3: rng (A --> x) = {x} by RELAT_1:160;
{x} c= B by A1,ZFMISC_1:31;
then {x} /\ B = {x} by XBOOLE_1:28;
hence (A --> x)"B = (A --> x)"{x} by A3,RELAT_1:133
.= dom (A -->x) by A3,RELAT_1:134
.= A;
end;
end;
hence thesis;
end;
theorem
(A --> x)"{x} = A
proof
x in {x} by TARSKI:def 1;
hence thesis by Th14;
end;
theorem
not x in B implies (A --> x)"B = {}
proof
assume
A1: not x in B;
rng (A --> x) c= {x} by Th13;
then rng (A --> x) misses B by A1,XBOOLE_1:63,ZFMISC_1:50;
hence thesis by RELAT_1:138;
end;
theorem
x in dom h implies h*(A --> x) = A --> h.x
proof
assume
A1: x in dom h;
A2: now
let z be object;
assume
A3: z in dom (h*(A --> x));
then z in dom (A --> x) by FUNCT_1:11;
then
A4: z in A;
thus (h*(A --> x)).z = h.((A --> x).z) by A3,FUNCT_1:12
.= h.x by A4,Th7
.= (A --> h.x).z by A4,Th7;
end;
dom (h*(A --> x)) = (A --> x)"dom h by RELAT_1:147
.= A by A1,Th14
.= dom (A --> h.x);
hence thesis by A2;
end;
theorem
A <> {} & x in dom h implies dom(h*(A --> x)) <> {}
proof
assume that
A1: A <> {} and
A2: x in dom h;
set y = the Element of A;
A3: y in dom (A -->x) by A1;
(A --> x).y = x by A1,Th7;
hence thesis by A2,A3,FUNCT_1:11;
end;
theorem
(A --> x)*h = h"A --> x
proof
A1: dom ((A --> x)*h) = h"dom(A --> x) by RELAT_1:147
.= h"A;
now
let z be object;
assume
A3: z in dom ((A --> x)*h);
then h.z in dom (A --> x) by FUNCT_1:11;
then
A4: h.z in A;
thus ((A --> x)*h).z = (A --> x).(h.z) by A3,FUNCT_1:12
.= x by A4,Th7
.= (h"A --> x).z by A1,A3,Th7;
end;
hence thesis by A1;
end;
theorem
(A --> [x,y])~ = A --> [y,x]
proof
A1: dom ((A --> [x,y])~) = dom (A --> [x,y]) by Def1;
then
A2: dom ((A --> [x,y])~) = A;
now
let z be object;
assume
A4: z in dom ((A --> [x,y])~);
then (A --> [x,y]).z = [x,y] by A2,Th7;
hence ((A --> [x,y])~).z = [y,x] by A1,A4,Def1
.= (A --> [y,x]).z by A2,A4,Th7;
end;
hence thesis by A2;
end;
definition
let F,f,g;
func F.:(f,g) -> set equals
F * <:f,g:>;
correctness;
end;
registration
let F,f,g;
cluster F.:(f,g) -> Function-like Relation-like;
coherence;
end;
Lm1: x in dom (F*<:f,g:>) implies (F*<:f,g:>).x = F.(f.x,g.x)
proof
assume
A1: x in dom (F*<:f,g:>);
then
A2: x in dom <:f,g:> by FUNCT_1:11;
thus (F*<:f,g:>).x = F.(<:f,g:>.x) by A1,FUNCT_1:12
.= F.(f.x,g.x) by A2,FUNCT_3:def 7;
end;
theorem
for h st dom h = dom(F.:(f,g)) & for z being set st z in dom (F.:(f,g)
) holds h.z = F.(f.z,g.z) holds h = F.:(f,g)
proof
let h;
assume that
A1: dom h = dom(F.:(f,g)) and
A2: for z being set st z in dom (F.:(f,g)) holds h.z = F.(f.z,g.z);
now
let z be object;
assume
A3: z in dom (F.:(f,g));
hence h.z = F.(f.z,g.z) by A2
.= (F.:(f,g)).z by A3,Lm1;
end;
hence thesis by A1;
end;
theorem
x in dom (F.:(f,g)) implies (F.:(f,g)).x = F.(f.x,g.x) by Lm1;
theorem Th23:
f|A = g|A implies (F.:(f,h))|A = (F.:(g,h))|A
proof
assume
A1: f|A = g|A;
thus (F.:(f,h))|A = F*<:f,h:>|A by RELAT_1:83
.= F*<:f|A,h:> by Th5
.= F*<:g,h:>|A by A1,Th5
.= (F.:(g,h))|A by RELAT_1:83;
end;
theorem Th24:
f|A = g|A implies (F.:(h,f))|A = (F.:(h,g))|A
proof
assume
A1: f|A = g|A;
thus (F.:(h,f))|A = F*<:h,f:>|A by RELAT_1:83
.= F*<:h,f|A:> by Th6
.= F*<:h,g:>|A by A1,Th6
.= (F.:(h,g))|A by RELAT_1:83;
end;
theorem Th25:
F.:(f,g)*h = F.:(f*h, g*h)
proof
thus F.:(f,g)*h = F*(<:f,g:>*h) by RELAT_1:36
.= F.:(f*h, g*h) by FUNCT_3:55;
end;
definition
let F,f,x;
func F[:](f,x) -> set equals
F * <:f, dom f --> x:>;
correctness;
end;
registration
let F,f,x;
cluster F[:](f,x) -> Function-like Relation-like;
coherence;
end;
theorem
F[:](f,x) = F.:(f, dom f --> x);
theorem Th27:
x in dom (F[:](f,z)) implies (F[:](f,z)).x = F.(f.x,z)
proof
A1: dom <:f, dom f --> z:> = dom f /\ dom (dom f --> z) by FUNCT_3:def 7;
assume
A2: x in dom (F[:](f,z));
then x in dom <:f, dom f --> z:> by FUNCT_1:11;
then
A3: x in dom f by A1;
thus (F[:](f,z)).x = F.(f.x,(dom f --> z).x) by A2,Lm1
.= F.(f.x,z) by A3,Th7;
end;
theorem
f|A = g|A implies (F[:](f,x))|A = (F[:](g,x))|A
proof
assume
A1: f|A = g|A;
dom f /\ A = dom (f|A) by RELAT_1:61
.= dom g /\ A by A1,RELAT_1:61;
then
A2: (dom f --> x)|A = dom g /\ A --> x by Th12
.= (dom g -->x)|A by Th12;
thus (F[:](f,x))|A = (F.:(f, dom f --> x))|A
.= (F.:(g, dom f --> x))|A by A1,Th23
.= (F.:(g, dom g --> x))|A by A2,Th24
.= (F[:](g,x))|A;
end;
theorem Th29:
F[:](f,x)*h = F[:](f*h,x)
proof
dom (dom f -->x) = dom f; then
A2: dom ((dom f --> x)*h) = dom (f*h) by RELAT_1:163;
A3: now
let z;
assume
A4: z in dom ((dom f --> x)*h);
then
A5: h.z in dom(dom f -->x) by FUNCT_1:11;
thus ((dom f --> x)*h).z = (dom f --> x).(h.z) by A4,FUNCT_1:12
.= x by A5,Th7;
end;
thus F[:](f,x)*h = F.:(f, dom f --> x)*h
.= F.:(f*h, (dom f --> x)*h) by Th25
.= F[:](f*h,x) by A2,A3,Th11;
end;
theorem
F[:](f,x)*id A = F[:](f|A,x)
proof
thus F[:](f,x)*id A = F[:](f*id A, x) by Th29
.= F[:](f|A, x) by RELAT_1:65;
end;
definition
let F,x,g;
func F[;](x,g) -> set equals
F * <:dom g --> x, g:>;
correctness;
end;
registration
let F,x,g;
cluster F[;](x,g) -> Function-like Relation-like;
coherence;
end;
theorem
F[;](x,g) = F.:(dom g --> x, g);
theorem Th32:
x in dom (F[;](z,f)) implies (F[;](z,f)).x = F.(z,f.x)
proof
A1: dom <:dom f --> z, f:> = dom (dom f --> z) /\ dom f by FUNCT_3:def 7;
assume
A2: x in dom (F[;](z,f));
then x in dom <:dom f --> z, f:> by FUNCT_1:11;
then
A3: x in dom f by A1;
thus (F[;](z,f)).x = F.((dom f --> z).x, f.x) by A2,Lm1
.= F.(z, f.x) by A3,Th7;
end;
theorem
f|A = g|A implies (F[;](x,f))|A = (F[;](x,g))|A
proof
assume
A1: f|A = g|A;
dom f /\ A = dom (f|A) by RELAT_1:61
.= dom g /\ A by A1,RELAT_1:61;
then
A2: (dom f --> x)|A = dom g /\ A --> x by Th12
.= (dom g -->x)|A by Th12;
thus (F[;](x,f))|A = (F.:(dom f --> x, f))|A
.= (F.:(dom f --> x, g))|A by A1,Th24
.= (F.:(dom g --> x, g))|A by A2,Th23
.= (F[;](x,g))|A;
end;
theorem Th34:
F[;](x,f)*h = F[;](x,f*h)
proof
dom (dom f -->x) = dom f; then
A2: dom ((dom f --> x)*h) = dom (f*h) by RELAT_1:163;
A3: now
let z;
assume
A4: z in dom ((dom f --> x)*h);
then
A5: h.z in dom(dom f -->x) by FUNCT_1:11;
thus ((dom f --> x)*h).z = (dom f --> x).(h.z) by A4,FUNCT_1:12
.= x by A5,Th7;
end;
thus F[;](x,f)*h = F.:(dom f --> x, f)*h
.= F.:((dom f --> x)*h, f*h) by Th25
.= F[;](x,f*h) by A2,A3,Th11;
end;
theorem
F[;](x,f)*id A = F[;](x,f|A)
proof
thus F[;](x,f)*id A = F[;](x,f*id A) by Th34
.= F[;](x,f|A) by RELAT_1:65;
end;
reserve X for non empty set,
Y for set,
F for BinOp of X,
f,g,h for Function of Y,X,
x,x1,x2 for Element of X;
theorem Th36:
F.:(f,g) is Function of Y,X
proof
F*<:f,g:> is Function of Y,X;
hence thesis;
end;
definition
let X be non empty set, Z be set;
let F be BinOp of X, f,g be Function of Z,X;
redefine func F.:(f,g) -> Function of Z,X; :: redefines .: (FUNCOP_1, definition)
coherence by Th36;
end;
reserve Y for non empty set,
F for BinOp of X,
f,g,h for Function of Y,X,
x,x1,x2 for Element of X;
theorem Th37:
for z being Element of Y holds (F.:(f,g)).z = F.(f.z,g.z)
proof
let z be Element of Y;
dom (F.:(f,g)) = Y by FUNCT_2:def 1;
hence thesis by Lm1;
end;
theorem Th38:
for h being Function of Y,X holds (for z being Element of Y
holds h.z = F.(f.z,g.z)) implies h = F.:(f,g)
proof
let h be Function of Y,X;
assume
A1: for z being Element of Y holds h.z = F.(f.z,g.z);
now
let z be Element of Y;
thus h.z = F.(f.z,g.z) by A1
.= (F.:(f,g)).z by Th37;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for g being Function of X,X holds F.:(id X, g)*f = F.:(f,g*f)
proof
let g be Function of X,X;
thus F.:(id X, g)*f = F.:(id X*f, g*f) by Th25
.= F.:(f,g*f) by FUNCT_2:17;
end;
theorem
for g being Function of X,X holds F.:(g, id X)*f = F.:(g*f,f)
proof
let g be Function of X,X;
thus F.:(g, id X)*f = F.:(g*f, id X*f) by Th25
.= F.:(g*f, f) by FUNCT_2:17;
end;
theorem
F.:(id X, id X)*f = F.:(f,f)
proof
thus F.:(id X, id X)*f = F.:(id X*f, id X*f) by Th25
.= F.:(id X*f, f) by FUNCT_2:17
.= F.:(f,f) by FUNCT_2:17;
end;
theorem
for g being Function of X,X holds F.:(id X, g).x = F.(x,g.x)
proof
let g be Function of X,X;
thus F.:(id X, g).x = F.(id X.x, g.x) by Th37
.= F.(x,g.x);
end;
theorem
for g being Function of X,X holds F.:(g, id X).x = F.(g.x,x)
proof
let g be Function of X,X;
thus F.:(g, id X).x = F.(g.x, id X.x) by Th37
.= F.(g.x, x);
end;
theorem
F.:(id X, id X).x = F.(x,x)
proof
thus F.:(id X, id X).x = F.(id X.x, id X.x) by Th37
.= F.(id X.x, x)
.= F.(x,x);
end;
theorem Th45:
x in B implies A --> x is Function of A,B
proof
A1: rng (A --> x) c= {x} by Th13;
A2: dom (A --> x) = A;
assume
A3: x in B;
then {x} c= B by ZFMISC_1:31;
then rng (A --> x) c= B by A1;
hence thesis by A3,A2,FUNCT_2:def 1,RELSET_1:4;
end;
definition
let I be set, i be object;
redefine func I --> i -> Function of I,{i}; :: redefines --> (FUNCOP_1, definition)
coherence
proof
dom (I --> i) = I & rng (I --> i) c= {i} by Th13;
hence thesis by FUNCT_2:def 1,RELSET_1:4;
end;
end;
definition
let B be non empty set, A be set, b be Element of B;
redefine func A --> b -> Function of A,B; :: redefines --> (FUNCOP_1, definition)
coherence by Th45;
end;
theorem
A --> x is Function of A,X;
reserve Y for set,
F for BinOp of X,
f,g,h for Function of Y,X,
x,x1,x2 for Element of X;
theorem Th47:
F[:](f,x) is Function of Y,X
proof
dom f = Y by FUNCT_2:def 1;
then reconsider g = dom f --> x as Function of Y,X;
F*<:f,g:> is Function of Y,X;
hence thesis;
end;
definition
let X be non empty set, Z be set;
let F be BinOp of X, f be Function of Z,X, x be Element of X;
redefine func F[:](f,x) -> Function of Z,X; :: redefines [:] (FUNCOP_1, definition)
coherence by Th47;
end;
reserve Y for non empty set,
F for BinOp of X,
f,g,h for Function of Y,X,
x,x1,x2 for Element of X;
theorem Th48:
for y being Element of Y holds (F[:](f,x)).y = F.(f.y,x)
proof
let y be Element of Y;
dom (F[:](f,x)) = Y by FUNCT_2:def 1;
hence thesis by Th27;
end;
theorem Th49:
(for y being Element of Y holds g.y = F.(f.y,x)) implies g = F
[:](f,x)
proof
assume
A1: for y being Element of Y holds g.y = F.(f.y,x);
now
let y be Element of Y;
thus g.y = F.(f.y,x) by A1
.= (F[:](f,x)).y by Th48;
end;
hence thesis by FUNCT_2:63;
end;
theorem
F[:](id X, x)*f = F[:](f,x)
proof
thus F[:](id X, x)*f = F[:](id X*f, x) by Th29
.= F[:](f,x) by FUNCT_2:17;
end;
theorem
F[:](id X, x).x = F.(x,x)
proof
thus F[:](id X, x).x = F.(id X.x, x) by Th48
.= F.(x,x);
end;
reserve Y for set,
F for BinOp of X,
f,g,h for Function of Y,X,
x,x1,x2 for Element of X;
theorem Th52:
F[;](x,g) is Function of Y,X
proof
dom g = Y by FUNCT_2:def 1;
then reconsider f = dom g --> x as Function of Y,X;
F*<:f,g:> is Function of Y,X;
hence thesis;
end;
definition
let X be non empty set, Z be set;
let F be BinOp of X, x be Element of X;
let g be Function of Z,X;
redefine func F[;](x,g) -> Function of Z,X; :: redefines [;] (FUNCOP_1, definition)
coherence by Th52;
end;
reserve Y for non empty set,
F for BinOp of X,
f,g,h for Function of Y,X,
x,x1,x2 for Element of X;
theorem Th53:
for y being Element of Y holds (F[;](x,f)).y = F.(x,f.y)
proof
let y be Element of Y;
dom (F[;](x,f)) = Y by FUNCT_2:def 1;
hence thesis by Th32;
end;
theorem Th54:
(for y being Element of Y holds g.y = F.(x,f.y)) implies g = F
[;](x,f)
proof
assume
A1: for y being Element of Y holds g.y = F.(x,f.y);
now
let y be Element of Y;
thus g.y = F.(x,f.y) by A1
.= (F[;](x,f)).y by Th53;
end;
hence thesis by FUNCT_2:63;
end;
reserve Y for set,
F for BinOp of X,
f,g,h for Function
of Y,X,
x,x1,x2 for Element of X;
theorem
F[;](x, id X)*f = F[;](x,f)
proof
thus F[;](x, id X)*f = F[;](x, id X*f) by Th34
.= F[;](x,f) by FUNCT_2:17;
end;
theorem
F[;](x, id X).x = F.(x,x)
proof
thus F[;](x, id X).x = F.(x, id X.x) by Th53
.= F.(x,x);
end;
theorem
for X,Y,Z being non empty set for f being Function of X, [:Y,Z:] for x
being Element of X holds f~.x =[(f.x)`2,(f.x)`1]
proof
let X,Y,Z be non empty set;
let f be Function of X, [:Y,Z:];
let x be Element of X;
x in X;
then
A1: x in dom f by FUNCT_2:def 1;
f.x = [(f.x)`1, (f.x)`2] by MCART_1:22;
hence thesis by A1,Def1;
end;
definition
let X,Y,Z be non empty set;
let f be Function of X, [:Y,Z:];
redefine func rng f -> Relation of Y,Z; :: redefines rng (FUNCT_1, redefinition) → rng (RELAT_1, synonym) → proj2 (XTUPLE_0, definition)
coherence by RELAT_1:def 19;
end;
definition
let X,Y,Z be non empty set;
let f be Function of X, [:Y,Z:];
redefine func f~ -> Function of X, [:Z,Y:]; :: redefines ~ (FUNCOP_1, definition)
coherence
proof
A1: rng (f~) c= [:Z,Y:]
proof
let x be object;
assume x in rng (f~);
then consider y being object such that
A2: y in dom (f~) and
A3: x = f~.y by FUNCT_1:def 3;
A4: y in dom f by A2,Def1;
then reconsider y as Element of X;
A5: f.y = [(f.y)`1,(f.y)`2] by MCART_1:21;
then f~.y = [(f.y)`2,(f.y)`1] by A4,Def1;
hence thesis by A3,A5,ZFMISC_1:88;
end;
X = dom f by FUNCT_2:def 1
.= dom (f~) by Def1;
hence thesis by A1,FUNCT_2:def 1,RELSET_1:4;
end;
end;
theorem
for X,Y,Z being non empty set for f being Function of X, [:Y,Z:] holds
rng (f~) = (rng f)~
proof
let X,Y,Z be non empty set;
let f be Function of X, [:Y,Z:];
let x,y be object;
thus [x,y] in rng (f~) implies [x,y] in (rng f)~
proof
assume [x,y] in rng (f~);
then consider z being object such that
A1: z in dom (f~) and
A2: [x,y] = f~.z by FUNCT_1:def 3;
A3: z in dom f by A1,Def1;
f.z = f~~.z
.= [y,x] by A1,A2,Def1;
then [y,x] in rng f by A3,FUNCT_1:def 3;
hence thesis by RELAT_1:def 7;
end;
assume [x,y] in (rng f)~;
then [y,x] in rng f by RELAT_1:def 7;
then consider z being object such that
A4: z in dom f & [y,x] = f.z by FUNCT_1:def 3;
z in dom (f~) & f~.z = [x,y] by A4,Def1;
hence thesis by FUNCT_1:def 3;
end;
reserve y for Element of Y;
theorem
F is associative implies F[:](F[;](x1,f),x2) = F[;](x1,F[:](f,x2))
proof
assume
A1: F is associative;
per cases;
suppose
Y = {};
hence thesis;
end;
suppose
A2: Y <> {};
now
let y;
reconsider x3 = f.y as Element of X by A2,FUNCT_2:5;
thus (F[:](F[;](x1,f),x2)).y = F.((F[;](x1,f)).y,x2) by A2,Th48
.= F.(F.(x1,x3),x2) by A2,Th53
.= F.(x1,F.(x3,x2)) by A1
.= F.(x1,(F[:](f,x2)).y) by A2,Th48;
end;
hence thesis by A2,Th54;
end;
end;
theorem
F is associative implies F.:(F[:](f,x),g) = F.:(f,F[;](x,g))
proof
assume
A1: F is associative;
per cases;
suppose
Y = {};
hence thesis;
end;
suppose
A2: Y <> {};
now
let y;
reconsider x1 = f.y, x2 = g.y as Element of X by A2,FUNCT_2:5;
thus (F.:(F[:](f,x),g)).y = F.((F[:](f,x)).y,g.y) by A2,Th37
.= F.(F.(x1,x),x2) by A2,Th48
.= F.(x1,F.(x,x2)) by A1
.= F.(f.y,(F[;](x,g)).y) by A2,Th53;
end;
hence thesis by A2,Th38;
end;
end;
theorem
F is associative implies F.:(F.:(f,g),h) = F.:(f,F.:(g,h))
proof
assume
A1: F is associative;
per cases;
suppose
Y = {};
hence thesis;
end;
suppose
A2: Y <> {};
now
let y;
reconsider x1 = f.y, x2 = g.y, x3 = h.y as Element of X by A2,FUNCT_2:5;
thus (F.:(F.:(f,g),h)).y = F.((F.:(f,g)).y,h.y) by A2,Th37
.= F.(F.(f.y,g.y),h.y) by A2,Th37
.= F.(x1,F.(x2,x3)) by A1
.= F.(f.y,(F.:(g,h)).y) by A2,Th37;
end;
hence thesis by A2,Th38;
end;
end;
theorem
F is associative implies F[;](F.(x1,x2),f) = F[;](x1,F[;](x2,f))
proof
assume
A1: F is associative;
per cases;
suppose
Y = {};
hence thesis;
end;
suppose
A2: Y <> {};
now
let y;
reconsider x3 = f.y as Element of X by A2,FUNCT_2:5;
thus (F[;](F.(x1,x2),f)).y = F.(F.(x1,x2),f.y) by A2,Th53
.= F.(x1,F.(x2,x3)) by A1
.= F.(x1,(F[;](x2,f)).y) by A2,Th53;
end;
hence thesis by A2,Th54;
end;
end;
theorem
F is associative implies F[:](f, F.(x1,x2)) = F[:](F[:](f,x1),x2)
proof
assume
A1: F is associative;
per cases;
suppose
Y = {};
hence thesis;
end;
suppose
A2: Y <> {};
now
let y;
reconsider x3 = f.y as Element of X by A2,FUNCT_2:5;
thus (F[:](f, F.(x1,x2))).y = F.(f.y, F.(x1,x2)) by A2,Th48
.= F.(F.(x3,x1),x2) by A1
.= F.(F[:](f,x1).y,x2) by A2,Th48;
end;
hence thesis by A2,Th49;
end;
end;
theorem
F is commutative implies F[;](x,f) = F[:](f,x)
proof
assume
A1: F is commutative;
per cases;
suppose
Y = {};
hence thesis;
end;
suppose
A2: Y <> {};
now
let y;
reconsider x1 = f.y as Element of X by A2,FUNCT_2:5;
thus (F[;](x,f)).y = F.(x,x1) by A2,Th53
.= F.(f.y,x) by A1;
end;
hence thesis by A2,Th49;
end;
end;
theorem
F is commutative implies F.:(f,g) = F.:(g,f)
proof
assume
A1: F is commutative;
per cases;
suppose
Y = {};
hence thesis;
end;
suppose
A2: Y <> {};
now
let y;
reconsider x1 = f.y, x2 = g.y as Element of X by A2,FUNCT_2:5;
thus (F.:(f,g)).y = F.(x1,x2) by A2,Th37
.= F.(g.y,f.y) by A1;
end;
hence thesis by A2,Th38;
end;
end;
theorem
F is idempotent implies F.:(f,f) = f
proof
assume
A1: F is idempotent;
per cases;
suppose
A2: Y = {};
hence F.:(f,f) = {}
.= f by A2;
end;
suppose
A3: Y <> {};
now
let y;
reconsider x = f.y as Element of X by A3,FUNCT_2:5;
thus f.y = F.(x,x) by A1
.= F.(f.y,f.y);
end;
hence thesis by A3,Th38;
end;
end;
reserve Y for non empty set,
F for BinOp of X,
f for Function of Y,X,
x for Element of X,
y for Element of Y;
theorem
F is idempotent implies F[;](f.y,f).y = f.y
proof
assume
A1: F is idempotent;
thus F[;](f.y,f).y = F.(f.y,f.y) by Th53
.= f.y by A1;
end;
theorem
F is idempotent implies F[:](f,f.y).y = f.y
proof
assume
A1: F is idempotent;
thus F[:](f,f.y).y = F.(f.y,f.y) by Th48
.= f.y by A1;
end;
:: Addendum, 2002.07.08
theorem
for F,f,g being Function st [:rng f, rng g:] c= dom F holds dom(F.:(f,
g)) = dom f /\ dom g
proof
let F,f,g be Function such that
A1: [:rng f, rng g:] c= dom F;
rng<:f,g:> c= [:rng f, rng g:] by FUNCT_3:51;
hence dom(F.:(f,g)) = dom<:f,g:> by A1,RELAT_1:27,XBOOLE_1:1
.= dom f /\ dom g by FUNCT_3:def 7;
end;
:: from PRALG_1, 2004.07.23
definition
let IT be Function;
attr IT is Function-yielding means
:Def6:
for x being object st x in dom IT holds IT.x is Function;
end;
registration
cluster Function-yielding for Function;
existence
proof
take the set --> the Function;
let x be object;
thus thesis;
end;
end;
registration
let B be Function-yielding Function, j be object;
cluster B.j -> Function-like Relation-like;
coherence
proof
per cases;
suppose
j in dom B;
hence thesis by Def6;
end;
suppose
not j in dom B;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
registration
let F be Function-yielding Function, f be Function;
cluster F * f -> Function-yielding;
coherence
proof
thus F * f is Function-yielding
proof
let x be object;
assume x in dom (F*f);
then (F*f).x = F.(f.x) by FUNCT_1:12;
hence thesis;
end;
end;
end;
:: missing, 2005.11.13, A.T.
registration
let B;
let c be non empty set;
cluster B --> c -> non-empty;
coherence
proof
not {} in rng(B --> c) by TARSKI:def 1;
hence thesis;
end;
end;
:: missing, 2005.12.20, A.T.
theorem
([:X,Y:] --> z).(x,y) = z by Th7,ZFMISC_1:87;
:: from CAT_1, 2007.02.11, A.T.
reserve a,b,c for set;
definition
let a,b,c be object;
func (a,b).-->c -> Function equals
{[a,b]} --> c;
coherence;
end;
theorem
for a,b,c being object holds
((a,b).-->c).(a,b) = c
proof let a,b,c be object;
[a,b] in {[a,b]} by TARSKI:def 1;
hence thesis by Th7;
end;
:: from CQC_LANG, 2007.03.13, A.T.
definition
let x,y,a,b be object;
func IFEQ(x,y,a,b) -> object equals
:Def8:
a if x = y otherwise b;
correctness;
end;
definition
let x,y be object; let a,b be set;
redefine func IFEQ(x,y,a,b) -> set; :: redefines IFEQ (FUNCOP_1, definition)
correctness
proof
x = y or x <> y;
hence thesis by Def8;
end;
end;
definition
let D be set;
let x,y be object, a,b be Element of D;
redefine func IFEQ(x,y,a,b) -> Element of D; :: redefines IFEQ (FUNCOP_1, definition)
coherence
proof
x = y or x <> y;
hence thesis by Def8;
end;
end;
definition
let x,y be object;
func x .--> y -> set equals
{x} --> y;
coherence;
end;
registration
let x,y be object;
cluster x .--> y -> Function-like Relation-like;
coherence;
end;
registration
let x,y be object;
cluster x .--> y -> one-to-one;
coherence
proof
let x1,x2 be object;
set f = x .--> y;
assume that
A1: x1 in dom f and
A2: x2 in dom f;
x1 =x by A1,TARSKI:def 1;
hence thesis by A2,TARSKI:def 1;
end;
end;
theorem Th72:
for x,y be object holds (x .--> y).x = y
proof
let x,y be object;
x in {x} by TARSKI:def 1;
hence thesis by Th7;
end;
:: from SCMFSA6A, 2007.07.22, A.T.
theorem
for a,b being object, f being Function holds a.-->b c= f iff a in dom f &
f.a = b
proof
let a,b be object, f be Function;
A1: dom(a.-->b) = {a};
A2: a in dom(a.-->b) by TARSKI:def 1;
hereby
assume
A3: a.-->b c= f;
then {a} c= dom f by A1,GRFUNC_1:2;
hence a in dom f by ZFMISC_1:31;
thus f.a = (a.-->b).a by A2,A3,GRFUNC_1:2
.= b by Th72;
end;
assume that
A4: a in dom f and
A5: f.a = b;
A6: now
let x be object;
assume x in dom(a.-->b);
then x = a by TARSKI:def 1;
hence (a.-->b).x = f.x by A5,Th72;
end;
dom(a.-->b) c= dom f by A4,ZFMISC_1:31;
hence thesis by A6,GRFUNC_1:2;
end;
:: from FUNCT_2, 2007.11.22, A.T., :: from CAT_4
notation
let o,m,r be object;
synonym (o,m) :-> r for (o,m) .--> r;
end;
Lm2: for o,m,r be object holds (o,m) :-> r is Function of [:{o},{m}:],{r}
proof
let o,m,r be object;
[:{o},{m}:] = {[o,m]} by ZFMISC_1:29;
hence thesis;
end;
definition
let o,m,r be object;
redefine func (o,m) :-> r -> Function of [:{o},{m}:],{r} means :: redefines :-> (FUNCOP_1, synonym) → .--> (FUNCOP_1, definition)
not contradiction;
coherence by Lm2;
compatibility
proof
let f be Function of [:{o},{m}:],{r};
(o,m) .--> r is Function of [:{o},{m}:],{r} by Lm2;
hence thesis by FUNCT_2:51;
end;
end;
:: missing, 2008.03.20, A.T.
reserve x,y,z for object;
theorem
x in dom(x .--> y) by TARSKI:def 1;
theorem
z in dom(x .--> y) implies z = x by TARSKI:def 1;
:: missing, 2008.04.15, A.T.
theorem
not x in A implies (x .--> y)|A = {}
proof
assume not x in A;
then dom(x .--> y) misses A by ZFMISC_1:50;
hence thesis by RELAT_1:66;
end;
:: from CAT_1, (new notation), 2008.06.30. A.T.
notation
let x,y be object;
synonym x :-> y for x .--> y;
end;
definition
let m,o be object;
redefine func m :-> o -> Function of {m}, {o}; :: redefines :-> (FUNCOP_1, synonym) → .--> (FUNCOP_1, definition)
coherence;
end;
theorem
for x being Element of {a} for y being Element of {b} holds
((a,b):->c).(x,y) = c by TARSKI:def 1;
:: from MSUHOM_1, ALTCAT_1, 2008.07.06, A.T.
registration
let f be Function-yielding Function, C be set;
cluster f|C -> Function-yielding;
coherence
proof
let i be object;
f.i is Function;
hence thesis by FUNCT_1:47;
end;
end;
:: from CIRCCOMB, 2008.07.06, A.T.
registration
let A be set;
let f be Function;
cluster A --> f -> Function-yielding;
coherence;
end;
:: from SEQM_3, 2008.07.17, A.T.
registration
let X be set, a be object;
cluster X --> a -> constant;
coherence
proof
let x,y be object;
assume that
A1: x in dom(X --> a) and
A2: y in dom(X --> a);
thus (X --> a).x = a by A1,Th7
.= (X --> a).y by A2,Th7;
end;
end;
:: from YELLOW_6, 2008.07.17, A.T.
registration
cluster non empty constant for Function;
existence
proof
take {{}} --> {};
thus thesis;
end;
let X be set, Y be non empty set;
cluster constant for Function of X,Y;
existence
proof
take X --> the Element of Y;
thus thesis;
end;
end;
:: missing, 2008.07.17, A.T.
registration
let f be constant Function, X be set;
cluster f|X -> constant;
coherence
proof
let x,y be object;
A1: dom(f|X) c= dom f by RELAT_1:60;
assume that
A2: x in dom(f|X) and
A3: y in dom (f|X);
thus (f|X).x = f.x by A2,FUNCT_1:47
.= f.y by A1,A2,A3,FUNCT_1:def 10
.= (f|X).y by A3,FUNCT_1:47;
end;
end;
:: missing, 2008.08.14, A.T.
theorem
for f being non empty constant Function ex y st for x st x in dom f
holds f.x = y
proof
let f be non empty constant Function;
consider y being object such that
A1: y in rng f by XBOOLE_0:def 1;
take y;
ex x0 being object st x0 in dom f & f.x0 = y by A1,FUNCT_1:def 3;
hence thesis by FUNCT_1:def 10;
end;
:: from YELLOW_6, 2008.12.26, A.T.
theorem
for X being non empty set, x being set holds the_value_of (X --> x) =
x
proof
let X be non empty set, x be set;
set f = X --> x;
ex i being set st i in dom f & the_value_of f = f.i by FUNCT_1:def 12;
hence thesis by Th7;
end;
:: from CIRCCMB3, 2008.12.26, A.T.
theorem
for f being constant Function holds f = (dom f) --> the_value_of f
proof
let f be constant Function;
thus dom ((dom f) --> the_value_of f) = dom f;
let x be object;
assume
A1: x in dom f;
then f <> {} & ((dom f) --> the_value_of f).x = the_value_of f by Th7;
hence thesis by A1,FUNCT_1:def 12;
end;
:: missing, 2009.01.21, A.T.
registration
let X be set, Y be non empty set;
cluster total for PartFunc of X,Y;
existence
proof
consider y being object such that
A1: y in Y by XBOOLE_0:def 1;
reconsider y as Element of Y by A1;
take X --> y;
thus thesis;
end;
end;
:: new, 2009.02.14, A.T.
registration
let I be set, A be object;
cluster I --> A -> I-defined;
coherence;
end;
registration
let I, A be object;
cluster I .--> A -> {I}-defined;
coherence;
end;
:: BORSUK_1:6, 2009.06.11, A.K.
theorem
(A --> x).:B c= {x};
registration
let I be set, f be Function;
cluster I .--> f -> Function-yielding;
coherence;
end;
:: 2009.10.03, A.T.
registration let I be set;
cluster total for I-defined non-empty Function;
existence
proof
take I --> {{}};
thus thesis;
end;
end;
theorem Th82:
x .--> y is_isomorphism_of {[x,x]},{[y,y]}
proof
set F = x .--> y;
set R = {[x,x]};
set S = {[y,y]};
A1: field R = {x} by RELAT_1:173;
hence dom F = field R;
field S = {y} by RELAT_1:173;
hence rng F = field S by RELAT_1:160;
thus F is one-to-one;
let a,b be object;
hereby
assume [a,b] in R;
then [a,b] = [x,x] by TARSKI:def 1;
then
A2: a = x & b = x by XTUPLE_0:1;
hence a in field R & b in field R by A1,TARSKI:def 1;
F.x = y by Th72;
hence [F.a,F.b] in S by A2,TARSKI:def 1;
end;
assume a in field R & b in field R;
then a = x & b = x by A1,TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
theorem
{[x,x]}, {[y,y]} are_isomorphic
proof
take x .--> y;
thus thesis by Th82;
end;
registration
let I be set, A be object;
cluster I --> A -> total for I-defined Function;
coherence;
end;
theorem
for f being Function st x in dom f
holds x .--> f.x c= f
proof
let f be Function;
assume x in dom f;
then {[x, f.x]} c= f by ZFMISC_1:31,FUNCT_1:1;
hence thesis by ZFMISC_1:29;
end;
registration let A be non empty set;
let x be set, i be Element of A;
cluster x .--> i -> A-valued;
coherence
proof
rng(x .--> i) = {i} by RELAT_1:160;
hence rng(x .--> i) c= A by ZFMISC_1:31;
end;
end;
reserve Y for set,
f,g for Function of Y,X,
x for Element of X,
y for Element of Y;
:: missing, 2010.02.10, A.T.
theorem
F is associative implies F.:(F[;](x,f),g) = F[;](x,F.:(f,g))
proof
assume
A1: F is associative;
per cases;
suppose
Y = {};
hence thesis;
end;
suppose
A2: Y <> {};
now
let y;
reconsider x1 = f.y, x2 = g.y as Element of X by A2,FUNCT_2:5;
thus (F[;](x,F.:(f,g))).y = F.(x,F.:(f,g).y) by A2,Th53
.= F.(x,F.(x1,x2)) by A2,Th37
.= F.(F.(x,x1),x2) by A1
.= F.(F[;](x,f).y,g.y) by A2,Th53;
end;
hence thesis by A2,Th38;
end;
end;
registration let A be set, B be non empty set, x be Element of B;
cluster A --> x -> B-valued;
coherence;
end;
registration let A be non empty set, x be Element of A, y be object;
cluster x .--> y -> A-defined;
coherence by ZFMISC_1:31;
end;
theorem
for x,y,A being set st x in A
holds (x .--> y)|A = x .--> y
proof let x,y,A be set;
assume x in A;
then dom(x .--> y) c= A by ZFMISC_1:31;
hence thesis by RELAT_1:68;
end;
:: missing, 2011.02.06, A.K.
registration
let Y be functional set;
cluster Y-valued -> Function-yielding for Function;
coherence;
end;
:: from MSUALG_4, 2011.04.16, A.T.
definition
let IT be Function;
attr IT is Relation-yielding means
for x being object st x in dom IT holds IT.x is Relation;
end;
registration
cluster Function-yielding -> Relation-yielding for Function;
coherence;
end;
registration
cluster empty -> Function-yielding for Function;
coherence;
end;
:: from CIRCCOMB, 2011.04.19, A.T.
theorem
for X,Y being set, x,y being object
holds X --> x tolerates Y --> y iff x = y or X misses Y
proof
let X,Y be set;
let x,y be object;
set f = X --> x, g = Y --> y;
thus f tolerates g implies x = y or X misses Y
proof
assume that
A3: for z being object st z in dom f /\ dom g holds f.z = g.z and
A4: x <> y;
assume X meets Y;
then consider z be object such that
A5: z in X and
A6: z in Y by XBOOLE_0:3;
A7: f.z = x by A5,Th7;
A8: g.z = y by A6,Th7;
z in X /\ Y by A5,A6,XBOOLE_0:def 4;
hence thesis by A3,A4,A7,A8;
end;
assume
A9: x = y or X misses Y;
let z be object;
assume
A10: z in dom f /\ dom g;
then
A11: z in Y;
A12: z in X by A10,XBOOLE_0:def 4;
then f.z = x by Th7;
hence thesis by A9,A12,A11,Th7,XBOOLE_0:3;
end;
reserve x,y,z,A for set;
theorem Th88:
rng(x .--> y) = {y}
proof
dom(x .--> y) = {x};
hence rng(x .--> y) = {(x .--> y).x} by FUNCT_1:4
.= {y} by Th72;
end;
theorem
z in A implies (A --> x)*(y .--> z) = y .--> x
proof assume
A1: z in A;
A2: dom(y .--> z) = {y}
.= dom(y .--> x);
rng(y .--> z) = {z} by Th88;
then rng(y .--> z) c= dom(A --> x) by A1,ZFMISC_1:31;
hence dom((A --> x)*(y .--> z)) = dom(y .--> x) by A2,RELAT_1:27;
let e be object;
assume
A3: e in dom((A --> x)*(y .--> z));
thus ((A --> x)*(y .--> z)).e = (A --> x).((y .--> z).e) by A3,FUNCT_1:12
.= (A --> x).z by A3,Th7
.= x by A1,Th7
.= (y .--> x).e by A3,Th7;
end;
registration
let f be Function-yielding Function;
let a,b be object;
cluster f.(a,b) -> Function-like Relation-like;
coherence;
end;
registration
let Y be set;
let X,Z be non empty set;
cluster -> Function-yielding for Function of X, Funcs(Y,Z);
coherence;
end;