:: GRFUNC_1 semantic presentation
begin
theorem Th1: :: GRFUNC_1:1
for f being Function
for G being set st G c= f holds
G is Function ;
theorem Th2: :: GRFUNC_1:2
for f, g being Function holds
( f c= g iff ( dom f c= dom g & ( for x being set st x in dom f holds
f . x = g . x ) ) )
proof
let f, g be Function; ::_thesis: ( f c= g iff ( dom f c= dom g & ( for x being set st x in dom f holds
f . x = g . x ) ) )
thus ( f c= g implies ( dom f c= dom g & ( for x being set st x in dom f holds
f . x = g . x ) ) ) ::_thesis: ( dom f c= dom g & ( for x being set st x in dom f holds
f . x = g . x ) implies f c= g )
proof
assume A1: f c= g ; ::_thesis: ( dom f c= dom g & ( for x being set st x in dom f holds
f . x = g . x ) )
hence dom f c= dom g by RELAT_1:11; ::_thesis: for x being set st x in dom f holds
f . x = g . x
let x be set ; ::_thesis: ( x in dom f implies f . x = g . x )
assume x in dom f ; ::_thesis: f . x = g . x
then [x,(f . x)] in f by FUNCT_1:def_2;
hence f . x = g . x by A1, FUNCT_1:1; ::_thesis: verum
end;
assume that
A2: dom f c= dom g and
A3: for x being set st x in dom f holds
f . x = g . x ; ::_thesis: f c= g
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in f or [x,b1] in g )
let y be set ; ::_thesis: ( not [x,y] in f or [x,y] in g )
assume A4: [x,y] in f ; ::_thesis: [x,y] in g
then A5: x in dom f by FUNCT_1:1;
y = f . x by A4, FUNCT_1:1;
then y = g . x by A3, A5;
hence [x,y] in g by A2, A5, FUNCT_1:def_2; ::_thesis: verum
end;
theorem :: GRFUNC_1:3
for f, g being Function st dom f = dom g & f c= g holds
f = g
proof
let f, g be Function; ::_thesis: ( dom f = dom g & f c= g implies f = g )
assume that
A1: dom f = dom g and
A2: f c= g ; ::_thesis: f = g
for x, y being set holds
( [x,y] in f iff [x,y] in g )
proof
let x, y be set ; ::_thesis: ( [x,y] in f iff [x,y] in g )
thus ( [x,y] in f implies [x,y] in g ) by A2; ::_thesis: ( [x,y] in g implies [x,y] in f )
assume A3: [x,y] in g ; ::_thesis: [x,y] in f
then x in dom f by A1, XTUPLE_0:def_12;
then [x,(f . x)] in f by FUNCT_1:1;
hence [x,y] in f by A2, A3, FUNCT_1:def_1; ::_thesis: verum
end;
hence f = g by RELAT_1:def_2; ::_thesis: verum
end;
Lm1: for x, y being set
for f, h being Function st (rng f) /\ (rng h) = {} & x in dom f & y in dom h holds
f . x <> h . y
proof
let x, y be set ; ::_thesis: for f, h being Function st (rng f) /\ (rng h) = {} & x in dom f & y in dom h holds
f . x <> h . y
let f, h be Function; ::_thesis: ( (rng f) /\ (rng h) = {} & x in dom f & y in dom h implies f . x <> h . y )
assume A1: (rng f) /\ (rng h) = {} ; ::_thesis: ( not x in dom f or not y in dom h or f . x <> h . y )
assume ( x in dom f & y in dom h ) ; ::_thesis: f . x <> h . y
then ( f . x in rng f & h . y in rng h ) by FUNCT_1:def_3;
hence f . x <> h . y by A1, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem :: GRFUNC_1:4
for x, z being set
for g, f being Function st [x,z] in g * f holds
( [x,(f . x)] in f & [(f . x),z] in g )
proof
let x, z be set ; ::_thesis: for g, f being Function st [x,z] in g * f holds
( [x,(f . x)] in f & [(f . x),z] in g )
let g, f be Function; ::_thesis: ( [x,z] in g * f implies ( [x,(f . x)] in f & [(f . x),z] in g ) )
assume [x,z] in g * f ; ::_thesis: ( [x,(f . x)] in f & [(f . x),z] in g )
then ex y being set st
( [x,y] in f & [y,z] in g ) by RELAT_1:def_8;
hence ( [x,(f . x)] in f & [(f . x),z] in g ) by FUNCT_1:1; ::_thesis: verum
end;
theorem :: GRFUNC_1:5
for x, y being set holds {[x,y]} is Function ;
Lm2: for x, y, x1, y1 being set st [x,y] in {[x1,y1]} holds
( x = x1 & y = y1 )
proof
let x, y, x1, y1 be set ; ::_thesis: ( [x,y] in {[x1,y1]} implies ( x = x1 & y = y1 ) )
assume [x,y] in {[x1,y1]} ; ::_thesis: ( x = x1 & y = y1 )
then [x,y] = [x1,y1] by TARSKI:def_1;
hence ( x = x1 & y = y1 ) by XTUPLE_0:1; ::_thesis: verum
end;
theorem :: GRFUNC_1:6
for x, y being set
for f being Function st f = {[x,y]} holds
f . x = y
proof
let x, y be set ; ::_thesis: for f being Function st f = {[x,y]} holds
f . x = y
let f be Function; ::_thesis: ( f = {[x,y]} implies f . x = y )
assume f = {[x,y]} ; ::_thesis: f . x = y
then [x,y] in f by TARSKI:def_1;
hence f . x = y by FUNCT_1:1; ::_thesis: verum
end;
theorem Th7: :: GRFUNC_1:7
for x being set
for f being Function st dom f = {x} holds
f = {[x,(f . x)]}
proof
let x be set ; ::_thesis: for f being Function st dom f = {x} holds
f = {[x,(f . x)]}
let f be Function; ::_thesis: ( dom f = {x} implies f = {[x,(f . x)]} )
reconsider g = {[x,(f . x)]} as Function ;
assume A1: dom f = {x} ; ::_thesis: f = {[x,(f . x)]}
for y, z being set holds
( [y,z] in f iff [y,z] in g )
proof
let y, z be set ; ::_thesis: ( [y,z] in f iff [y,z] in g )
thus ( [y,z] in f implies [y,z] in g ) ::_thesis: ( [y,z] in g implies [y,z] in f )
proof
assume A2: [y,z] in f ; ::_thesis: [y,z] in g
then y in {x} by A1, XTUPLE_0:def_12;
then A3: y = x by TARSKI:def_1;
A4: rng f = {(f . x)} by A1, FUNCT_1:4;
z in rng f by A2, XTUPLE_0:def_13;
then z = f . x by A4, TARSKI:def_1;
hence [y,z] in g by A3, TARSKI:def_1; ::_thesis: verum
end;
assume [y,z] in g ; ::_thesis: [y,z] in f
then A5: ( y = x & z = f . x ) by Lm2;
x in dom f by A1, TARSKI:def_1;
hence [y,z] in f by A5, FUNCT_1:def_2; ::_thesis: verum
end;
hence f = {[x,(f . x)]} by RELAT_1:def_2; ::_thesis: verum
end;
theorem :: GRFUNC_1:8
for x1, y1, x2, y2 being set holds
( {[x1,y1],[x2,y2]} is Function iff ( x1 = x2 implies y1 = y2 ) )
proof
let x1, y1, x2, y2 be set ; ::_thesis: ( {[x1,y1],[x2,y2]} is Function iff ( x1 = x2 implies y1 = y2 ) )
thus ( {[x1,y1],[x2,y2]} is Function & x1 = x2 implies y1 = y2 ) ::_thesis: ( ( x1 = x2 implies y1 = y2 ) implies {[x1,y1],[x2,y2]} is Function )
proof
A1: ( [x1,y1] in {[x1,y1],[x2,y2]} & [x2,y2] in {[x1,y1],[x2,y2]} ) by TARSKI:def_2;
assume {[x1,y1],[x2,y2]} is Function ; ::_thesis: ( not x1 = x2 or y1 = y2 )
hence ( not x1 = x2 or y1 = y2 ) by A1, FUNCT_1:def_1; ::_thesis: verum
end;
assume A2: ( x1 = x2 implies y1 = y2 ) ; ::_thesis: {[x1,y1],[x2,y2]} is Function
now__::_thesis:_(_(_for_p_being_set_st_p_in_{[x1,y1],[x2,y2]}_holds_
ex_x,_y_being_set_st_[x,y]_=_p_)_&_(_for_x,_z1,_z2_being_set_st_[x,z1]_in_{[x1,y1],[x2,y2]}_&_[x,z2]_in_{[x1,y1],[x2,y2]}_holds_
z1_=_z2_)_)
thus for p being set st p in {[x1,y1],[x2,y2]} holds
ex x, y being set st [x,y] = p ::_thesis: for x, z1, z2 being set st [x,z1] in {[x1,y1],[x2,y2]} & [x,z2] in {[x1,y1],[x2,y2]} holds
z1 = z2
proof
let p be set ; ::_thesis: ( p in {[x1,y1],[x2,y2]} implies ex x, y being set st [x,y] = p )
assume p in {[x1,y1],[x2,y2]} ; ::_thesis: ex x, y being set st [x,y] = p
then ( p = [x1,y1] or p = [x2,y2] ) by TARSKI:def_2;
hence ex x, y being set st [x,y] = p ; ::_thesis: verum
end;
let x, z1, z2 be set ; ::_thesis: ( [x,z1] in {[x1,y1],[x2,y2]} & [x,z2] in {[x1,y1],[x2,y2]} implies z1 = z2 )
A3: ( ( not ( [x,z1] = [x1,y1] & [x,z2] = [x1,y1] ) & not ( [x,z1] = [x2,y2] & [x,z2] = [x2,y2] ) ) or ( z1 = y1 & z2 = y1 ) or ( z1 = y2 & z2 = y2 ) ) by XTUPLE_0:1;
A4: now__::_thesis:_(_(_(_[x,z1]_=_[x1,y1]_&_[x,z2]_=_[x2,y2]_)_or_(_[x,z1]_=_[x2,y2]_&_[x,z2]_=_[x1,y1]_)_)_implies_z1_=_z2_)
assume A5: ( ( [x,z1] = [x1,y1] & [x,z2] = [x2,y2] ) or ( [x,z1] = [x2,y2] & [x,z2] = [x1,y1] ) ) ; ::_thesis: z1 = z2
then ( x = x1 & x = x2 ) by XTUPLE_0:1;
hence z1 = z2 by A2, A5, XTUPLE_0:1; ::_thesis: verum
end;
assume ( [x,z1] in {[x1,y1],[x2,y2]} & [x,z2] in {[x1,y1],[x2,y2]} ) ; ::_thesis: z1 = z2
hence z1 = z2 by A3, A4, TARSKI:def_2; ::_thesis: verum
end;
hence {[x1,y1],[x2,y2]} is Function by FUNCT_1:def_1; ::_thesis: verum
end;
theorem Th9: :: GRFUNC_1:9
for f being Function holds
( f is one-to-one iff for x1, x2, y being set st [x1,y] in f & [x2,y] in f holds
x1 = x2 )
proof
let f be Function; ::_thesis: ( f is one-to-one iff for x1, x2, y being set st [x1,y] in f & [x2,y] in f holds
x1 = x2 )
thus ( f is one-to-one implies for x1, x2, y being set st [x1,y] in f & [x2,y] in f holds
x1 = x2 ) ::_thesis: ( ( for x1, x2, y being set st [x1,y] in f & [x2,y] in f holds
x1 = x2 ) implies f is one-to-one )
proof
assume A1: f is one-to-one ; ::_thesis: for x1, x2, y being set st [x1,y] in f & [x2,y] in f holds
x1 = x2
let x1, x2, y be set ; ::_thesis: ( [x1,y] in f & [x2,y] in f implies x1 = x2 )
assume A2: ( [x1,y] in f & [x2,y] in f ) ; ::_thesis: x1 = x2
then A3: ( f . x1 = y & f . x2 = y ) by FUNCT_1:1;
( x1 in dom f & x2 in dom f ) by A2, FUNCT_1:1;
hence x1 = x2 by A1, A3, FUNCT_1:def_4; ::_thesis: verum
end;
assume A4: for x1, x2, y being set st [x1,y] in f & [x2,y] in f holds
x1 = x2 ; ::_thesis: f is one-to-one
let x1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x1 in proj1 f or not b1 in proj1 f or not f . x1 = f . b1 or x1 = b1 )
let x2 be set ; ::_thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; ::_thesis: x1 = x2
then ( [x1,(f . x1)] in f & [x2,(f . x1)] in f ) by FUNCT_1:1;
hence x1 = x2 by A4; ::_thesis: verum
end;
theorem Th10: :: GRFUNC_1:10
for g, f being Function st g c= f & f is one-to-one holds
g is one-to-one
proof
let g, f be Function; ::_thesis: ( g c= f & f is one-to-one implies g is one-to-one )
assume ( g c= f & f is one-to-one ) ; ::_thesis: g is one-to-one
then for x1, x2, y being set st [x1,y] in g & [x2,y] in g holds
x1 = x2 by Th9;
hence g is one-to-one by Th9; ::_thesis: verum
end;
registration
let f be Function;
let X be set ;
clusterf /\ X -> Function-like ;
coherence
f /\ X is Function-like by Th1, XBOOLE_1:17;
end;
theorem :: GRFUNC_1:11
for x being set
for f, g being Function st x in dom (f /\ g) holds
(f /\ g) . x = f . x
proof
let x be set ; ::_thesis: for f, g being Function st x in dom (f /\ g) holds
(f /\ g) . x = f . x
let f, g be Function; ::_thesis: ( x in dom (f /\ g) implies (f /\ g) . x = f . x )
set y = (f /\ g) . x;
assume x in dom (f /\ g) ; ::_thesis: (f /\ g) . x = f . x
then [x,((f /\ g) . x)] in f /\ g by FUNCT_1:def_2;
then [x,((f /\ g) . x)] in f by XBOOLE_0:def_4;
hence (f /\ g) . x = f . x by FUNCT_1:1; ::_thesis: verum
end;
theorem :: GRFUNC_1:12
for f, g being Function st f is one-to-one holds
f /\ g is one-to-one by Th10, XBOOLE_1:17;
theorem :: GRFUNC_1:13
for f, g being Function st dom f misses dom g holds
f \/ g is Function
proof
let f, g be Function; ::_thesis: ( dom f misses dom g implies f \/ g is Function )
assume A1: (dom f) /\ (dom g) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: f \/ g is Function
now__::_thesis:_(_(_for_p_being_set_st_p_in_f_\/_g_holds_
ex_x,_y_being_set_st_[x,y]_=_p_)_&_(_for_x,_y1,_y2_being_set_st_[x,y1]_in_f_\/_g_&_[x,y2]_in_f_\/_g_holds_
y1_=_y2_)_)
thus for p being set st p in f \/ g holds
ex x, y being set st [x,y] = p by RELAT_1:def_1; ::_thesis: for x, y1, y2 being set st [x,y1] in f \/ g & [x,y2] in f \/ g holds
y1 = y2
let x, y1, y2 be set ; ::_thesis: ( [x,y1] in f \/ g & [x,y2] in f \/ g implies y1 = y2 )
assume [x,y1] in f \/ g ; ::_thesis: ( [x,y2] in f \/ g implies y1 = y2 )
then A2: ( [x,y1] in f or [x,y1] in g ) by XBOOLE_0:def_3;
assume [x,y2] in f \/ g ; ::_thesis: y1 = y2
then A3: ( [x,y2] in f or [x,y2] in g ) by XBOOLE_0:def_3;
( not x in dom f or not x in dom g ) by A1, XBOOLE_0:def_4;
hence y1 = y2 by A2, A3, FUNCT_1:def_1, XTUPLE_0:def_12; ::_thesis: verum
end;
hence f \/ g is Function by FUNCT_1:def_1; ::_thesis: verum
end;
theorem :: GRFUNC_1:14
for f, h, g being Function st f c= h & g c= h holds
f \/ g is Function by Th1, XBOOLE_1:8;
Lm3: for x being set
for h, f, g being Function st h = f \/ g holds
( x in dom h iff ( x in dom f or x in dom g ) )
proof
let x be set ; ::_thesis: for h, f, g being Function st h = f \/ g holds
( x in dom h iff ( x in dom f or x in dom g ) )
let h, f, g be Function; ::_thesis: ( h = f \/ g implies ( x in dom h iff ( x in dom f or x in dom g ) ) )
assume A1: h = f \/ g ; ::_thesis: ( x in dom h iff ( x in dom f or x in dom g ) )
thus ( not x in dom h or x in dom f or x in dom g ) ::_thesis: ( ( x in dom f or x in dom g ) implies x in dom h )
proof
assume x in dom h ; ::_thesis: ( x in dom f or x in dom g )
then [x,(h . x)] in h by FUNCT_1:def_2;
then ( [x,(h . x)] in f or [x,(h . x)] in g ) by A1, XBOOLE_0:def_3;
hence ( x in dom f or x in dom g ) by XTUPLE_0:def_12; ::_thesis: verum
end;
assume ( x in dom f or x in dom g ) ; ::_thesis: x in dom h
then ( [x,(f . x)] in f or [x,(g . x)] in g ) by FUNCT_1:def_2;
then ( [x,(f . x)] in h or [x,(g . x)] in h ) by A1, XBOOLE_0:def_3;
hence x in dom h by XTUPLE_0:def_12; ::_thesis: verum
end;
theorem Th15: :: GRFUNC_1:15
for x being set
for g, h, f being Function st x in dom g & h = f \/ g holds
h . x = g . x
proof
let x be set ; ::_thesis: for g, h, f being Function st x in dom g & h = f \/ g holds
h . x = g . x
let g, h, f be Function; ::_thesis: ( x in dom g & h = f \/ g implies h . x = g . x )
assume x in dom g ; ::_thesis: ( not h = f \/ g or h . x = g . x )
then [x,(g . x)] in g by FUNCT_1:def_2;
then ( h = f \/ g implies [x,(g . x)] in h ) by XBOOLE_0:def_3;
hence ( not h = f \/ g or h . x = g . x ) by FUNCT_1:1; ::_thesis: verum
end;
theorem :: GRFUNC_1:16
for x being set
for h, f, g being Function st x in dom h & h = f \/ g & not h . x = f . x holds
h . x = g . x
proof
let x be set ; ::_thesis: for h, f, g being Function st x in dom h & h = f \/ g & not h . x = f . x holds
h . x = g . x
let h, f, g be Function; ::_thesis: ( x in dom h & h = f \/ g & not h . x = f . x implies h . x = g . x )
assume x in dom h ; ::_thesis: ( not h = f \/ g or h . x = f . x or h . x = g . x )
then [x,(h . x)] in h by FUNCT_1:def_2;
then ( not h = f \/ g or [x,(h . x)] in f or [x,(h . x)] in g ) by XBOOLE_0:def_3;
hence ( not h = f \/ g or h . x = f . x or h . x = g . x ) by FUNCT_1:1; ::_thesis: verum
end;
theorem :: GRFUNC_1:17
for f, g, h being Function st f is one-to-one & g is one-to-one & h = f \/ g & rng f misses rng g holds
h is one-to-one
proof
let f, g, h be Function; ::_thesis: ( f is one-to-one & g is one-to-one & h = f \/ g & rng f misses rng g implies h is one-to-one )
assume that
A1: ( f is one-to-one & g is one-to-one ) and
A2: h = f \/ g and
A3: (rng f) /\ (rng g) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: h is one-to-one
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_h_&_x2_in_dom_h_&_h_._x1_=_h_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom h & x2 in dom h & h . x1 = h . x2 implies x1 = x2 )
assume that
A4: ( x1 in dom h & x2 in dom h ) and
A5: h . x1 = h . x2 ; ::_thesis: x1 = x2
A6: now__::_thesis:_(_(_(_x1_in_dom_f_&_x2_in_dom_g_)_or_(_x1_in_dom_g_&_x2_in_dom_f_)_)_implies_x1_=_x2_)
assume ( ( x1 in dom f & x2 in dom g ) or ( x1 in dom g & x2 in dom f ) ) ; ::_thesis: x1 = x2
then ( ( h . x1 = f . x1 & h . x2 = g . x2 & f . x1 <> g . x2 ) or ( h . x1 = g . x1 & h . x2 = f . x2 & f . x2 <> g . x1 ) ) by A2, A3, Lm1, Th15;
hence x1 = x2 by A5; ::_thesis: verum
end;
A7: ( x1 in dom g & x2 in dom g implies ( h . x1 = g . x1 & h . x2 = g . x2 ) ) by A2, Th15;
( x1 in dom f & x2 in dom f implies ( h . x1 = f . x1 & h . x2 = f . x2 ) ) by A2, Th15;
then ( ( ( x1 in dom f & x2 in dom f ) or ( x1 in dom g & x2 in dom g ) ) implies x1 = x2 ) by A1, A5, A7, FUNCT_1:def_4;
hence x1 = x2 by A2, A4, A6, Lm3; ::_thesis: verum
end;
hence h is one-to-one by FUNCT_1:def_4; ::_thesis: verum
end;
theorem :: GRFUNC_1:18
canceled;
theorem :: GRFUNC_1:19
canceled;
theorem :: GRFUNC_1:20
for f being Function st f is one-to-one holds
for x, y being set holds
( [y,x] in f " iff [x,y] in f )
proof
let f be Function; ::_thesis: ( f is one-to-one implies for x, y being set holds
( [y,x] in f " iff [x,y] in f ) )
assume A1: f is one-to-one ; ::_thesis: for x, y being set holds
( [y,x] in f " iff [x,y] in f )
let x, y be set ; ::_thesis: ( [y,x] in f " iff [x,y] in f )
dom (f ") = rng f by A1, FUNCT_1:33;
then ( y in dom (f ") & x = (f ") . y iff ( x in dom f & y = f . x ) ) by A1, FUNCT_1:32;
hence ( [y,x] in f " iff [x,y] in f ) by FUNCT_1:1; ::_thesis: verum
end;
theorem :: GRFUNC_1:21
for f being Function st f = {} holds
f " = {}
proof
let f be Function; ::_thesis: ( f = {} implies f " = {} )
assume f = {} ; ::_thesis: f " = {}
then dom (f ") = {} by FUNCT_1:33, RELAT_1:38;
hence f " = {} ; ::_thesis: verum
end;
theorem :: GRFUNC_1:22
for x, X being set
for f being Function holds
( ( x in dom f & x in X ) iff [x,(f . x)] in f | X )
proof
let x, X be set ; ::_thesis: for f being Function holds
( ( x in dom f & x in X ) iff [x,(f . x)] in f | X )
let f be Function; ::_thesis: ( ( x in dom f & x in X ) iff [x,(f . x)] in f | X )
( x in dom f iff [x,(f . x)] in f ) by FUNCT_1:def_2, XTUPLE_0:def_12;
hence ( ( x in dom f & x in X ) iff [x,(f . x)] in f | X ) by RELAT_1:def_11; ::_thesis: verum
end;
theorem Th23: :: GRFUNC_1:23
for g, f being Function st g c= f holds
f | (dom g) = g
proof
let g, f be Function; ::_thesis: ( g c= f implies f | (dom g) = g )
assume A1: g c= f ; ::_thesis: f | (dom g) = g
for x, y being set st [x,y] in f | (dom g) holds
[x,y] in g
proof
let x, y be set ; ::_thesis: ( [x,y] in f | (dom g) implies [x,y] in g )
assume A2: [x,y] in f | (dom g) ; ::_thesis: [x,y] in g
then x in dom g by RELAT_1:def_11;
then A3: [x,(g . x)] in g by FUNCT_1:def_2;
[x,y] in f by A2, RELAT_1:def_11;
hence [x,y] in g by A1, A3, FUNCT_1:def_1; ::_thesis: verum
end;
then A4: f | (dom g) c= g by RELAT_1:def_3;
g | (dom g) c= f | (dom g) by A1, RELAT_1:76;
then g c= f | (dom g) ;
hence f | (dom g) = g by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: GRFUNC_1:24
for x, Y being set
for f being Function holds
( ( x in dom f & f . x in Y ) iff [x,(f . x)] in Y |` f )
proof
let x, Y be set ; ::_thesis: for f being Function holds
( ( x in dom f & f . x in Y ) iff [x,(f . x)] in Y |` f )
let f be Function; ::_thesis: ( ( x in dom f & f . x in Y ) iff [x,(f . x)] in Y |` f )
( x in dom f iff [x,(f . x)] in f ) by FUNCT_1:def_2, XTUPLE_0:def_12;
hence ( ( x in dom f & f . x in Y ) iff [x,(f . x)] in Y |` f ) by RELAT_1:def_12; ::_thesis: verum
end;
theorem :: GRFUNC_1:25
for g, f being Function st g c= f & f is one-to-one holds
(rng g) |` f = g
proof
let g, f be Function; ::_thesis: ( g c= f & f is one-to-one implies (rng g) |` f = g )
assume A1: g c= f ; ::_thesis: ( not f is one-to-one or (rng g) |` f = g )
assume A2: f is one-to-one ; ::_thesis: (rng g) |` f = g
for x, y being set st [x,y] in (rng g) |` f holds
[x,y] in g
proof
let x, y be set ; ::_thesis: ( [x,y] in (rng g) |` f implies [x,y] in g )
assume A3: [x,y] in (rng g) |` f ; ::_thesis: [x,y] in g
then y in rng g by RELAT_1:def_12;
then A4: ex x1 being set st [x1,y] in g by XTUPLE_0:def_13;
[x,y] in f by A3, RELAT_1:def_12;
hence [x,y] in g by A1, A2, A4, Th9; ::_thesis: verum
end;
then A5: (rng g) |` f c= g by RELAT_1:def_3;
(rng g) |` g c= (rng g) |` f by A1, RELAT_1:101;
then g c= (rng g) |` f ;
hence (rng g) |` f = g by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: GRFUNC_1:26
for x, Y being set
for f being Function holds
( x in f " Y iff ( [x,(f . x)] in f & f . x in Y ) )
proof
let x, Y be set ; ::_thesis: for f being Function holds
( x in f " Y iff ( [x,(f . x)] in f & f . x in Y ) )
let f be Function; ::_thesis: ( x in f " Y iff ( [x,(f . x)] in f & f . x in Y ) )
thus ( x in f " Y implies ( [x,(f . x)] in f & f . x in Y ) ) ::_thesis: ( [x,(f . x)] in f & f . x in Y implies x in f " Y )
proof
assume x in f " Y ; ::_thesis: ( [x,(f . x)] in f & f . x in Y )
then ex y being set st
( [x,y] in f & y in Y ) by RELAT_1:def_14;
hence ( [x,(f . x)] in f & f . x in Y ) by FUNCT_1:1; ::_thesis: verum
end;
thus ( [x,(f . x)] in f & f . x in Y implies x in f " Y ) by RELAT_1:def_14; ::_thesis: verum
end;
begin
theorem :: GRFUNC_1:27
for X being set
for f, g being Function st X c= dom f & f c= g holds
f | X = g | X
proof
let X be set ; ::_thesis: for f, g being Function st X c= dom f & f c= g holds
f | X = g | X
let f, g be Function; ::_thesis: ( X c= dom f & f c= g implies f | X = g | X )
assume A1: X c= dom f ; ::_thesis: ( not f c= g or f | X = g | X )
assume f c= g ; ::_thesis: f | X = g | X
hence f | X = (g | (dom f)) | X by Th23
.= g | ((dom f) /\ X) by RELAT_1:71
.= g | X by A1, XBOOLE_1:28 ;
::_thesis: verum
end;
theorem Th28: :: GRFUNC_1:28
for f being Function
for x being set st x in dom f holds
f | {x} = {[x,(f . x)]}
proof
let f be Function; ::_thesis: for x being set st x in dom f holds
f | {x} = {[x,(f . x)]}
let x be set ; ::_thesis: ( x in dom f implies f | {x} = {[x,(f . x)]} )
assume A1: x in dom f ; ::_thesis: f | {x} = {[x,(f . x)]}
A2: x in {x} by TARSKI:def_1;
dom (f | {x}) = (dom f) /\ {x} by RELAT_1:61
.= {x} by A1, ZFMISC_1:46 ;
hence f | {x} = {[x,((f | {x}) . x)]} by Th7
.= {[x,(f . x)]} by A2, FUNCT_1:49 ;
::_thesis: verum
end;
theorem Th29: :: GRFUNC_1:29
for f, g being Function
for x being set st dom f = dom g & f . x = g . x holds
f | {x} = g | {x}
proof
let f, g be Function; ::_thesis: for x being set st dom f = dom g & f . x = g . x holds
f | {x} = g | {x}
let x be set ; ::_thesis: ( dom f = dom g & f . x = g . x implies f | {x} = g | {x} )
assume that
A1: dom f = dom g and
A2: f . x = g . x ; ::_thesis: f | {x} = g | {x}
percases ( x in dom f or not x in dom f ) ;
supposeA3: x in dom f ; ::_thesis: f | {x} = g | {x}
hence f | {x} = {[x,(g . x)]} by A2, Th28
.= g | {x} by A1, A3, Th28 ;
::_thesis: verum
end;
suppose not x in dom f ; ::_thesis: f | {x} = g | {x}
then A4: {x} misses dom f by ZFMISC_1:50;
hence f | {x} = {} by RELAT_1:66
.= g | {x} by A1, A4, RELAT_1:66 ;
::_thesis: verum
end;
end;
end;
theorem Th30: :: GRFUNC_1:30
for f, g being Function
for x, y being set st dom f = dom g & f . x = g . x & f . y = g . y holds
f | {x,y} = g | {x,y}
proof
let f, g be Function; ::_thesis: for x, y being set st dom f = dom g & f . x = g . x & f . y = g . y holds
f | {x,y} = g | {x,y}
let x, y be set ; ::_thesis: ( dom f = dom g & f . x = g . x & f . y = g . y implies f | {x,y} = g | {x,y} )
assume ( dom f = dom g & f . x = g . x & f . y = g . y ) ; ::_thesis: f | {x,y} = g | {x,y}
then A1: ( f | {x} = g | {x} & f | {y} = g | {y} ) by Th29;
{x,y} = {x} \/ {y} by ENUMSET1:1;
hence f | {x,y} = g | {x,y} by A1, RELAT_1:150; ::_thesis: verum
end;
theorem :: GRFUNC_1:31
for f, g being Function
for x, y, z being set st dom f = dom g & f . x = g . x & f . y = g . y & f . z = g . z holds
f | {x,y,z} = g | {x,y,z}
proof
let f, g be Function; ::_thesis: for x, y, z being set st dom f = dom g & f . x = g . x & f . y = g . y & f . z = g . z holds
f | {x,y,z} = g | {x,y,z}
let x, y, z be set ; ::_thesis: ( dom f = dom g & f . x = g . x & f . y = g . y & f . z = g . z implies f | {x,y,z} = g | {x,y,z} )
assume ( dom f = dom g & f . x = g . x & f . y = g . y & f . z = g . z ) ; ::_thesis: f | {x,y,z} = g | {x,y,z}
then A1: ( f | {x,y} = g | {x,y} & f | {z} = g | {z} ) by Th29, Th30;
{x,y,z} = {x,y} \/ {z} by ENUMSET1:3;
hence f | {x,y,z} = g | {x,y,z} by A1, RELAT_1:150; ::_thesis: verum
end;
registration
let f be Function;
let A be set ;
clusterf \ A -> Function-like ;
coherence
f \ A is Function-like ;
end;
theorem :: GRFUNC_1:32
for x being set
for f, g being Function st x in (dom f) \ (dom g) holds
(f \ g) . x = f . x
proof
let x be set ; ::_thesis: for f, g being Function st x in (dom f) \ (dom g) holds
(f \ g) . x = f . x
let f, g be Function; ::_thesis: ( x in (dom f) \ (dom g) implies (f \ g) . x = f . x )
assume A1: x in (dom f) \ (dom g) ; ::_thesis: (f \ g) . x = f . x
( f \ g c= f & (dom f) \ (dom g) c= dom (f \ g) ) by RELAT_1:3;
hence (f \ g) . x = f . x by A1, Th2; ::_thesis: verum
end;
theorem :: GRFUNC_1:33
for f, g, h being Function st f c= g & f c= h holds
g | (dom f) = h | (dom f)
proof
let f, g, h be Function; ::_thesis: ( f c= g & f c= h implies g | (dom f) = h | (dom f) )
assume that
A1: f c= g and
A2: f c= h ; ::_thesis: g | (dom f) = h | (dom f)
thus g | (dom f) = f by A1, Th23
.= h | (dom f) by A2, Th23 ; ::_thesis: verum
end;
registration
let f be Function;
let g be Subset of f;
cluster Relation-like Function-like g -compatible -> f -compatible for set ;
coherence
for b1 being Function st b1 is g -compatible holds
b1 is f -compatible
proof
let F be Function; ::_thesis: ( F is g -compatible implies F is f -compatible )
assume A1: F is g -compatible ; ::_thesis: F is f -compatible
let x be set ; :: according to FUNCT_1:def_14 ::_thesis: ( not x in proj1 F or F . x in f . x )
assume x in dom F ; ::_thesis: F . x in f . x
then A2: F . x in g . x by A1, FUNCT_1:def_14;
then x in dom g by FUNCT_1:def_2;
hence F . x in f . x by A2, Th2; ::_thesis: verum
end;
end;
theorem Th34: :: GRFUNC_1:34
for g, f being Function st g c= f holds
g = f | (dom g)
proof
let g, f be Function; ::_thesis: ( g c= f implies g = f | (dom g) )
assume A1: g c= f ; ::_thesis: g = f | (dom g)
then dom g c= dom f by RELAT_1:11;
hence dom g = dom (f | (dom g)) by RELAT_1:62; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in proj1 g or g . b1 = (f | (dom g)) . b1 )
let x be set ; ::_thesis: ( not x in proj1 g or g . x = (f | (dom g)) . x )
assume A2: x in dom g ; ::_thesis: g . x = (f | (dom g)) . x
hence g . x = f . x by A1, Th2
.= (f | (dom g)) . x by A2, FUNCT_1:49 ;
::_thesis: verum
end;
registration
let f be Function;
let g be f -compatible Function;
cluster -> f -compatible for Element of K10(g);
coherence
for b1 being Subset of g holds b1 is f -compatible
proof
let h be Subset of g; ::_thesis: h is f -compatible
h = g | (dom h) by Th34;
hence h is f -compatible ; ::_thesis: verum
end;
end;
theorem :: GRFUNC_1:35
for x, X being set
for g, f being Function st g c= f & x in X & X /\ (dom f) c= dom g holds
f . x = g . x
proof
let x, X be set ; ::_thesis: for g, f being Function st g c= f & x in X & X /\ (dom f) c= dom g holds
f . x = g . x
let g, f be Function; ::_thesis: ( g c= f & x in X & X /\ (dom f) c= dom g implies f . x = g . x )
assume that
A1: g c= f and
A2: x in X and
A3: X /\ (dom f) c= dom g ; ::_thesis: f . x = g . x
percases ( x in dom g or not x in dom g ) ;
suppose x in dom g ; ::_thesis: f . x = g . x
hence f . x = g . x by A1, Th2; ::_thesis: verum
end;
supposeA4: not x in dom g ; ::_thesis: f . x = g . x
then not x in X /\ (dom f) by A3;
then not x in dom f by A2, XBOOLE_0:def_4;
hence f . x = {} by FUNCT_1:def_2
.= g . x by A4, FUNCT_1:def_2 ;
::_thesis: verum
end;
end;
end;