:: Graphs of Functions
:: by Czes{\l}aw Byli\'nski
::
:: Received April 14, 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, TARSKI, RELAT_1, XBOOLE_0, SUBSET_1;
notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ENUMSET1, RELAT_1, FUNCT_1;
constructors TARSKI, SUBSET_1, FUNCT_1, ENUMSET1, XTUPLE_0;
registrations FUNCT_1, RELAT_1;
requirements SUBSET, BOOLE;
definitions RELAT_1, XBOOLE_0, FUNCT_1;
equalities XBOOLE_0;
expansions RELAT_1, FUNCT_1;
theorems TARSKI, XBOOLE_0, ZFMISC_1, FUNCT_1, RELAT_1, XBOOLE_1, ENUMSET1,
XTUPLE_0;
begin
reserve X,Y for set, p,x,x1,x2,y,y1,y2,z,z1,z2 for object;
reserve f,g,h for Function;
theorem Th1:
for G being set st G c= f holds G is Function;
theorem Th2:
f c= g iff dom f c= dom g &
for x being object st x in dom f holds f.x = g.x
proof
thus f c= g implies dom f c= dom g &
for x being object st x in dom f holds f.x = g.x
proof
assume
A1: f c= g;
hence dom f c= dom g by RELAT_1:11;
let x be object;
assume x in dom f;
then [x,f.x] in f by FUNCT_1:def 2;
hence thesis by A1,FUNCT_1:1;
end;
assume that
A2: dom f c= dom g and
A3: for x being object st x in dom f holds f.x = g.x;
let x,y be object;
assume
A4: [x,y] in f;
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 thesis by A2,A5,FUNCT_1:def 2;
end;
theorem
dom f = dom g & f c= g implies f = g
proof
assume that
A1: dom f = dom g and
A2: f c= g;
for x,y being object holds [x,y] in f iff [x,y] in g
proof let x,y be object;
thus [x,y] in f implies [x,y] in g by A2;
assume
A3: [x,y] in g;
then x in dom f by A1,XTUPLE_0:def 12;
then [x,f.x] in f by FUNCT_1:1;
hence thesis by A2,A3,FUNCT_1:def 1;
end;
hence thesis;
end;
Lm1: rng f /\ rng h = {} & x in dom f & y in dom h implies f.x <> h.y
proof
assume
A1: rng f /\ rng h = {};
assume x in dom f & y in dom h;
then f.x in rng f & h.y in rng h by FUNCT_1:def 3;
hence thesis by A1,XBOOLE_0:def 4;
end;
theorem
[x,z] in (g*f) implies [x,f.x] in f & [f.x,z] in g
proof
assume [x,z] in (g*f);
then ex y being object st [x,y] in f & [y,z] in g by RELAT_1:def 8;
hence thesis by FUNCT_1:1;
end;
theorem
{[x,y]} is Function;
Lm2: [x,y] in {[x1,y1]} implies x = x1 & y = y1
proof
assume [x,y] in {[x1,y1]};
then [x,y] = [x1,y1] by TARSKI:def 1;
hence thesis by XTUPLE_0:1;
end;
theorem
f = {[x,y]} implies f.x = y
proof
assume f = {[x,y]};
then [x,y] in f by TARSKI:def 1;
hence thesis by FUNCT_1:1;
end;
theorem Th7:
dom f = {x} implies f = {[x,f.x]}
proof
reconsider g = {[x,f.x]} as Function;
assume
A1: dom f = {x};
for y,z being object holds [y,z] in f iff [y,z] in g
proof let y,z be object;
thus [y,z] in f implies [y,z] in g
proof
assume
A2: [y,z] in f;
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 thesis by A3,TARSKI:def 1;
end;
assume [y,z] in g;
then
A5: y = x & z = f.x by Lm2;
x in dom f by A1,TARSKI:def 1;
hence thesis by A5,FUNCT_1:def 2;
end;
hence thesis;
end;
theorem
{[x1,y1],[x2,y2]} is Function iff (x1 = x2 implies y1 = y2)
proof
thus {[x1,y1],[x2,y2]} is Function & x1 = x2 implies y1 = y2
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;
hence thesis by A1,FUNCT_1:def 1;
end;
assume
A2: x1 = x2 implies y1 = y2;
now
thus p in {[x1,y1],[x2,y2]} implies ex x,y st [x,y] = p
proof
assume p in {[x1,y1],[x2,y2]};
then p = [x1,y1] or p = [x2,y2] by TARSKI:def 2;
hence thesis;
end;
let x,z1,z2;
A3: [x,z1] = [x1,y1] & [x,z2] = [x1,y1] or [x,z1] = [x2,y2] & [x,z2] = [
x2,y2] implies z1 = y1 & z2 = y1 or z1 = y2 & z2 = y2 by XTUPLE_0:1;
A4: now
assume
A5: [x,z1] = [x1,y1] & [x,z2] = [x2,y2] or [x,z1] = [x2,y2] & [x,z2
] = [x1,y1];
then x = x1 & x = x2 by XTUPLE_0:1;
hence z1 = z2 by A2,A5,XTUPLE_0:1;
end;
assume [x,z1] in {[x1,y1],[x2,y2]} & [x,z2] in {[x1,y1],[x2,y2]};
hence z1 = z2 by A3,A4,TARSKI:def 2;
end;
hence thesis by FUNCT_1:def 1;
end;
theorem Th9:
f is one-to-one iff for x1,x2,y st [x1,y] in f & [x2,y] in f holds x1 = x2
proof
thus f is one-to-one implies for x1,x2,y st [x1,y] in f & [x2,y] in f holds
x1 = x2
proof
assume
A1: f is one-to-one;
let x1,x2,y;
assume
A2: [x1,y] in f & [x2,y] in f;
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 thesis by A1,A3;
end;
assume
A4: for x1,x2,y st [x1,y] in f & [x2,y] in f holds x1 = x2;
let x1,x2;
assume x1 in dom f & x2 in dom f & f.x1 = f.x2;
then [x1,f.x1] in f & [x2,f.x1] in f by FUNCT_1:1;
hence thesis by A4;
end;
theorem Th10:
g c= f & f is one-to-one implies g is one-to-one
proof
assume g c= f & f is one-to-one;
then for x1,x2,y st [x1,y] in g & [x2,y] in g holds x1 = x2 by Th9;
hence thesis by Th9;
end;
registration
let f,X;
cluster f /\ X -> Function-like;
coherence by Th1,XBOOLE_1:17;
end;
theorem
x in dom(f /\ g) implies (f /\ g).x = f.x
proof
set y = (f /\ g).x;
assume x in dom(f /\ g);
then [x,y] in (f /\ g) by FUNCT_1:def 2;
then [x,y] in f by XBOOLE_0:def 4;
hence thesis by FUNCT_1:1;
end;
theorem
f is one-to-one implies f /\ g is one-to-one by Th10,XBOOLE_1:17;
theorem
dom f misses dom g implies f \/ g is Function
proof
assume
A1: dom f /\ dom g = {};
now
thus p in f \/ g implies ex x,y being object st [x,y] = p
by RELAT_1:def 1;
let x,y1,y2;
assume [x,y1] in f \/ g;
then
A2: [x,y1] in f or [x,y1] in g by XBOOLE_0:def 3;
assume [x,y2] in f \/ g;
then
A3: [x,y2] in f or [x,y2] in g by XBOOLE_0:def 3;
not (x in dom f & x in dom g) by A1,XBOOLE_0:def 4;
hence y1 = y2 by A2,A3,FUNCT_1:def 1,XTUPLE_0:def 12;
end;
hence thesis by FUNCT_1:def 1;
end;
theorem
f c= h & g c= h implies f \/ g is Function by Th1,XBOOLE_1:8;
Lm3: h = f \/ g implies (x in dom h iff x in dom f or x in dom g)
proof
assume
A1: h = f \/ g;
thus x in dom h implies x in dom f or x in dom g
proof
assume x in dom h;
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 thesis by XTUPLE_0:def 12;
end;
assume x in dom f or x in dom g;
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 thesis by XTUPLE_0:def 12;
end;
theorem Th15:
x in dom g & h = f \/ g implies h.x = g.x
proof
assume x in dom g;
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 thesis by FUNCT_1:1;
end;
theorem
x in dom h & h = f \/ g implies h.x = f.x or h.x = g.x
proof
assume x in dom h;
then [x,h.x] in h by FUNCT_1:def 2;
then h = f \/ g implies [x,h.x] in f or [x,h.x] in g by XBOOLE_0:def 3;
hence thesis by FUNCT_1:1;
end;
theorem
f is one-to-one & g is one-to-one & h = f \/ g & rng f misses rng g
implies h is one-to-one
proof
assume that
A1: f is one-to-one & g is one-to-one and
A2: h = f \/ g and
A3: rng f /\ rng g = {};
now
let x1,x2;
assume that
A4: x1 in dom h & x2 in dom h and
A5: h.x1 = h.x2;
A6: now
assume x1 in dom f & x2 in dom g or x1 in dom g & x2 in dom f;
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;
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;
hence x1 = x2 by A2,A4,A6,Lm3;
end;
hence thesis;
end;
::$CT 2
theorem
f is one-to-one implies for x,y holds [y,x] in f" iff [x,y] in f
proof
assume
A1: f is one-to-one;
let x,y;
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 thesis by FUNCT_1:1;
end;
theorem
f = {} implies f" = {}
proof
assume f = {};
then dom(f") = {} by FUNCT_1:33,RELAT_1:38;
hence thesis;
end;
theorem
x in dom f & x in X iff [x,f.x] in f|X
proof
x in dom f iff [x,f.x] in f by FUNCT_1:def 2,XTUPLE_0:def 12;
hence thesis by RELAT_1:def 11;
end;
theorem Th21:
g c= f implies f|dom g = g
proof
assume
A1: g c= f;
for x,y being object holds [x,y] in (f|dom g) implies [x,y] in g
proof let x,y be object;
assume
A2: [x,y] in (f|dom 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 thesis by A1,A3,FUNCT_1:def 1;
end;
then
A4: (f|dom g) c= g;
(g|dom g) c= (f|dom g) by A1,RELAT_1:76;
hence thesis by A4;
end;
theorem
x in dom f & f.x in Y iff [x,f.x] in Y|`f
proof
x in dom f iff [x,f.x] in f by FUNCT_1:def 2,XTUPLE_0:def 12;
hence thesis by RELAT_1:def 12;
end;
theorem
g c= f & f is one-to-one implies rng g|`f = g
proof
assume
A1: g c= f;
assume
A2: f is one-to-one;
for x,y being object holds [x,y] in (rng g|`f) implies [x,y] in g
proof let x,y be object;
assume
A3: [x,y] in (rng g|`f);
then y in rng g by RELAT_1:def 12;
then
A4: ex x1 being object st [x1,y] in g by XTUPLE_0:def 13;
[x,y] in f by A3,RELAT_1:def 12;
hence thesis by A1,A2,A4,Th9;
end;
then
A5: (rng g|`f) c= g;
(rng g|`g) c= (rng g|`f) by A1,RELAT_1:101;
hence thesis by A5;
end;
theorem
x in f"Y iff [x,f.x] in f & f.x in Y
proof
thus x in f"Y implies [x,f.x] in f & f.x in Y
proof
assume x in f"Y;
then ex y being object st [x,y] in f & y in Y by RELAT_1:def 14;
hence thesis by FUNCT_1:1;
end;
thus thesis by RELAT_1:def 14;
end;
begin :: Addenda
:: from HAHNBAN
theorem
for X being set, f,g being Function st X c= dom f & f c= g holds f|X = g|X
proof
let X be set, f,g be Function such that
A1: X c= dom f;
assume f c= g;
hence f|X = g|(dom f)|X by Th21
.= g|((dom f) /\ X) by RELAT_1:71
.= g|X by A1,XBOOLE_1:28;
end;
:: from AMI_3
theorem Th26:
for f being Function, x being object st x in dom f holds f|{x} = {[x,f.x]}
proof
let f be Function, x be object such that
A1: x in dom f;
A2: x in {x} by TARSKI:def 1;
dom(f|{x} qua Function) = 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;
end;
:: from AMI_3, 2007.06.14, A.T.
theorem Th27:
for f,g being Function, x being object st dom f = dom g & f.x = g.x
holds f|{x} = g|{x}
proof
let f,g be Function, x be object such that
A1: dom f = dom g and
A2: f.x = g.x;
per cases;
suppose
A3: x in dom f;
hence f|{x} = {[x,g.x]} by A2,Th26
.= g|{x} by A1,A3,Th26;
end;
suppose
not x in dom f;
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;
end;
end;
theorem Th28:
for f,g being Function, x,y being object
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, x,y be object;
assume dom f = dom g & f.x = g.x & f.y = g.y;
then
A1: f|{x} = g|{x} & f|{y} = g|{y} by Th27;
{x,y} = {x} \/ {y} by ENUMSET1:1;
hence thesis by A1,RELAT_1:150;
end;
theorem
for f,g being Function, x,y,z being object 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, x,y,z be object;
assume dom f = dom g & f.x = g.x & f.y = g.y & f.z = g.z;
then
A1: f|{x,y} = g|{x,y} & f|{z} = g|{z} by Th27,Th28;
{x,y,z} = {x,y} \/ {z} by ENUMSET1:3;
hence thesis by A1,RELAT_1:150;
end;
:: from AMISTD_2, 2007.07.26, A.T.
registration
let f be Function, A be set;
cluster f \ A -> Function-like;
coherence;
end;
theorem
for f,g being Function st x in dom f \ dom g holds (f \ g).x = f.x
proof
let f, g be Function such that
A1: x in dom f \ dom g;
f \ g c= f & dom f \ dom g c= dom (f \ g) by XTUPLE_0:25;
hence thesis by A1,Th2;
end;
:: missing, 2007.06.19, A.T.
theorem
f c= g & f c= h implies g|dom f = h|dom f
proof
assume that
A1: f c= g and
A2: f c= h;
thus g|dom f = f by A1,Th21
.= h|dom f by A2,Th21;
end;
:: new, 2009.09.30, A.T.
registration let f be Function, g be Subset of f;
cluster g-compatible -> f-compatible for Function;
coherence
proof let F be Function such that
A1: F is g-compatible;
let x;
assume x in dom F;
then
A2: F.x in g.x by A1;
then x in dom g by FUNCT_1:def 2;
hence F.x in f.x by A2,Th2;
end;
end;
:: 2009.10.17, A.T.
theorem Th32:
g c= f implies g = f|dom g
proof
assume
A1: g c= f;
then dom g c= dom f by RELAT_1:11;
hence dom g = dom(f|dom g) by RELAT_1:62;
let x;
assume
A2: x in dom g;
hence g.x = f.x by A1,Th2
.= (f|dom g).x by A2,FUNCT_1:49;
end;
registration
let f be Function, g be f-compatible Function;
cluster -> f-compatible for Subset of g;
coherence
proof let h be Subset of g;
h = g|dom h by Th32;
hence thesis;
end;
end;
theorem
g c= f & x in X & X /\ dom f c= dom g implies f.x = g.x
proof assume that
A1: g c= f and
A2: x in X and
A3: X /\ dom f c= dom g;
per cases;
suppose x in dom g;
hence f.x = g.x by A1,Th2;
end;
suppose
A4: not x in dom g;
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;
end;
end;