:: About Graph Mappings
:: by Sebastian Koch
::
:: Received August 29, 2019
:: Copyright (c) 2019-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 NUMBERS, RELAT_1, FUNCT_1, TARSKI, CARD_1, XBOOLE_0, GLIB_000,
PARTFUN1, ZFMISC_1, FUNCOP_1, ALGSTR_0, FUNCT_2, GLIB_009, MOD_4,
WAYBEL_0, RING_3, ORDINAL2, CHORD, CARD_2, SCMYCIEL, GLIB_010, GLIB_011;
notations TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1,
FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1,
SETWISEO, EQREL_1, FUNCOP_1, FUNCT_4, PARTFUN2, CARD_1, PBOOLE, CARD_2,
CARD_3, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, VALUED_0, FINSEQ_1,
BSPACE, GLIB_000, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_6,
GLIB_001, CHORD, GLIB_008, GLIB_009, GLIB_010;
constructors DOMAIN_1, FUNCT_4, XXREAL_0, NAT_1, NAT_D, BINOP_2, CARD_2,
FINSEQ_4, PBOOLE, ORDINAL3, WELLORD2, PARTFUN1, RELSET_1, GLIB_000,
STRUCT_0, RELAT_1, FUNCT_1, FUNCT_2, ALGSTR_0, GROUP_1, GLIB_001, ABIAN,
CARD_3, FINSEQ_1, GLIB_002, GLIB_003, SETFAM_1, EQREL_1, GROUP_2,
GROUP_6, GLIB_006, GLIB_007, PARTFUN2, BSPACE, SETWISEO, CHORD, RAT_1,
GLIB_008, GLIB_009, GLIB_010, FUNCT_7;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, GLIB_000,
CARD_1, FUNCT_2, PARTFUN1, RELSET_1, XTUPLE_0, GLIB_006, GLIB_008,
GLIB_009, GLIB_010, FUNCT_7;
requirements BOOLE, SUBSET;
theorems TARSKI, XBOOLE_0, ZFMISC_1, XBOOLE_1, CARD_1, CARD_2, RELAT_1,
RELSET_1, FUNCT_1, FUNCT_2, FUNCOP_1, PARTFUN1, GLIB_000, CHORD,
GLIB_009, GLIB_010;
schemes FUNCT_1;
begin :: Vertex Mappings
definition
let G1, G2 be _Graph;
mode PVertexMapping of G1, G2 ->
PartFunc of the_Vertices_of G1, the_Vertices_of G2 means
:Def1:
for v,w being Vertex of G1
st v in dom it & w in dom it & v,w are_adjacent
holds it/.v, it/.w are_adjacent;
existence
proof
take the empty PartFunc of the_Vertices_of G1, the_Vertices_of G2;
thus thesis;
end;
end;
theorem Th1:
for G1, G2 being _Graph
for f being PartFunc of the_Vertices_of G1, the_Vertices_of G2
holds f is PVertexMapping of G1, G2 iff
for v,w,e being object st v in dom f & w in dom f & e Joins v,w,G1
ex e9 being object st e9 Joins f.v,f.w,G2
proof
let G1, G2 be _Graph;
let f be PartFunc of the_Vertices_of G1, the_Vertices_of G2;
hereby
assume A1: f is PVertexMapping of G1, G2;
let v,w,e be object;
assume A2: v in dom f & w in dom f & e Joins v,w,G1;
then reconsider v0 = v, w0 = w as Vertex of G1;
v0, w0 are_adjacent by A2, CHORD:def 3;
then consider e9 being object such that
A3: e9 Joins f/.v0, f/.w0, G2 by A1, A2, Def1, CHORD:def 3;
take e9;
f/.v0 = f.v & f/.w0 = f.w by A2, PARTFUN1:def 6;
hence e9 Joins f.v,f.w,G2 by A3;
end;
assume A4: for v,w,e being object st v in dom f & w in dom f & e Joins v,w,G1
ex e9 being object st e9 Joins f.v,f.w,G2;
let v,w be Vertex of G1;
assume A5: v in dom f & w in dom f;
assume v,w are_adjacent;
then consider e being object such that
A6: e Joins v,w,G1 by CHORD:def 3;
consider e9 being object such that
A7: e9 Joins f.v,f.w,G2 by A4, A5, A6;
f/.v = f.v & f/.w = f.w by A5, PARTFUN1:def 6;
hence thesis by A7, CHORD:def 3;
end;
definition
let G1, G2 be _Graph, f be PVertexMapping of G1, G2;
attr f is directed means
:Def2:
for v,w,e being object st v in dom f & w in dom f & e DJoins v,w,G1
ex e9 being object st e9 DJoins f.v,f.w,G2;
attr f is continuous means
for v,w being Vertex of G1
st v in dom f & w in dom f & f/.v, f/.w are_adjacent
holds v, w are_adjacent;
attr f is Dcontinuous means
:Def4:
for v,w,e9 being object st v in dom f & w in dom f & e9 DJoins f.v,f.w,G2
ex e being object st e DJoins v,w,G1;
end;
theorem Th2:
for G1, G2 being _Graph, f being PVertexMapping of G1, G2
holds f is continuous iff
for v,w,e9 being object st v in dom f & w in dom f & e9 Joins f.v,f.w,G2
ex e being object st e Joins v,w,G1
proof
let G1, G2 be _Graph;
let f be PVertexMapping of G1, G2;
hereby
assume A1: f is continuous;
let v,w,e9 be object;
assume A2: v in dom f & w in dom f & e9 Joins f.v,f.w,G2;
then reconsider v0 = v, w0 = w as Vertex of G1;
f/.v0 = f.v & f/.w0 = f.w by A2, PARTFUN1:def 6;
then f/.v0, f/.w0 are_adjacent by A2, CHORD:def 3;
then consider e being object such that
A3: e Joins v0, w0, G1 by A1, A2, CHORD:def 3;
take e;
thus e Joins v,w,G1 by A3;
end;
assume A4: for v,w,e9 being object
st v in dom f & w in dom f & e9 Joins f.v,f.w,G2
ex e being object st e Joins v,w,G1;
let v,w be Vertex of G1;
assume A5: v in dom f & w in dom f;
assume f/.v,f/.w are_adjacent;
then consider e9 being object such that
A6: e9 Joins f/.v,f/.w,G2 by CHORD:def 3;
f/.v = f.v & f/.w = f.w by A5, PARTFUN1:def 6;
then consider e being object such that
A7: e Joins v,w,G1 by A4, A5, A6;
thus thesis by A7, CHORD:def 3;
end;
theorem
for G1, G2 being _Graph, f being PVertexMapping of G1, G2
holds f is continuous iff
for v,w being Vertex of G1 st v in dom f & w in dom f
holds v, w are_adjacent iff f/.v, f/.w are_adjacent by Def1;
registration
let G1, G2 be _Graph;
cluster Dcontinuous -> continuous for PVertexMapping of G1, G2;
coherence
proof
let f be PVertexMapping of G1, G2;
assume A1: f is Dcontinuous;
now
let v,w,e9 be object;
assume A2: v in dom f & w in dom f & e9 Joins f.v,f.w,G2;
then per cases by GLIB_000:16;
suppose e9 DJoins f.v,f.w,G2;
then consider e being object such that
A3: e DJoins v,w,G1 by A1, A2;
take e;
thus e Joins v,w,G1 by A3, GLIB_000:16;
end;
suppose e9 DJoins f.w,f.v,G2;
then consider e being object such that
A4: e DJoins w,v,G1 by A1, A2;
take e;
thus e Joins v,w,G1 by A4, GLIB_000:16;
end;
end;
hence thesis by Th2;
end;
cluster empty -> one-to-one Dcontinuous directed continuous
for PVertexMapping of G1, G2;
coherence;
cluster total -> non empty for PVertexMapping of G1, G2;
coherence;
cluster onto -> non empty for PVertexMapping of G1, G2;
coherence
proof
let f be PVertexMapping of G1, G2;
assume f is onto;
then rng f = the_Vertices_of G2 by FUNCT_2:def 3;
hence thesis;
end;
end;
registration
let G1 be simple _Graph, G2 be _Graph;
cluster Dcontinuous -> directed for PVertexMapping of G1, G2;
coherence
proof
let f be PVertexMapping of G1, G2;
assume A1: f is Dcontinuous;
let v,w,e be object;
assume A2: v in dom f & w in dom f & e DJoins v,w,G1;
then A3: e Joins v,w,G1 by GLIB_000:16;
then consider e9 being object such that
A4: e9 Joins f.v,f.w,G2 by A2, Th1;
take e9;
assume not e9 DJoins f.v,f.w,G2;
then e9 DJoins f.w,f.v,G2 by A4, GLIB_000:16;
then consider e0 being object such that
A5: e0 DJoins w,v,G1 by A1, A2;
e0 Joins v,w,G1 by A5, GLIB_000:16;
then e = e0 by A3, GLIB_000:def 20;
then (the_Source_of G1).e = w by A5, GLIB_000:def 14;
then v = w by A2, GLIB_000:def 14;
hence contradiction by A3, GLIB_000:18;
end;
end;
registration
let G1 be _Graph, G2 be simple _Graph;
cluster directed continuous -> Dcontinuous for PVertexMapping of G1, G2;
coherence
proof
let f be PVertexMapping of G1, G2;
assume A1: f is directed continuous;
let v,w,e9 be object;
assume A2: v in dom f & w in dom f & e9 DJoins f.v,f.w,G2;
then A3: e9 Joins f.v,f.w,G2 by GLIB_000:16;
then consider e being object such that
A4: e Joins v,w,G1 by A1, A2, Th2;
take e;
assume not e DJoins v,w,G1;
then e DJoins w,v,G1 by A4, GLIB_000:16;
then consider e0 being object such that
A5: e0 DJoins f.w,f.v,G2 by A1, A2;
e0 Joins f.v,f.w,G2 by A5, GLIB_000:16;
then e0 = e9 by A3, GLIB_000:def 20;
then (the_Source_of G2).e9 = f.w by A5, GLIB_000:def 14;
then f.w = f.v by A2, GLIB_000:def 14;
hence contradiction by A3, GLIB_000:18;
end;
end;
registration
let G1 be _trivial _Graph, G2 be _Graph;
cluster -> directed for PVertexMapping of G1, G2;
coherence
proof
let f be PVertexMapping of G1, G2;
consider v0 being Vertex of G1 such that
A1: the_Vertices_of G1 = {v0} by GLIB_000:22;
let v,w,e be object;
assume A2: v in dom f & w in dom f & e DJoins v,w,G1;
then e Joins v,w,G1 by GLIB_000:16;
then consider e9 being object such that
A3: e9 Joins f.v,f.w,G2 by A2, Th1;
take e9;
v = v0 & w = v0 by A1, A2, TARSKI:def 1;
hence e9 DJoins f.v,f.w,G2 by A3, GLIB_000:16;
end;
cluster continuous -> Dcontinuous for PVertexMapping of G1, G2;
coherence
proof
let f be PVertexMapping of G1, G2;
assume A4: f is continuous;
consider v0 being Vertex of G1 such that
A5: the_Vertices_of G1 = {v0} by GLIB_000:22;
let v,w,e9 be object;
assume A6: v in dom f & w in dom f & e9 DJoins f.v,f.w,G2;
then e9 Joins f.v,f.w,G2 by GLIB_000:16;
then consider e being object such that
A7: e Joins v,w,G1 by A4, A6, Th2;
take e;
v = v0 & w = v0 by A5, A6, TARSKI:def 1;
hence e DJoins v,w,G1 by A7, GLIB_000:16;
end;
cluster non empty -> total for PVertexMapping of G1, G2;
coherence
proof
let f be PVertexMapping of G1, G2;
assume A8: f is non empty;
consider v being Vertex of G1 such that
A9: the_Vertices_of G1 = {v} by GLIB_000:22;
dom f = the_Vertices_of G1 by A8, A9, ZFMISC_1:33;
hence thesis by PARTFUN1:def 2;
end;
end;
registration
let G1 be _Graph, G2 be _trivial _Graph;
cluster non empty -> onto for PVertexMapping of G1, G2;
coherence
proof
let f be PVertexMapping of G1, G2;
assume A1: f is non empty;
consider v being Vertex of G2 such that
A2: the_Vertices_of G2 = {v} by GLIB_000:22;
rng f = the_Vertices_of G2 by A1, A2, ZFMISC_1:33;
hence thesis by FUNCT_2:def 3;
end;
end;
registration
let G1 be _Graph, G2 be _trivial loopless _Graph;
cluster -> Dcontinuous continuous for PVertexMapping of G1, G2;
coherence
proof
let f be PVertexMapping of G1, G2;
consider v0 being Vertex of G2 such that
A1: the_Vertices_of G2 = {v0} by GLIB_000:22;
now
let v,w,e9 be object;
assume A2: v in dom f & w in dom f & e9 DJoins f.v,f.w,G2;
then f.v in rng f & f.w in rng f by FUNCT_1:3;
then f.v = v0 & f.w = v0 by A1, TARSKI:def 1;
then e9 Joins v0,v0,G2 by A2, GLIB_000:16; :: hence by contradiction
hence ex e being object st e DJoins v,w,G1 by GLIB_000:18;
end;
hence f is Dcontinuous;
hence f is continuous;
end;
end;
registration
let G1, G2 be _Graph;
cluster empty one-to-one directed continuous Dcontinuous
for PVertexMapping of G1, G2;
existence
proof
set f = the empty PartFunc of the_Vertices_of G1, the_Vertices_of G2;
for v, w being Vertex of G1 st v in dom f & w in dom f & v,w are_adjacent
holds f/.v, f/.w are_adjacent;
then reconsider f as PVertexMapping of G1, G2 by Def1;
take f;
thus thesis;
end;
end;
theorem
for G1, G2 being _Graph
for f being PartFunc of the_Vertices_of G1, the_Vertices_of G2
holds f is directed PVertexMapping of G1, G2 iff
for v,w,e being object st v in dom f & w in dom f & e DJoins v,w,G1
ex e9 being object st e9 DJoins f.v,f.w,G2
proof
let G1, G2 be _Graph;
let f be PartFunc of the_Vertices_of G1, the_Vertices_of G2;
thus f is directed PVertexMapping of G1, G2
implies for v,w,e being object st v in dom f & w in dom f & e DJoins v,w,G1
ex e9 being object st e9 DJoins f.v,f.w,G2 by Def2;
assume A1: for v,w,e being object
st v in dom f & w in dom f & e DJoins v,w,G1
ex e9 being object st e9 DJoins f.v,f.w,G2;
now
let v,w,e be object;
assume A2: v in dom f & w in dom f & e Joins v,w,G1;
then per cases by GLIB_000:16;
suppose e DJoins v,w,G1;
then consider e9 being object such that
A3: e9 DJoins f.v,f.w,G2 by A1, A2;
take e9;
thus e9 Joins f.v,f.w,G2 by A3, GLIB_000:16;
end;
suppose e DJoins w,v,G1;
then consider e9 being object such that
A4: e9 DJoins f.w,f.v,G2 by A1, A2;
take e9;
thus e9 Joins f.v,f.w,G2 by A4, GLIB_000:16;
end;
end;
hence thesis by A1, Th1, Def2;
end;
registration
let G1 be loopless _Graph, G2 be _Graph;
cluster non empty one-to-one directed for PVertexMapping of G1, G2;
existence
proof
set v1 = the Vertex of G1, v2 = the Vertex of G2;
set f = v1 .--> v2;
f = {v1} --> v2 by FUNCOP_1:def 9;
then reconsider f
as one-to-one PartFunc of the_Vertices_of G1, the_Vertices_of G2;
now
let v,w be Vertex of G1;
assume A1: v in dom f & w in dom f & v,w are_adjacent;
then v = v1 & w = v1 by FUNCOP_1:75;
hence f/.v,f/.w are_adjacent by A1, GLIB_009:39; :: by contradiction
end;
then reconsider f as PVertexMapping of G1, G2 by Def1;
take f;
thus f is non empty one-to-one;
thus f is directed
proof
let v,w,e be object;
assume A2: v in dom f & w in dom f & e DJoins v,w,G1;
then v = v1 & w = v1 by FUNCOP_1:75;
then e Joins v1,v1,G1 by A2, GLIB_000:16;
hence thesis by GLIB_000:18; :: by contradiction
end;
end;
end;
registration
let G1, G2 be loopless _Graph;
cluster non empty one-to-one directed continuous Dcontinuous
for PVertexMapping of G1, G2;
existence
proof
set v1 = the Vertex of G1, v2 = the Vertex of G2;
set f = v1 .--> v2;
f = {v1} --> v2 by FUNCOP_1:def 9;
then reconsider f
as one-to-one PartFunc of the_Vertices_of G1, the_Vertices_of G2;
now
let v,w be Vertex of G1;
assume A1: v in dom f & w in dom f & v,w are_adjacent;
then v = v1 & w = v1 by FUNCOP_1:75;
hence f/.v,f/.w are_adjacent by A1, GLIB_009:39; :: by contradiction
end;
then reconsider f as PVertexMapping of G1, G2 by Def1;
take f;
thus f is non empty one-to-one;
thus f is directed
proof
let v,w,e be object;
assume A2: v in dom f & w in dom f & e DJoins v,w,G1;
then v = v1 & w = v1 by FUNCOP_1:75;
then e Joins v1,v1,G1 by A2, GLIB_000:16;
hence thesis by GLIB_000:18; :: by contradiction
end;
thus f is continuous
proof
let v,w be Vertex of G1;
assume A3: v in dom f & w in dom f & f/.v,f/.w are_adjacent;
then v = v1 & w = v1 by FUNCOP_1:75;
hence v,w are_adjacent by A3, GLIB_009:39; :: by contradiction
end;
thus f is Dcontinuous
proof
let v,w,e9 be object;
assume A4: v in dom f & w in dom f & e9 DJoins f.v,f.w,G2;
then v = v1 & w = v1 by FUNCOP_1:75;
then e9 Joins f.v1,f.v1,G2 by A4, GLIB_000:16;
hence thesis by GLIB_000:18; :: by contradiction
end;
end;
end;
registration
let G1, G2 be non loopless _Graph;
cluster non empty one-to-one directed continuous Dcontinuous
for PVertexMapping of G1, G2;
existence
proof
consider v1 being object such that
A1: ex e1 being object st e1 Joins v1,v1,G1 by GLIB_000:18;
reconsider v1 as Vertex of G1 by A1, GLIB_000:13;
consider v2 being object such that
A2: ex e2 being object st e2 Joins v2,v2,G2 by GLIB_000:18;
reconsider v2 as Vertex of G2 by A2, GLIB_000:13;
set f = v1 .--> v2;
f = {v1} --> v2 by FUNCOP_1:def 9;
then reconsider f
as one-to-one PartFunc of the_Vertices_of G1, the_Vertices_of G2;
now
let v,w be Vertex of G1;
assume A3: v in dom f & w in dom f & v,w are_adjacent;
then v = v1 & w = v1 by FUNCOP_1:75;
then f/.v = f.v1 & f/.w = f.v1 by A3, PARTFUN1:def 6;
then f/.v = v2 & f/.w = v2 by FUNCOP_1:72;
hence f/.v,f/.w are_adjacent by A2, CHORD:def 3;
end;
then reconsider f as PVertexMapping of G1, G2 by Def1;
take f;
thus f is non empty one-to-one;
thus f is directed
proof
let v,w,e be object;
assume v in dom f & w in dom f & e DJoins v,w,G1;
then v = v1 & w = v1 by FUNCOP_1:75;
then A4: f.v = v2 & f.w = v2 by FUNCOP_1:72;
then consider e2 being object such that
A5: e2 Joins f.v,f.w,G2 by A2;
take e2;
thus thesis by A4, A5, GLIB_000:16;
end;
thus f is continuous
proof
let v,w be Vertex of G1;
assume v in dom f & w in dom f & f/.v,f/.w are_adjacent;
then v = v1 & w = v1 by FUNCOP_1:75;
hence v,w are_adjacent by A1, CHORD:def 3;
end;
thus f is Dcontinuous
proof
let v,w,e9 be object;
assume v in dom f & w in dom f & e9 DJoins f.v,f.w,G2;
then A6: v = v1 & w = v1 by FUNCOP_1:75;
then consider e1 being object such that
A7: e1 Joins v,w,G1 by A1;
take e1;
thus thesis by A6, A7, GLIB_000:16;
end;
end;
end;
theorem Th5:
for G being _Graph holds id the_Vertices_of G is
directed continuous Dcontinuous PVertexMapping of G, G
proof
let G be _Graph;
set f = id the_Vertices_of G;
A1: now
let v,w,e be object;
assume A2: v in dom f & w in dom f & e Joins v,w,G;
take e;
e Joins v,f.w,G by A2, FUNCT_1:18;
hence e Joins f.v,f.w,G by A2, FUNCT_1:18;
end;
A3: now
let v,w,e be object;
assume A4: v in dom f & w in dom f & e DJoins v,w,G;
take e;
e DJoins v,f.w,G by A4, FUNCT_1:18;
hence e DJoins f.v,f.w,G by A4, FUNCT_1:18;
end;
A5: now
let v,w,e be object;
assume A6: v in dom f & w in dom f & e Joins f.v,f.w,G;
take e;
e Joins v,f.w,G by A6, FUNCT_1:18;
hence e Joins v,w,G by A6, FUNCT_1:18;
end;
now
let v,w,e be object;
assume A7: v in dom f & w in dom f & e DJoins f.v,f.w,G;
take e;
e DJoins v,f.w,G by A7, FUNCT_1:18;
hence e DJoins v,w,G by A7, FUNCT_1:18;
end;
hence thesis by A1, A3, A5, Th1, Th2, Def2, Def4;
end;
theorem
for G1, G2 being _Graph, f being PVertexMapping of G1, G2
st f is total holds
(G2 is loopless implies G1 is loopless) &
(G2 is edgeless implies G1 is edgeless)
proof
let G1, G2 be _Graph, f be PVertexMapping of G1, G2;
assume A1: f is total;
hereby
assume A2: G2 is loopless;
assume not G1 is loopless;
then consider v being object such that
A3: ex e being object st e Joins v,v,G1 by GLIB_000:18;
consider e being object such that
A4: e Joins v,v,G1 by A3;
v in the_Vertices_of G1 by A4, GLIB_000:13;
then v in dom f by A1, PARTFUN1:def 2;
then consider e9 being object such that
A5: e9 Joins f.v,f.v,G2 by A4, Th1;
thus contradiction by A2, A5, GLIB_000:18;
end;
hereby
assume A6: G2 is edgeless;
assume not G1 is edgeless;
then consider e being object such that
A7: e in the_Edges_of G1 by XBOOLE_0:def 1;
set v = (the_Source_of G1).e, w = (the_Target_of G1).e;
A8: e Joins v,w,G1 by A7, GLIB_000:def 13;
then v in the_Vertices_of G1 & w in the_Vertices_of G1 by GLIB_000:13;
then v in dom f & w in dom f by A1, FUNCT_2:def 1;
then consider e9 being object such that
A9: e9 Joins f.v,f.w,G2 by A8, Th1;
e9 in the_Edges_of G2 by A9, GLIB_000:def 13;
hence contradiction by A6;
end;
end;
theorem
for G1, G2 being _Graph, f being continuous PVertexMapping of G1, G2
st f is onto holds
(G1 is loopless implies G2 is loopless) &
(G1 is edgeless implies G2 is edgeless)
proof
let G1, G2 be _Graph, f be continuous PVertexMapping of G1, G2;
assume A1: f is onto;
hereby
assume A2: G1 is loopless;
assume not G2 is loopless;
then consider v being object such that
A3: ex e being object st e Joins v,v,G2 by GLIB_000:18;
consider e being object such that
A4: e Joins v,v,G2 by A3;
v in the_Vertices_of G2 by A4, GLIB_000:13;
then v in rng f by A1, FUNCT_2:def 3;
then consider v0 being object such that
A5: v0 in dom f & f.v0 = v by FUNCT_1:def 3;
consider e0 being object such that
A6: e0 Joins v0,v0,G1 by A4, A5, Th2;
thus contradiction by A2, A6, GLIB_000:18;
end;
hereby
assume A7: G1 is edgeless;
assume not G2 is edgeless;
then consider e9 being object such that
A8: e9 in the_Edges_of G2 by XBOOLE_0:def 1;
set v = (the_Source_of G2).e9, w = (the_Target_of G2).e9;
A9: e9 Joins v,w,G2 by A8, GLIB_000:def 13;
then v in the_Vertices_of G2 & w in the_Vertices_of G2 by GLIB_000:13;
then A10: v in rng f & w in rng f by A1, FUNCT_2:def 3;
then consider v0 being object such that
A11: v0 in dom f & f.v0 = v by FUNCT_1:def 3;
consider w0 being object such that
A12: w0 in dom f & f.w0 = w by A10, FUNCT_1:def 3;
consider e being object such that
A13: e Joins v0,w0,G1 by A9, A11, A12, Th2;
e in the_Edges_of G1 by A13, GLIB_000:def 13;
hence contradiction by A7;
end;
end;
definition
let G1, G2 be _Graph, f be PVertexMapping of G1, G2;
attr f is isomorphism means
f is total one-to-one onto &
for v,w being Vertex of G1
holds card G1.edgesBetween({v},{w}) = card G2.edgesBetween({f.v},{f.w});
attr f is Disomorphism means
f is total one-to-one onto &
for v,w being Vertex of G1
holds card G1.edgesDBetween({v},{w}) = card G2.edgesDBetween({f.v},{f.w}) &
card G1.edgesDBetween({w},{v}) = card G2.edgesDBetween({f.w},{f.v});
end;
registration
let G1, G2 be _Graph;
cluster isomorphism -> total one-to-one onto continuous
for PVertexMapping of G1, G2;
coherence
proof
let f be PVertexMapping of G1, G2;
assume A1: f is isomorphism;
hence f is total one-to-one onto;
now
let v,w,e9 be object;
assume A2: v in dom f & w in dom f & e9 Joins f.v,f.w,G2;
then reconsider v0 = v, w0 = w as Vertex of G1;
f.v in {f.v} & f.w in {f.w} by TARSKI:def 1;
then e9 SJoins {f.v},{f.w},G2 by A2, GLIB_000:17;
then e9 in G2.edgesBetween({f.v},{f.w}) by GLIB_000:def 30;
then card G2.edgesBetween({f.v0},{f.w0}) <> 0;
then card G1.edgesBetween({v0},{w0}) <> 0 by A1;
then G1.edgesBetween({v0},{w0}) <> {};
then consider e being object such that
A3: e in G1.edgesBetween({v0},{w0}) by XBOOLE_0:def 1;
take e;
e SJoins {v},{w},G1 by A3, GLIB_000:def 30;
then e in the_Edges_of G1 &
((the_Source_of G1).e in {v} & (the_Target_of G1).e in {w} or
(the_Source_of G1).e in {w} & (the_Target_of G1).e in {v})
by GLIB_000:def 15;
then e in the_Edges_of G1 &
((the_Source_of G1).e = v & (the_Target_of G1).e = w or
(the_Source_of G1).e = w & (the_Target_of G1).e = v) by TARSKI:def 1;
hence e Joins v,w,G1 by GLIB_000:def 13;
end;
hence thesis by Th2;
end;
cluster Disomorphism -> total one-to-one onto isomorphism
continuous directed Dcontinuous for PVertexMapping of G1, G2;
coherence
proof
let f be PVertexMapping of G1, G2;
assume A4: f is Disomorphism;
hence f is total one-to-one onto;
now
let v,w be Vertex of G1;
per cases;
suppose A5: v <> w;
then A6: f.v <> f.w by A4, FUNCT_2:19;
thus card G1.edgesBetween({v},{w})
= card (G1.edgesDBetween({v},{w}) \/ G1.edgesDBetween({w},{v}))
by A5, GLIB_000:133
.= card G1.edgesDBetween({v},{w}) +` card G1.edgesDBetween({w},{v})
by A5, GLIB_000:133, CARD_2:35
.= card G1.edgesDBetween({v},{w})
+` card G2.edgesDBetween({f.w},{f.v}) by A4
.= card G2.edgesDBetween({f.v},{f.w})
+` card G2.edgesDBetween({f.w},{f.v}) by A4
.= card (G2.edgesDBetween({f.v},{f.w})
\/ G2.edgesDBetween({f.w},{f.v})) by A6, GLIB_000:133, CARD_2:35
.= card G2.edgesBetween({f.v},{f.w}) by A6, GLIB_000:133;
end;
suppose A7: v = w;
thus card G1.edgesBetween({v},{w})
= card G1.edgesDBetween({v},{w}) by A7, GLIB_000:134
.= card G2.edgesDBetween({f.v},{f.w}) by A4
.= card G2.edgesBetween({f.v},{f.w}) by A7, GLIB_000:134;
end;
end;
hence f is isomorphism by A4;
hence f is continuous;
now
let v,w,e be object;
assume A8: v in dom f & w in dom f & e DJoins v,w,G1;
then reconsider v0 = v, w0 = w as Vertex of G1;
v in {v} & w in {w} by TARSKI:def 1;
then e DSJoins {v},{w},G1 by A8, GLIB_000:126;
then e in G1.edgesDBetween({v},{w}) by GLIB_000:def 31;
then card G1.edgesDBetween({v0},{w0}) <> 0;
then card G2.edgesDBetween({f.v0},{f.w0}) <> 0 by A4;
then G2.edgesDBetween({f.v},{f.w}) <> {};
then consider e9 being object such that
A9: e9 in G2.edgesDBetween({f.v},{f.w}) by XBOOLE_0:def 1;
take e9;
e9 DSJoins {f.v},{f.w},G2 by A9, GLIB_000:def 31;
then e9 in the_Edges_of G2 & (the_Source_of G2).e9 in {f.v} &
(the_Target_of G2).e9 in {f.w} by GLIB_000:def 16;
then e9 in the_Edges_of G2 & (the_Source_of G2).e9 = f.v &
(the_Target_of G2).e9 = f.w by TARSKI:def 1;
hence e9 DJoins f.v,f.w,G2 by GLIB_000:def 14;
end;
hence f is directed;
now
let v,w,e9 be object;
assume A10: v in dom f & w in dom f & e9 DJoins f.v,f.w,G2;
then reconsider v0 = v, w0 = w as Vertex of G1;
f.v in {f.v} & f.w in {f.w} by TARSKI:def 1;
then e9 DSJoins {f.v},{f.w},G2 by A10, GLIB_000:126;
then e9 in G2.edgesDBetween({f.v},{f.w}) by GLIB_000:def 31;
then card G2.edgesDBetween({f.v0},{f.w0}) <> 0;
then card G1.edgesDBetween({v0},{w0}) <> 0 by A4;
then G1.edgesDBetween({v},{w}) <> {};
then consider e being object such that
A11: e in G1.edgesDBetween({v},{w}) by XBOOLE_0:def 1;
take e;
e DSJoins {v},{w},G1 by A11, GLIB_000:def 31;
then e in the_Edges_of G1 & (the_Source_of G1).e in {v} &
(the_Target_of G1).e in {w} by GLIB_000:def 16;
then e in the_Edges_of G1 & (the_Source_of G1).e = v &
(the_Target_of G1).e = w by TARSKI:def 1;
hence e DJoins v,w,G1 by GLIB_000:def 14;
end;
hence f is Dcontinuous;
end;
end;
theorem Th8:
for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2
st f is total one-to-one continuous for v,w being Vertex of G1
holds card G1.edgesBetween({v},{w}) = card G2.edgesBetween({f.v},{f.w})
proof
let G1, G2 be non-multi _Graph, f be PVertexMapping of G1, G2;
assume A1: f is total one-to-one continuous;
let v,w be Vertex of G1;
per cases;
suppose A2: G1.edgesBetween({v},{w}) = {};
G2.edgesBetween({f.v},{f.w}) = {}
proof
assume G2.edgesBetween({f.v},{f.w}) <> {};
then consider e2 being object such that
A3: G2.edgesBetween({f.v},{f.w}) = {e2} by ZFMISC_1:131;
set v1 = (the_Source_of G2).e2, v2 = (the_Target_of G2).e2;
e2 in G2.edgesBetween({f.v},{f.w}) by A3, TARSKI:def 1;
then e2 SJoins {f.v},{f.w},G2 by GLIB_000:def 30;
then A4: e2 in the_Edges_of G2 & (v1 in {f.v} & v2 in {f.w} or
v1 in {f.w} & v2 in {f.v}) by GLIB_000:def 15;
then v1 = f.v & v2 = f.w or v1 = f.w & v2 = f.v by TARSKI:def 1;
then A5: e2 Joins f.v, f.w, G2 by A4, GLIB_000:def 13;
v in the_Vertices_of G1 & w in the_Vertices_of G1 & f is total by A1;
then v in dom f & w in dom f by FUNCT_2:def 1;
then consider e1 being object such that
A6: e1 Joins v,w,G1 by A1, A5, Th2;
v in {v} & w in {w} by TARSKI:def 1;
then e1 SJoins {v},{w},G1 by A6, GLIB_000:17;
hence contradiction by A2, GLIB_000:def 30;
end;
hence card G1.edgesBetween({v},{w})
= card G2.edgesBetween({f.v},{f.w}) by A2;
end;
suppose G1.edgesBetween({v},{w}) <> {};
then consider e1 being object such that
A7: G1.edgesBetween({v},{w}) = {e1} by ZFMISC_1:131;
set v1 = (the_Source_of G1).e1, v2 = (the_Target_of G1).e1;
e1 in G1.edgesBetween({v},{w}) by A7, TARSKI:def 1;
then e1 SJoins {v},{w},G1 by GLIB_000:def 30;
then A8: e1 in the_Edges_of G1 &
(v1 in {v} & v2 in {w} or v1 in {w} & v2 in {v}) by GLIB_000:def 15;
then v1 = v & v2 = w or v1 = w & v2 = v by TARSKI:def 1;
then A9: e1 Joins v,w,G1 by A8, GLIB_000:def 13;
v in the_Vertices_of G1 & w in the_Vertices_of G1 & f is total by A1;
then v in dom f & w in dom f by FUNCT_2:def 1;
then consider e2 being object such that
A10: e2 Joins f.v,f.w,G2 by A9, Th1;
f.v in {f.v} & f.w in {f.w} by TARSKI:def 1;
then e2 SJoins {f.v},{f.w},G2 by A10, GLIB_000:17;
then e2 in G2.edgesBetween({f.v},{f.w}) by GLIB_000:def 30;
then consider e being object such that
A11: G2.edgesBetween({f.v},{f.w}) = {e} by ZFMISC_1:131;
card G1.edgesBetween({v},{w}) = 1 &
card G2.edgesBetween({f.v},{f.w}) = 1 by A7, A11, CARD_1:30;
hence card G1.edgesBetween({v},{w})
= card G2.edgesBetween({f.v},{f.w});
end;
end;
definition
let G1, G2 be non-multi _Graph, f be PVertexMapping of G1, G2;
redefine attr f is isomorphism means :: redefines isomorphism (GLIB_011, definition)
f is total one-to-one onto continuous;
compatibility by Th8;
end;
registration
let G1, G2 be non-multi _Graph;
cluster total one-to-one onto continuous -> isomorphism
for PVertexMapping of G1, G2;
coherence;
end;
theorem Th9:
for G1, G2 being non-Dmulti _Graph, f being PVertexMapping of G1, G2
st f is total one-to-one directed Dcontinuous for v,w being Vertex of G1
holds card G1.edgesDBetween({v},{w}) = card G2.edgesDBetween({f.v},{f.w}) &
card G1.edgesDBetween({w},{v}) = card G2.edgesDBetween({f.w},{f.v})
proof
let G1, G2 be non-Dmulti _Graph, f be PVertexMapping of G1, G2;
assume A1: f is total one-to-one directed Dcontinuous;
let v,w be Vertex of G1;
hereby
per cases;
suppose A2: G1.edgesDBetween({v},{w}) = {};
G2.edgesDBetween({f.v},{f.w}) = {}
proof
assume G2.edgesDBetween({f.v},{f.w}) <> {};
then consider e2 being object such that
A3: G2.edgesDBetween({f.v},{f.w}) = {e2}
by ZFMISC_1:131;
set v1 = (the_Source_of G2).e2, v2 = (the_Target_of G2).e2;
e2 in G2.edgesDBetween({f.v},{f.w}) by A3, TARSKI:def 1;
then e2 DSJoins {f.v},{f.w},G2 by GLIB_000:def 31;
then A4: e2 in the_Edges_of G2 & v1 in {f.v} & v2 in {f.w}
by GLIB_000:def 16;
then A5: v1 = f.v & v2 = f.w by TARSKI:def 1;
v in the_Vertices_of G1 & w in the_Vertices_of G1 & f is total by A1;
then v in dom f & w in dom f by FUNCT_2:def 1;
then consider e1 being object such that
A6: e1 DJoins v,w,G1 by A1, A4, A5, GLIB_000:def 14;
v in {v} & w in {w} by TARSKI:def 1;
then e1 DSJoins {v},{w},G1 by A6, GLIB_000:126;
hence contradiction by A2, GLIB_000:def 31;
end;
hence card G1.edgesDBetween({v},{w})
= card G2.edgesDBetween({f.v},{f.w}) by A2;
end;
suppose G1.edgesDBetween({v},{w}) <> {};
then consider e1 being object such that
A7: G1.edgesDBetween({v},{w}) = {e1} by ZFMISC_1:131;
set v1 = (the_Source_of G1).e1, v2 = (the_Target_of G1).e1;
e1 in G1.edgesDBetween({v},{w}) by A7, TARSKI:def 1;
then e1 DSJoins {v},{w},G1 by GLIB_000:def 31;
then A8: e1 in the_Edges_of G1 & v1 in {v} & v2 in {w}
by GLIB_000:def 16;
then v1 = v & v2 = w by TARSKI:def 1;
then A9: e1 DJoins v,w,G1 by A8, GLIB_000:def 14;
v in the_Vertices_of G1 & w in the_Vertices_of G1 & f is total by A1;
then v in dom f & w in dom f by FUNCT_2:def 1;
then consider e2 being object such that
A10: e2 DJoins f.v,f.w,G2 by A1, A9;
f.v in {f.v} & f.w in {f.w} by TARSKI:def 1;
then e2 DSJoins {f.v},{f.w},G2 by A10, GLIB_000:126;
then e2 in G2.edgesDBetween({f.v},{f.w}) by GLIB_000:def 31;
then consider e being object such that
A11: G2.edgesDBetween({f.v},{f.w}) = {e} by ZFMISC_1:131;
card G1.edgesDBetween({v},{w}) = 1 &
card G2.edgesDBetween({f.v},{f.w}) = 1 by A7, A11, CARD_1:30;
hence card G1.edgesDBetween({v},{w})
= card G2.edgesDBetween({f.v},{f.w});
end;
end;
per cases;
suppose A12: G1.edgesDBetween({w},{v}) = {};
G2.edgesDBetween({f.w},{f.v}) = {}
proof
assume G2.edgesDBetween({f.w},{f.v}) <> {};
then consider e2 being object such that
A13: G2.edgesDBetween({f.w},{f.v}) = {e2} by ZFMISC_1:131;
set v1 = (the_Source_of G2).e2, v2 = (the_Target_of G2).e2;
e2 in G2.edgesDBetween({f.w},{f.v}) by A13, TARSKI:def 1;
then e2 DSJoins {f.w},{f.v},G2 by GLIB_000:def 31;
then A14: e2 in the_Edges_of G2 & v1 in {f.w} & v2 in {f.v}
by GLIB_000:def 16;
then A15: v1 = f.w & v2 = f.v by TARSKI:def 1;
v in the_Vertices_of G1 & w in the_Vertices_of G1 & f is total by A1;
then v in dom f & w in dom f by FUNCT_2:def 1;
then consider e1 being object such that
A16: e1 DJoins w,v,G1 by A1, A14, A15, GLIB_000:def 14;
v in {v} & w in {w} by TARSKI:def 1;
then e1 DSJoins {w},{v},G1 by A16, GLIB_000:126;
hence contradiction by A12, GLIB_000:def 31;
end;
hence card G1.edgesDBetween({w},{v})
= card G2.edgesDBetween({f.w},{f.v}) by A12;
end;
suppose G1.edgesDBetween({w},{v}) <> {};
then consider e1 being object such that
A17: G1.edgesDBetween({w},{v}) = {e1} by ZFMISC_1:131;
set v1 = (the_Source_of G1).e1, v2 = (the_Target_of G1).e1;
e1 in G1.edgesDBetween({w},{v}) by A17, TARSKI:def 1;
then e1 DSJoins {w},{v},G1 by GLIB_000:def 31;
then A18: e1 in the_Edges_of G1 & v1 in {w} & v2 in {v}
by GLIB_000:def 16;
then v1 = w & v2 = v by TARSKI:def 1;
then A19: e1 DJoins w,v,G1 by A18, GLIB_000:def 14;
v in the_Vertices_of G1 & w in the_Vertices_of G1 & f is total by A1;
then v in dom f & w in dom f by FUNCT_2:def 1;
then consider e2 being object such that
A20: e2 DJoins f.w,f.v,G2 by A1, A19;
f.v in {f.v} & f.w in {f.w} by TARSKI:def 1;
then e2 DSJoins {f.w},{f.v},G2 by A20, GLIB_000:126;
then e2 in G2.edgesDBetween({f.w},{f.v}) by GLIB_000:def 31;
then consider e being object such that
A21: G2.edgesDBetween({f.w},{f.v}) = {e} by ZFMISC_1:131;
card G1.edgesDBetween({w},{v}) = 1 &
card G2.edgesDBetween({f.w},{f.v}) = 1 by A17, A21, CARD_1:30;
hence card G1.edgesDBetween({w},{v})
= card G2.edgesDBetween({f.w},{f.v});
end;
end;
definition
let G1, G2 be non-Dmulti _Graph, f be PVertexMapping of G1, G2;
redefine attr f is Disomorphism means :: redefines Disomorphism (GLIB_011, definition)
f is total one-to-one onto directed Dcontinuous;
compatibility by Th9;
end;
registration
let G1, G2 be non-Dmulti _Graph;
cluster total one-to-one onto directed Dcontinuous -> Disomorphism
for PVertexMapping of G1, G2;
coherence;
end;
registration
let G be_Graph;
cluster Disomorphism isomorphism for PVertexMapping of G, G;
existence
proof
reconsider f = id the_Vertices_of G as PVertexMapping of G, G by Th5;
take f;
thus f is Disomorphism;
thus f is isomorphism;
end;
end;
theorem
for G being _Graph holds id the_Vertices_of G
is Disomorphism isomorphism PVertexMapping of G, G
proof
let G be _Graph;
reconsider f = id the_Vertices_of G as PVertexMapping of G, G by Th5;
f is Disomorphism;
hence thesis;
end;
definition
let G1, G2 be _Graph, f be PVertexMapping of G1, G2;
attr f is invertible means
f is one-to-one continuous;
end;
registration
let G1, G2 be _Graph;
cluster invertible -> one-to-one continuous for PVertexMapping of G1, G2;
coherence;
cluster one-to-one continuous -> invertible for PVertexMapping of G1, G2;
coherence;
cluster isomorphism -> invertible for PVertexMapping of G1, G2;
coherence;
cluster Disomorphism -> invertible for PVertexMapping of G1, G2;
coherence;
cluster empty invertible for PVertexMapping of G1, G2;
existence
proof
take the empty one-to-one continuous PVertexMapping of G1, G2;
thus thesis;
end;
end;
registration
let G1, G2 be loopless _Graph;
cluster non empty directed invertible for PVertexMapping of G1, G2;
existence
proof
take the non empty directed one-to-one continuous PVertexMapping of G1, G2;
thus thesis;
end;
end;
registration
let G1, G2 be non loopless _Graph;
cluster non empty directed invertible for PVertexMapping of G1, G2;
existence
proof
take the non empty directed one-to-one continuous PVertexMapping of G1, G2;
thus thesis;
end;
end;
definition
let G1, G2 be _Graph, f be invertible PVertexMapping of G1, G2;
redefine func f" -> PVertexMapping of G2, G1; :: redefines " (FUNCT_1, definition)
coherence
proof
now
let v,w,e be object;
assume A1: v in dom(f") & w in dom(f") & e Joins v,w,G2;
then A2: v in rng f & w in rng f by FUNCT_1:33;
then consider v0 being object such that
A3: v0 in dom f & f.v0 = v by FUNCT_1:def 3;
consider w0 being object such that
A4: w0 in dom f & f.w0 = w by A2, FUNCT_1:def 3;
consider e0 being object such that
A5: e0 Joins v0,w0,G1 by A1, A3, A4, Th2;
take e0;
f".v = v0 & f".w = w0 by A3, A4, FUNCT_1:34;
hence e0 Joins f".v,f".w,G1 by A5;
end;
hence thesis by Th1;
end;
end;
registration
let G1, G2 be _Graph, f be invertible PVertexMapping of G1, G2;
cluster f" -> one-to-one continuous invertible for PVertexMapping of G2, G1;
coherence
proof
let g be PVertexMapping of G2, G1;
assume A1: g = f";
hence A2: g is one-to-one;
now
let v,w,e9 be object;
assume v in dom g;
then v in rng f by A1, FUNCT_1:33;
then consider v0 being object such that
A3: v0 in dom f & f.v0 = v by FUNCT_1:def 3;
assume w in dom g;
then w in rng f by A1, FUNCT_1:33;
then consider w0 being object such that
A4: w0 in dom f & f.w0 = w by FUNCT_1:def 3;
assume e9 Joins g.v,g.w,G1;
then e9 Joins v0,g.(f.w0),G1 by A1, A3, A4, FUNCT_1:34;
then e9 Joins v0,w0,G1 by A1, A4, FUNCT_1:34;
then consider e being object such that
A5: e Joins f.v0,f.w0,G2 by A3, A4, Th1;
take e;
thus e Joins v,w,G2 by A3, A4, A5;
end;
hence g is continuous invertible by A2, Th2;
end;
end;
definition
let G1, G2, G3 be _Graph;
let f be PVertexMapping of G1, G2, g be PVertexMapping of G2, G3;
redefine func g*f -> PVertexMapping of G1, G3; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence
proof
now
let v,w,e be object;
assume A1: v in dom(g*f) & w in dom(g*f) & e Joins v,w,G1;
then A2: v in dom f & w in dom f & f.v in dom g & f.w in dom g
by FUNCT_1:11;
then consider e8 being object such that
A3: e8 Joins f.v,f.w,G2 by A1, Th1;
consider e9 being object such that
A4: e9 Joins g.(f.v),g.(f.w),G3 by A2, A3, Th1;
take e9;
(g*f).v = g.(f.v) & (g*f).w = g.(f.w) by A1, FUNCT_1:12;
hence e9 Joins (g*f).v,(g*f).w,G3 by A4;
end;
hence thesis by Th1;
end;
end;
theorem
for G1, G2, G3 being _Graph
for f being PVertexMapping of G1, G2, g being PVertexMapping of G2, G3
st f is continuous & g is continuous holds g*f is continuous
proof
let G1, G2, G3 be _Graph;
let f be PVertexMapping of G1, G2, g be PVertexMapping of G2, G3;
assume A1: f is continuous & g is continuous;
now
let v,w,e9 be object;
assume A2: v in dom (g*f) & w in dom (g*f) & e9 Joins (g*f).v,(g*f).w,G3;
then e9 Joins g.(f.v),(g*f).w,G3 by FUNCT_1:12;
then A3: e9 Joins g.(f.v),g.(f.w),G3 by A2, FUNCT_1:12;
f.v in dom g & f.w in dom g by A2, FUNCT_1:11;
then consider e8 being object such that
A4: e8 Joins f.v,f.w,G2 by A1, A3, Th2;
v in dom f & w in dom f by A2, FUNCT_1:11;
then consider e being object such that
A5: e Joins v,w,G1 by A1, A4, Th2;
take e;
thus e Joins v,w,G1 by A5;
end;
hence thesis by Th2;
end;
theorem
for G1, G2, G3 being _Graph
for f being PVertexMapping of G1, G2, g being PVertexMapping of G2, G3
st f is directed & g is directed holds g*f is directed
proof
let G1, G2, G3 be _Graph;
let f be PVertexMapping of G1, G2, g be PVertexMapping of G2, G3;
assume A1: f is directed & g is directed;
now
let v,w,e9 be object;
assume A2: v in dom (g*f) & w in dom (g*f) & e9 DJoins v,w,G1;
then v in dom f & w in dom f by FUNCT_1:11;
then consider e8 being object such that
A3: e8 DJoins f.v,f.w,G2 by A1, A2;
f.v in dom g & f.w in dom g by A2, FUNCT_1:11;
then consider e being object such that
A4: e DJoins g.(f.v),g.(f.w),G3 by A1, A3;
take e;
e DJoins (g*f).v,g.(f.w),G3 by A2, A4, FUNCT_1:12;
hence e DJoins (g*f).v,(g*f).w,G3 by A2, FUNCT_1:12;
end;
hence thesis;
end;
theorem
for G1, G2, G3 being _Graph
for f being PVertexMapping of G1, G2, g being PVertexMapping of G2, G3
st f is Dcontinuous & g is Dcontinuous holds g*f is Dcontinuous
proof
let G1, G2, G3 be _Graph;
let f be PVertexMapping of G1, G2, g be PVertexMapping of G2, G3;
assume A1: f is Dcontinuous & g is Dcontinuous;
now
let v,w,e9 be object;
assume A2: v in dom (g*f) & w in dom (g*f) & e9 DJoins (g*f).v,(g*f).w,G3;
then e9 DJoins g.(f.v),(g*f).w,G3 by FUNCT_1:12;
then A3: e9 DJoins g.(f.v),g.(f.w),G3 by A2, FUNCT_1:12;
f.v in dom g & f.w in dom g by A2, FUNCT_1:11;
then consider e8 being object such that
A4: e8 DJoins f.v,f.w,G2 by A1, A3;
v in dom f & w in dom f by A2, FUNCT_1:11;
then consider e being object such that
A5: e DJoins v,w,G1 by A1, A4;
take e;
thus e DJoins v,w,G1 by A5;
end;
hence thesis;
end;
theorem
for G1, G2, G3 being _Graph
for f being PVertexMapping of G1, G2, g being PVertexMapping of G2, G3
st f is isomorphism & g is isomorphism holds g*f is isomorphism
proof
let G1, G2, G3 be _Graph;
let f be PVertexMapping of G1, G2, g be PVertexMapping of G2, G3;
assume A1: f is isomorphism & g is isomorphism;
hence g*f is total one-to-one onto by FUNCT_2:27;
let v,w be Vertex of G1;
v in the_Vertices_of G1 & w in the_Vertices_of G1;
then A2: v in dom f & w in dom f by A1, PARTFUN1:def 2;
then A3: f.v in rng f & f.w in rng f by FUNCT_1:3;
thus card G1.edgesBetween({v},{w})
= card G2.edgesBetween({f.v},{f.w}) by A1
.= card G3.edgesBetween({g.(f.v)},{g.(f.w)}) by A1, A3
.= card G3.edgesBetween({(g*f).v},{g.(f.w)}) by A2, FUNCT_1:13
.= card G3.edgesBetween({(g*f).v},{(g*f).w}) by A2, FUNCT_1:13;
end;
theorem
for G1, G2, G3 being _Graph
for f being PVertexMapping of G1, G2, g being PVertexMapping of G2, G3
st f is Disomorphism & g is Disomorphism holds g*f is Disomorphism
proof
let G1, G2, G3 be _Graph;
let f be PVertexMapping of G1, G2, g be PVertexMapping of G2, G3;
assume A1: f is Disomorphism & g is Disomorphism;
hence g*f is total one-to-one onto by FUNCT_2:27;
let v,w be Vertex of G1;
v in the_Vertices_of G1 & w in the_Vertices_of G1;
then A2: v in dom f & w in dom f by A1, PARTFUN1:def 2;
then A3: f.v in rng f & f.w in rng f by FUNCT_1:3;
thus card G1.edgesDBetween({v},{w})
= card G2.edgesDBetween({f.v},{f.w}) by A1
.= card G3.edgesDBetween({g.(f.v)},{g.(f.w)}) by A1, A3
.= card G3.edgesDBetween({(g*f).v},{g.(f.w)}) by A2, FUNCT_1:13
.= card G3.edgesDBetween({(g*f).v},{(g*f).w}) by A2, FUNCT_1:13;
thus card G1.edgesDBetween({w},{v})
= card G2.edgesDBetween({f.w},{f.v}) by A1
.= card G3.edgesDBetween({g.(f.w)},{g.(f.v)}) by A1, A3
.= card G3.edgesDBetween({(g*f).w},{g.(f.v)}) by A2, FUNCT_1:13
.= card G3.edgesDBetween({(g*f).w},{(g*f).v}) by A2, FUNCT_1:13;
end;
begin :: The relation between Graph Mappings and Vertex Mappings
theorem Th16:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st for v,w being Vertex of G1 st v in dom F_V & w in dom F_V &
v,w are_adjacent ex e being object st e in dom F_E & e Joins v,w,G1
holds F_V is PVertexMapping of G1, G2
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: for v,w being Vertex of G1 st v in dom F_V & w in dom F_V &
v,w are_adjacent ex e being object st e in dom F_E & e Joins v,w,G1;
let v,w be Vertex of G1;
assume A2: v in dom F_V & w in dom F_V & v,w are_adjacent;
then consider e being object such that
A3: e in dom F_E & e Joins v,w,G1 by A1;
A4: F_V/.v = F_V.v & F_V/.w = F_V.w by A2, PARTFUN1:def 6;
F_E.e Joins F_V.v,F_V.w,G2 by A2, A3, GLIB_010:4;
hence F_V/.v, F_V/.w are_adjacent by A4, CHORD:def 3;
end;
theorem Th17:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st dom F_E = the_Edges_of G1 holds F_V is PVertexMapping of G1, G2
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: dom F_E = the_Edges_of G1;
now
let v,w be Vertex of G1;
assume v in dom F_V & w in dom F_V & v,w are_adjacent;
then consider e being object such that
A2: e Joins v,w,G1 by CHORD:def 3;
take e;
thus e in dom F_E by A1, A2, GLIB_000:def 13;
thus e Joins v,w,G1 by A2;
end;
hence thesis by Th16;
end;
theorem Th18:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is total holds F_V is PVertexMapping of G1, G2
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume F is total;
then dom F_E = the_Edges_of G1 by GLIB_010:def 11;
hence thesis by Th17;
end;
theorem Th19:
for G1, G2 being _Graph, F being directed PGraphMapping of G1, G2
st for v,w being object st v in dom F_V & w in dom F_V &
ex e being object st e DJoins v,w,G1
holds ex e being object st e in dom F_E & e DJoins v,w,G1
holds F_V is directed PVertexMapping of G1, G2
proof
let G1, G2 be _Graph, F be directed PGraphMapping of G1, G2;
assume A1: for v,w being object st v in dom F_V & w in dom F_V &
ex e being object st e DJoins v,w,G1
holds ex e being object st e in dom F_E & e DJoins v,w,G1;
now
let v,w,e be object;
assume A2: v in dom F_V & w in dom F_V & e Joins v,w,G1;
then per cases by GLIB_000:16;
suppose e DJoins v,w,G1;
then consider e0 being object such that
A3: e0 in dom F_E & e0 DJoins v,w,G1 by A1, A2;
reconsider e9 = F_E.e0 as object;
take e9;
e0 Joins v,w,G1 by A3, GLIB_000:16;
hence e9 Joins F_V.v,F_V.w,G2 by A2, A3, GLIB_010:4;
end;
suppose e DJoins w,v,G1;
then consider e0 being object such that
A4: e0 in dom F_E & e0 DJoins w,v,G1 by A1, A2;
reconsider e9 = F_E.e0 as object;
take e9;
e0 Joins v,w,G1 by A4, GLIB_000:16;
hence e9 Joins F_V.v,F_V.w,G2 by A2, A4, GLIB_010:4;
end;
end;
then A5: F_V is PVertexMapping of G1, G2 by Th1;
now
let v,w,e be object;
assume A6: v in dom F_V & w in dom F_V & e DJoins v,w,G1;
then consider e0 being object such that
A7: e0 in dom F_E & e0 DJoins v,w,G1 by A1;
reconsider e9 = F_E.e0 as object;
take e9;
thus e9 DJoins F_V.v,F_V.w,G2 by A6, A7, GLIB_010:def 14;
end;
hence thesis by A5, Def2;
end;
theorem Th20:
for G1, G2 being _Graph, F being directed PGraphMapping of G1, G2
st dom F_E = the_Edges_of G1 holds F_V is directed PVertexMapping of G1, G2
proof
let G1, G2 be _Graph, F be directed PGraphMapping of G1, G2;
assume A1: dom F_E = the_Edges_of G1;
for v,w being object st v in dom F_V & w in dom F_V holds
(ex e being object st e DJoins v,w,G1) implies
(ex e being object st e in dom F_E & e DJoins v,w,G1)
by A1, GLIB_000:def 14;
hence thesis by Th19;
end;
theorem Th21:
for G1, G2 being _Graph, F being directed PGraphMapping of G1, G2
st F is total holds F_V is directed PVertexMapping of G1, G2
proof
let G1, G2 be _Graph, F be directed PGraphMapping of G1, G2;
assume F is total;
then dom F_E = the_Edges_of G1 by GLIB_010:def 11;
hence thesis by Th20;
end;
theorem Th22:
for G1, G2 being _Graph, F being semi-continuous PGraphMapping of G1, G2
st F_V is PVertexMapping of G1, G2 &
for v,w being Vertex of G1 st v in dom F_V & w in dom F_V &
F_V/.v, F_V/.w are_adjacent
ex e9 being object st e9 in rng F_E & e9 Joins F_V.v,F_V.w,G2
holds F_V is continuous PVertexMapping of G1, G2
proof
let G1, G2 be _Graph, F be semi-continuous PGraphMapping of G1, G2;
assume that
A1: F_V is PVertexMapping of G1, G2 and
A2: for v,w being Vertex of G1 st v in dom F_V & w in dom F_V &
F_V/.v, F_V/.w are_adjacent
ex e9 being object st e9 in rng F_E & e9 Joins F_V.v,F_V.w,G2;
reconsider f = F_V as PVertexMapping of G1, G2 by A1;
now
let v,w,e9 be object;
assume A3: v in dom f & w in dom f & e9 Joins f.v,f.w,G2;
then e9 Joins f/.v,f.w,G2 by PARTFUN1:def 6;
then e9 Joins f/.v,f/.w,G2 by A3, PARTFUN1:def 6;
then consider e8 being object such that
A4: e8 in rng F_E & e8 Joins f.v,f.w,G2 by A2, A3, CHORD:def 3;
consider e being object such that
A5: e in dom F_E & F_E.e = e8 by A4, FUNCT_1:def 3;
take e;
thus e Joins v,w,G1 by A3, A4, A5, GLIB_010:def 15;
end;
hence thesis by Th2;
end;
theorem Th23:
for G1, G2 being _Graph, F being semi-continuous PGraphMapping of G1, G2
st dom F_E = the_Edges_of G1 & rng F_E = the_Edges_of G2
holds F_V is continuous PVertexMapping of G1, G2
proof
let G1, G2 be _Graph, F be semi-continuous PGraphMapping of G1, G2;
assume A1: dom F_E = the_Edges_of G1 & rng F_E = the_Edges_of G2;
then A2: F_V is PVertexMapping of G1, G2 by Th17;
now
let v,w be Vertex of G1;
assume A3: v in dom F_V & w in dom F_V & F_V/.v, F_V/.w are_adjacent;
then consider e being object such that
A4: e Joins F_V/.v,F_V/.w,G2 by CHORD:def 3;
take e;
thus e in rng F_E by A1, A4, GLIB_000:def 13;
e Joins F_V.v,F_V/.w,G2 by A3, A4, PARTFUN1:def 6;
hence e Joins F_V.v,F_V.w,G2 by A3, PARTFUN1:def 6;
end;
hence thesis by A2, Th22;
end;
theorem
for G1, G2 being _Graph, F being semi-continuous PGraphMapping of G1, G2
st F is total onto holds F_V is continuous PVertexMapping of G1, G2
proof
let G1, G2 be _Graph, F be semi-continuous PGraphMapping of G1, G2;
assume F is total onto;
then dom F_E = the_Edges_of G1 & rng F_E = the_Edges_of G2
by GLIB_010:def 11, GLIB_010:def 12;
hence thesis by Th23;
end;
Lm1:
for x being object, f being Function st x in dom f holds f.:{x} = {f.x}
proof
let x be object, f be Function;
assume A1: x in dom f;
thus f.:{x} = Im(f,x) by RELAT_1:def 16
.= {f.x} by A1, FUNCT_1:59;
end;
theorem Th25:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is isomorphism ex f being PVertexMapping of G1, G2
st F_V = f & f is isomorphism
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: F is isomorphism;
then reconsider f = F_V as PVertexMapping of G1, G2 by Th18;
take f;
thus F_V = f;
A2: dom f = the_Vertices_of G1 by A1, GLIB_010:def 11;
hence f is total by PARTFUN1:def 2;
thus f is one-to-one by A1;
rng f = the_Vertices_of G2 by A1, GLIB_010:def 12;
hence f is onto by FUNCT_2:def 3;
let v,w be Vertex of G1;
card G1.edgesBetween({v},{w})
= card G2.edgesBetween(F_V.:{v},F_V.:{w}) by A1, GLIB_010:86
.= card G2.edgesBetween(F_V.:{v},{F_V.w}) by A2, Lm1
.= card G2.edgesBetween({f.v},{f.w}) by A2, Lm1;
hence thesis;
end;
theorem Th26:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is Disomorphism ex f being directed PVertexMapping of G1, G2
st F_V = f & f is Disomorphism
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: F is Disomorphism;
then reconsider f = F_V as directed PVertexMapping of G1, G2 by Th21;
take f;
thus F_V = f;
A2: dom f = the_Vertices_of G1 by A1, GLIB_010:def 11;
hence f is total by PARTFUN1:def 2;
thus f is one-to-one by A1;
rng f = the_Vertices_of G2 by A1, GLIB_010:def 12;
hence f is onto by FUNCT_2:def 3;
let v,w be Vertex of G1;
A3: card G1.edgesDBetween({v},{w})
= card G2.edgesDBetween(F_V.:{v},F_V.:{w}) by A1, GLIB_010:88
.= card G2.edgesDBetween(F_V.:{v},{F_V.w}) by A2, Lm1
.= card G2.edgesDBetween({f.v},{f.w}) by A2, Lm1;
card G1.edgesDBetween({w},{v})
= card G2.edgesDBetween(F_V.:{w},F_V.:{v}) by A1, GLIB_010:88
.= card G2.edgesDBetween(F_V.:{w},{F_V.v}) by A2, Lm1
.= card G2.edgesDBetween({f.w},{f.v}) by A2, Lm1;
hence thesis by A3;
end;
:: Maybe add that f is continuous implies rng F_E = E2 /\ ... ?
:: An example why this isn't always the case is the embedding of P_3 into K_3
theorem Th27:
for G1, G2 being _Graph, f being PVertexMapping of G1, G2
for E1 being RepEdgeSelection of G1, E2 being RepEdgeSelection of G2
ex F being PGraphMapping of G1, G2
st F_V = f & dom F_E = E1 /\ G1.edgesBetween(dom f) &
rng F_E c= E2 /\ G2.edgesBetween(rng f)
proof
let G1, G2 be _Graph, f be PVertexMapping of G1, G2;
let E1 be RepEdgeSelection of G1, E2 be RepEdgeSelection of G2;
defpred P[object,object] means ex v,w being object
st v in dom f & w in dom f & $1 in E1 & $2 in E2 &
$1 Joins v,w,G1 & $2 Joins f.v,f.w,G2;
A1: for e1,e2,e3 being object st e1 in E1 /\ G1.edgesBetween(dom f) &
P[e1,e2] & P[e1,e3] holds e2 = e3
proof
let e1,e2,e3 be object;
assume A2: e1 in E1 /\ G1.edgesBetween(dom f) & P[e1,e2] & P[e1,e3];
then consider v2,w2 being object such that
A3: v2 in dom f & w2 in dom f & e1 in E1 & e2 in E2 &
e1 Joins v2,w2,G1 & e2 Joins f.v2,f.w2,G2;
consider v3,w3 being object such that
A4: v3 in dom f & w3 in dom f & e1 in E1 & e3 in E2 &
e1 Joins v3,w3,G1 & e3 Joins f.v3,f.w3,G2 by A2;
v2 = v3 & w2 = w3 or v2 = w3 & w2 = v3 by A3, A4, GLIB_000:15;
then f.v2 = f.v3 & f.w2 = f.w3 or f.v2 = f.w3 & f.w2 = f.v3;
then A5: e3 Joins f.v2,f.w2,G2 by A4, GLIB_000:14;
then consider e0 being object such that
e0 Joins f.v2,f.w2,G2 & e0 in E2 and
A6: for e9 being object st e9 Joins f.v2,f.w2,G2 & e9 in E2
holds e9 = e0 by GLIB_009:def 5;
e2 = e0 & e3 = e0 by A3, A4, A5, A6;
hence e2 = e3;
end;
A7: for e1 being object st e1 in E1 /\ G1.edgesBetween(dom f)
ex e2 being object st P[e1,e2]
proof
let e1 be object;
set v = (the_Source_of G1).e1, w = (the_Target_of G1).e1;
assume A8: e1 in E1 /\ G1.edgesBetween(dom f);
then e1 in G1.edgesBetween(dom f) by XBOOLE_0:def 4;
then A9: e1 in the_Edges_of G1 & v in dom f & w in dom f by GLIB_000:31;
then A10: e1 Joins v,w,G1 by GLIB_000:def 13;
then consider e0 being object such that
A11: e0 Joins f.v,f.w,G2 by A9, Th1;
consider e2 being object such that
A12: e2 Joins f.v,f.w,G2 & e2 in E2 and
for e9 being object st e9 Joins f.v,f.w,G2 & e9 in E2 holds e9 = e2
by A11, GLIB_009:def 5;
take e2, v, w;
thus v in dom f & w in dom f & e1 in E1 by A8, A9, XBOOLE_0:def 4;
thus e2 in E2 & e1 Joins v,w,G1 & e2 Joins f.v,f.w,G2 by A10, A12;
end;
consider g being Function such that
A13: dom g = E1 /\ G1.edgesBetween(dom f) and
A14: for e1 being object st e1 in E1 /\ G1.edgesBetween(dom f)
holds P[e1,g.e1] from FUNCT_1:sch 2(A1,A7);
for y being object holds y in rng g implies y in E2 /\ G2.edgesBetween(rng f)
proof
let y be object;
assume y in rng g;
then consider x being object such that
A15: x in dom g & g.x = y by FUNCT_1:def 3;
consider v,w being object such that
A16: v in dom f & w in dom f & x in E1 & g.x in E2 and
A17: x Joins v,w,G1 & g.x Joins f.v,f.w,G2 by A13, A14, A15;
f.v in rng f & f.w in rng f by A16, FUNCT_1:3;
then (the_Source_of G2).y in rng f & (the_Target_of G2).y in rng f &
y in the_Edges_of G2 by A15, A17, GLIB_000:def 13;
then y in G2.edgesBetween(rng f) by GLIB_000:31;
hence y in E2 /\ G2.edgesBetween(rng f) by A15, A16, XBOOLE_0:def 4;
end;
then A18: rng g c= E2 /\ G2.edgesBetween(rng f) by TARSKI:def 3;
rng g c= the_Edges_of G2 by A18, XBOOLE_1:1;
then reconsider g as PartFunc of the_Edges_of G1, the_Edges_of G2
by A13, RELSET_1:4;
:: defining properties of PGM
now
hereby
let e be object;
assume e in dom g;
then consider v,w being object such that
A19: v in dom f & w in dom f & e in E1 & g.e in E2 &
e Joins v,w,G1 & g.e Joins f.v,f.w,G2 by A13, A14;
thus (the_Source_of G1).e in dom f & (the_Target_of G1).e in dom f
by A19, GLIB_000:def 13;
end;
let e,v,w be object;
assume e in dom g & v in dom f & w in dom f;
then consider v0,w0 being object such that
A20: v0 in dom f & w0 in dom f & e in E1 & g.e in E2 &
e Joins v0,w0,G1 & g.e Joins f.v0,f.w0,G2 by A13, A14;
assume e Joins v,w,G1;
then v = v0 & w = w0 or v = w0 & w = v0 by A20, GLIB_000:15;
hence g.e Joins f.v,f.w,G2 by A20, GLIB_000:14;
end;
then reconsider F = [f,g] as PGraphMapping of G1, G2 by GLIB_010:8;
take F;
thus thesis by A13, A18;
end;
definition
let G1, G2 be non-multi _Graph, f be PVertexMapping of G1, G2;
func PVM2PGM(f) -> PGraphMapping of G1, G2 means
:Def10:
it _V = f & dom it _E = G1.edgesBetween(dom f) &
rng it _E c= G2.edgesBetween(rng f);
existence
proof
set E1 = the RepEdgeSelection of G1, E2 = the RepEdgeSelection of G2;
consider F being PGraphMapping of G1, G2 such that
A1: F_V = f & dom F_E = E1 /\ G1.edgesBetween(dom f) &
rng F_E c= E2 /\ G2.edgesBetween(rng f) by Th27;
take F;
thus F_V = f by A1;
A2: E1 = the_Edges_of G1 & E2 = the_Edges_of G2 by GLIB_009:74;
hence dom F_E = G1.edgesBetween(dom f) by A1, XBOOLE_1:28;
thus rng F_E c= G2.edgesBetween(rng f) by A1, A2, XBOOLE_1:28;
end;
uniqueness by GLIB_010:40;
end;
theorem Th28:
for G1, G2 being non-multi _Graph
for f be PVertexMapping of G1, G2 holds (PVM2PGM(f))_V = f by Def10;
registration
let G1, G2 be non-multi _Graph, f be PVertexMapping of G1, G2;
reduce (PVM2PGM f)_V to f;
reducibility by Th28;
end;
:: as above
theorem Th29:
for G1, G2 being _Graph, f being directed PVertexMapping of G1, G2
for E1 being RepDEdgeSelection of G1, E2 being RepDEdgeSelection of G2
ex F being directed PGraphMapping of G1, G2
st F_V = f & dom F_E = E1 /\ G1.edgesBetween(dom f) &
rng F_E c= E2 /\ G2.edgesBetween(rng f)
proof
let G1, G2 be _Graph, f be directed PVertexMapping of G1, G2;
let E1 be RepDEdgeSelection of G1, E2 be RepDEdgeSelection of G2;
defpred P[object,object] means ex v,w being object
st v in dom f & w in dom f & $1 in E1 & $2 in E2 &
$1 DJoins v,w,G1 & $2 DJoins f.v,f.w,G2;
A1: for e1,e2,e3 being object st e1 in E1 /\ G1.edgesBetween(dom f) &
P[e1,e2] & P[e1,e3] holds e2 = e3
proof
let e1,e2,e3 be object;
assume A2: e1 in E1 /\ G1.edgesBetween(dom f) & P[e1,e2] & P[e1,e3];
then consider v2,w2 being object such that
A3: v2 in dom f & w2 in dom f & e1 in E1 & e2 in E2 &
e1 DJoins v2,w2,G1 & e2 DJoins f.v2,f.w2,G2;
consider v3,w3 being object such that
A4: v3 in dom f & w3 in dom f & e1 in E1 & e3 in E2 &
e1 DJoins v3,w3,G1 & e3 DJoins f.v3,f.w3,G2 by A2;
A5: v2 = v3 & w2 = w3 by A3, A4, GLIB_000:125;
then consider e0 being object such that
e0 DJoins f.v2,f.w2,G2 & e0 in E2 and
A6: for e9 being object st e9 DJoins f.v2,f.w2,G2 & e9 in E2
holds e9 = e0 by A4, GLIB_009:def 6;
e2 = e0 & e3 = e0 by A3, A4, A5, A6;
hence e2 = e3;
end;
A7: for e1 being object st e1 in E1 /\ G1.edgesBetween(dom f)
ex e2 being object st P[e1,e2]
proof
let e1 be object;
set v = (the_Source_of G1).e1, w = (the_Target_of G1).e1;
assume A8: e1 in E1 /\ G1.edgesBetween(dom f);
then e1 in G1.edgesBetween(dom f) by XBOOLE_0:def 4;
then A9: e1 in the_Edges_of G1 & v in dom f & w in dom f by GLIB_000:31;
then A10: e1 DJoins v,w,G1 by GLIB_000:def 14;
then consider e0 being object such that
A11: e0 DJoins f.v,f.w,G2 by A9, Def2;
consider e2 being object such that
A12: e2 DJoins f.v,f.w,G2 & e2 in E2 and
for e9 being object st e9 DJoins f.v,f.w,G2 & e9 in E2 holds e9 = e2
by A11, GLIB_009:def 6;
take e2, v, w;
thus v in dom f & w in dom f & e1 in E1 by A8, A9, XBOOLE_0:def 4;
thus e2 in E2 & e1 DJoins v,w,G1 & e2 DJoins f.v,f.w,G2 by A10, A12;
end;
consider g being Function such that
A13: dom g = E1 /\ G1.edgesBetween(dom f) and
A14: for e1 being object st e1 in E1 /\ G1.edgesBetween(dom f)
holds P[e1,g.e1] from FUNCT_1:sch 2(A1,A7);
for y being object holds y in rng g implies y in E2 /\ G2.edgesBetween(rng f)
proof
let y be object;
assume y in rng g;
then consider x being object such that
A15: x in dom g & g.x = y by FUNCT_1:def 3;
consider v,w being object such that
A16: v in dom f & w in dom f & x in E1 & g.x in E2 and
A17: x DJoins v,w,G1 & g.x DJoins f.v,f.w,G2 by A13, A14, A15;
f.v in rng f & f.w in rng f by A16, FUNCT_1:3;
then (the_Source_of G2).y in rng f & (the_Target_of G2).y in rng f &
y in the_Edges_of G2 by A15, A17, GLIB_000:def 14;
then y in G2.edgesBetween(rng f) by GLIB_000:31;
hence y in E2 /\ G2.edgesBetween(rng f) by A15, A16, XBOOLE_0:def 4;
end;
then A18: rng g c= E2 /\ G2.edgesBetween(rng f) by TARSKI:def 3;
rng g c= the_Edges_of G2 by A18, XBOOLE_1:1;
then reconsider g as PartFunc of the_Edges_of G1, the_Edges_of G2
by A13, RELSET_1:4;
:: defining properties of PGM
now
hereby
let e be object;
assume e in dom g;
then consider v,w being object such that
A19: v in dom f & w in dom f & e in E1 & g.e in E2 &
e DJoins v,w,G1 & g.e DJoins f.v,f.w,G2 by A13, A14;
thus (the_Source_of G1).e in dom f & (the_Target_of G1).e in dom f
by A19, GLIB_000:def 14;
end;
let e,v,w be object;
assume e in dom g & v in dom f & w in dom f;
then consider v0,w0 being object such that
v0 in dom f & w0 in dom f & e in E1 & g.e in E2 and
A20: e DJoins v0,w0,G1 & g.e DJoins f.v0,f.w0,G2 by A13, A14;
assume e DJoins v,w,G1;
then v = v0 & w = w0 by A20, GLIB_000:125;
hence g.e DJoins f.v,f.w,G2 by A20;
end;
then reconsider F = [f,g] as directed PGraphMapping of G1, G2 by GLIB_010:30;
take F;
thus thesis by A13, A18;
end;
definition
let G1, G2 be non-Dmulti _Graph;
let f be directed PVertexMapping of G1, G2;
func DPVM2PGM(f) -> directed PGraphMapping of G1, G2 means
:Def11:
it _V = f & dom it _E = G1.edgesBetween(dom f) &
rng it _E c= G2.edgesBetween(rng f);
existence
proof
set E1 = the RepDEdgeSelection of G1, E2 = the RepDEdgeSelection of G2;
consider F being directed PGraphMapping of G1, G2 such that
A1: F_V = f & dom F_E = E1 /\ G1.edgesBetween(dom f) &
rng F_E c= E2 /\ G2.edgesBetween(rng f) by Th29;
take F;
thus F_V = f by A1;
A2: E1 = the_Edges_of G1 & E2 = the_Edges_of G2 by GLIB_009:76;
hence dom F_E = G1.edgesBetween(dom f) by A1, XBOOLE_1:28;
thus rng F_E c= G2.edgesBetween(rng f) by A1, A2, XBOOLE_1:28;
end;
uniqueness by GLIB_010:41;
end;
theorem Th30:
for G1, G2 being non-Dmulti _Graph
for f be directed PVertexMapping of G1, G2 holds (DPVM2PGM(f))_V = f
by Def11;
registration
let G1, G2 be non-Dmulti _Graph;
let f be directed PVertexMapping of G1, G2;
reduce (DPVM2PGM f)_V to f;
reducibility by Th30;
end;
theorem
for G1, G2 being non-multi _Graph
for f being directed PVertexMapping of G1, G2
holds PVM2PGM(f) = DPVM2PGM(f)
proof
let G1, G2 be non-multi _Graph;
let f be directed PVertexMapping of G1, G2;
A1: (PVM2PGM f)_V = f & (DPVM2PGM f)_V = f;
dom (PVM2PGM f)_E = G1.edgesBetween(dom f) &
dom (DPVM2PGM f)_E = G1.edgesBetween(dom f) by Def10, Def11;
hence thesis by A1, GLIB_010:40;
end;
theorem Th32:
for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2
st f is total holds PVM2PGM(f) is total
proof
let G1, G2 be non-multi _Graph, f be PVertexMapping of G1, G2;
assume f is total;
then A1: dom f = the_Vertices_of G1 by PARTFUN1:def 2;
A2: dom (PVM2PGM f)_E = G1.edgesBetween(dom f) by Def10
.= the_Edges_of G1 by A1, GLIB_000:34;
(PVM2PGM f)_V = f;
hence thesis by A1, A2, GLIB_010:def 11;
end;
theorem Th33:
for G1, G2 being non-Dmulti _Graph, f being directed PVertexMapping of G1, G2
st f is total holds DPVM2PGM(f) is total
proof
let G1, G2 be non-Dmulti _Graph, f be directed PVertexMapping of G1, G2;
assume f is total;
then A1: dom f = the_Vertices_of G1 by PARTFUN1:def 2;
A2: dom (DPVM2PGM f)_E = G1.edgesBetween(dom f) by Def11
.= the_Edges_of G1 by A1, GLIB_000:34;
(DPVM2PGM f)_V = f;
hence thesis by A1, A2, GLIB_010:def 11;
end;
theorem Th34:
for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2
st f is one-to-one holds PVM2PGM(f) is one-to-one
proof
let G1, G2 be non-multi _Graph, f be PVertexMapping of G1, G2;
assume A1: f is one-to-one;
then A2: (PVM2PGM f)_V is one-to-one;
set g = (PVM2PGM f)_E;
for x1,x2 being object st x1 in dom g & x2 in dom g & g.x1 = g.x2
holds x1 = x2
proof
let x1,x2 be object;
set v1 = (the_Source_of G1).x1, w1 = (the_Target_of G1).x1,
v2 = (the_Source_of G1).x2, w2 = (the_Target_of G1).x2;
assume A3: x1 in dom g & x2 in dom g & g.x1 = g.x2;
then x1 in G1.edgesBetween(dom f) by Def10;
then A4: x1 in the_Edges_of G1 & v1 in dom f & w1 in dom f by GLIB_000:31;
then A5: x1 Joins v1,w1,G1 by GLIB_000:def 13;
then g.x1 Joins (PVM2PGM f)_V.v1,(PVM2PGM f)_V.w1,G2 by A3, A4, GLIB_010:4;
then A6: g.x1 Joins f.v1,f.w1,G2;
x2 in G1.edgesBetween(dom f) by A3, Def10;
then A7: x2 in the_Edges_of G1 & v2 in dom f & w2 in dom f by GLIB_000:31;
then A8: x2 Joins v2,w2,G1 by GLIB_000:def 13;
then g.x2 Joins (PVM2PGM f)_V.v2,(PVM2PGM f)_V.w2,G2 by A3, A7, GLIB_010:4;
then per cases by A3, A6, GLIB_000:15;
suppose f.v1 = f.v2 & f.w1 = f.w2;
then v1 = v2 & w1 = w2 by A1, A4, A7, FUNCT_1:def 4;
hence x1 = x2 by A5, A8, GLIB_000:def 20;
end;
suppose f.v1 = f.w2 & f.w1 = f.v2;
then v1 = w2 & w1 = v2 by A1, A4, A7, FUNCT_1:def 4;
then x2 Joins v1,w1,G1 by A8, GLIB_000:14;
hence x1 = x2 by A5, GLIB_000:def 20;
end;
end;
then g is one-to-one by FUNCT_1:def 4;
hence thesis by A2, GLIB_010:def 13;
end;
theorem Th35:
for G1, G2 being non-Dmulti _Graph, f being directed PVertexMapping of G1, G2
st f is one-to-one holds DPVM2PGM(f) is one-to-one
proof
let G1, G2 be non-Dmulti _Graph, f be directed PVertexMapping of G1, G2;
assume A1: f is one-to-one;
then A2: (DPVM2PGM f)_V is one-to-one;
set g = (DPVM2PGM f)_E;
for x1,x2 being object st x1 in dom g & x2 in dom g & g.x1 = g.x2
holds x1 = x2
proof
let x1,x2 be object;
set v1 = (the_Source_of G1).x1, w1 = (the_Target_of G1).x1,
v2 = (the_Source_of G1).x2, w2 = (the_Target_of G1).x2;
assume A3: x1 in dom g & x2 in dom g & g.x1 = g.x2;
then x1 in G1.edgesBetween(dom f) by Def11;
then A4: x1 in the_Edges_of G1 & v1 in dom f & w1 in dom f by GLIB_000:31;
then A5: x1 DJoins v1,w1,G1 by GLIB_000:def 14;
then g.x1 DJoins (DPVM2PGM f)_V.v1,(DPVM2PGM f)_V.w1,G2
by A3, A4, GLIB_010:def 14;
then A6: g.x1 DJoins f.v1,f.w1,G2;
x2 in G1.edgesBetween(dom f) by A3, Def11;
then A7: x2 in the_Edges_of G1 & v2 in dom f & w2 in dom f by GLIB_000:31;
then A8: x2 DJoins v2,w2,G1 by GLIB_000:def 14;
then g.x2 DJoins (DPVM2PGM f)_V.v2,(DPVM2PGM f)_V.w2,G2
by A3, A7, GLIB_010:def 14;
then f.v1 = f.v2 & f.w1 = f.w2 by A3, A6, GLIB_000:125;
then v1 = v2 & w1 = w2 by A1, A4, A7, FUNCT_1:def 4;
hence x1 = x2 by A5, A8, GLIB_000:def 21;
end;
then g is one-to-one by FUNCT_1:def 4;
hence thesis by A2, GLIB_010:def 13;
end;
theorem Th36:
for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2
st f is onto continuous holds PVM2PGM(f) is onto
proof
let G1, G2 be non-multi _Graph, f be PVertexMapping of G1, G2;
assume A1: f is onto continuous;
then A2: rng (PVM2PGM f)_V = the_Vertices_of G2 by FUNCT_2:def 3;
set g = (PVM2PGM f)_E;
for e being object st e in the_Edges_of G2 holds e in rng g
proof
let e be object;
set v2 = (the_Source_of G2).e, w2 = (the_Target_of G2).e;
assume e in the_Edges_of G2;
then e in G2.edgesBetween(the_Vertices_of G2) by GLIB_000:34;
then e in G2.edgesBetween(rng f) by A1, FUNCT_2:def 3;
then A3: e in the_Edges_of G2 & v2 in rng f & w2 in rng f by GLIB_000:31;
consider v1 being object such that
A4: v1 in dom f & f.v1 = v2 by A3, FUNCT_1:def 3;
consider w1 being object such that
A5: w1 in dom f & f.w1 = w2 by A3, FUNCT_1:def 3;
A6: e Joins f.v1,f.w1,G2 by A3, A4, A5, GLIB_000:def 13;
then consider e0 being object such that
A7: e0 Joins v1,w1,G1 by A1, A4, A5, Th2;
e0 in G1.edgesBetween(dom f) by A4, A5, A7, GLIB_000:32;
then A8: e0 in dom g by Def10;
then g.e0 Joins (PVM2PGM f)_V.v1,(PVM2PGM f)_V.w1,G2
by A4, A5, A7, GLIB_010:4;
then g.e0 = e by A6, GLIB_000:def 20;
hence e in rng g by A8, FUNCT_1:def 3;
end;
then the_Edges_of G2 c= rng g by TARSKI:def 3;
then rng g = the_Edges_of G2 by XBOOLE_0:def 10;
hence thesis by A2, GLIB_010:def 12;
end;
theorem Th37:
for G1, G2 being non-Dmulti _Graph, f being directed PVertexMapping of G1, G2
st f is onto Dcontinuous holds DPVM2PGM(f) is onto
proof
let G1, G2 be non-Dmulti _Graph, f be directed PVertexMapping of G1, G2;
assume A1: f is onto Dcontinuous;
then A2: rng (DPVM2PGM f)_V = the_Vertices_of G2 by FUNCT_2:def 3;
set g = (DPVM2PGM f)_E;
for e being object st e in the_Edges_of G2 holds e in rng g
proof
let e be object;
set v2 = (the_Source_of G2).e, w2 = (the_Target_of G2).e;
assume e in the_Edges_of G2;
then e in G2.edgesBetween(the_Vertices_of G2) by GLIB_000:34;
then e in G2.edgesBetween(rng f) by A1, FUNCT_2:def 3;
then A3: e in the_Edges_of G2 & v2 in rng f & w2 in rng f by GLIB_000:31;
consider v1 being object such that
A4: v1 in dom f & f.v1 = v2 by A3, FUNCT_1:def 3;
consider w1 being object such that
A5: w1 in dom f & f.w1 = w2 by A3, FUNCT_1:def 3;
e DJoins v2,w2,G2 by A3, GLIB_000:def 14;
then A6: e DJoins f.v1,f.w1,G2 by A4, A5;
then consider e0 being object such that
A7: e0 DJoins v1,w1,G1 by A1, A4, A5;
e0 Joins v1,w1, G1 by A7, GLIB_000:16;
then e0 in G1.edgesBetween(dom f) by A4, A5, GLIB_000:32;
then A8: e0 in dom g by Def11;
then g.e0 DJoins (DPVM2PGM f)_V.v1,(DPVM2PGM f)_V.w1,G2
by A4, A5, A7, GLIB_010:def 14;
then g.e0 = e by A6, GLIB_000:def 21;
hence e in rng g by A8, FUNCT_1:def 3;
end;
then the_Edges_of G2 c= rng g by TARSKI:def 3;
then rng g = the_Edges_of G2 by XBOOLE_0:def 10;
hence thesis by A2, GLIB_010:def 12;
end;
theorem
for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2
st f is continuous one-to-one holds PVM2PGM(f) is semi-continuous
proof
let G1, G2 be non-multi _Graph, f be PVertexMapping of G1, G2;
assume A1: f is continuous one-to-one;
set g = (PVM2PGM f)_E;
now
let e,v,w be object;
assume A2: e in dom g & v in dom (PVM2PGM f)_V & w in dom (PVM2PGM f)_V;
assume A3: g.e Joins (PVM2PGM f)_V.v,(PVM2PGM f)_V.w,G2;
then g.e Joins f.v,f.w,G2;
then consider e0 being object such that
A4: e0 Joins v,w,G1 by A1, A2, Th2;
e0 in G1.edgesBetween(dom f) by A2, A4, GLIB_000:32;
then A5: e0 in dom g by Def10;
then g.e0 Joins (PVM2PGM f)_V.v,(PVM2PGM f)_V.w,G2 by A2, A4, GLIB_010:4;
then A6: g.e0 = g.e by A3, GLIB_000:def 20;
PVM2PGM(f) is one-to-one by A1, Th34;
hence e Joins v,w,G1 by A2, A4, A5, A6, FUNCT_1:def 4;
end;
hence thesis by GLIB_010:def 15;
end;
theorem Th39:
for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2
st f is continuous holds PVM2PGM(f) is continuous
proof
let G1, G2 be non-multi _Graph, f be PVertexMapping of G1, G2;
assume A1: f is continuous;
now
let e9,v,w be object;
assume A2: v in dom (PVM2PGM f)_V & w in dom (PVM2PGM f)_V;
assume A3: e9 Joins (PVM2PGM f)_V.v,(PVM2PGM f)_V.w,G2;
then consider e being object such that
A4: e Joins v,w,G1 by A1, A2, Th2;
take e;
thus e Joins v,w,G1 by A4;
e in G1.edgesBetween(dom (PVM2PGM f)_V) by A2, A4, GLIB_000:32;
hence e in dom (PVM2PGM f)_E by Def10;
then (PVM2PGM f)_E.e Joins (PVM2PGM f)_V.v,(PVM2PGM f)_V.w,G2
by A2, A4, GLIB_010:4;
hence (PVM2PGM f)_E.e = e9 by A3, GLIB_000:def 20;
end;
hence thesis by GLIB_010:def 16;
end;
theorem
for G1, G2 being non-Dmulti _Graph, f being directed PVertexMapping of G1, G2
st f is one-to-one holds DPVM2PGM(f) is semi-Dcontinuous semi-continuous
proof
let G1, G2 be non-Dmulti _Graph, f be directed PVertexMapping of G1, G2;
assume f is one-to-one;
then DPVM2PGM(f) is one-to-one by Th35;
hence thesis;
end;
theorem Th41:
for G1, G2 being non-Dmulti _Graph, f being directed PVertexMapping of G1, G2
st f is Dcontinuous holds DPVM2PGM(f) is Dcontinuous
proof
let G1, G2 be non-Dmulti _Graph, f be directed PVertexMapping of G1, G2;
assume A1: f is Dcontinuous;
now
let e9,v,w be object;
assume A2: v in dom (DPVM2PGM f)_V & w in dom (DPVM2PGM f)_V;
then reconsider v0 = v, w0 = w as Vertex of G1;
assume A3: e9 DJoins (DPVM2PGM f)_V.v,(DPVM2PGM f)_V.w,G2;
then consider e being object such that
A4: e DJoins v,w,G1 by A1, A2;
take e;
thus e DJoins v,w,G1 by A4;
e Joins v,w,G1 by A4, GLIB_000:16;
then e in G1.edgesBetween(dom (DPVM2PGM f)_V) by A2, GLIB_000:32;
hence e in dom (DPVM2PGM f)_E by Def11;
then (DPVM2PGM f)_E.e DJoins (DPVM2PGM f)_V.v,(DPVM2PGM f)_V.w,G2
by A2, A4, GLIB_010:def 14;
hence (DPVM2PGM f)_E.e = e9 by A3, GLIB_000:def 21;
end;
hence thesis by GLIB_010:def 18;
end;
theorem
for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2
st f is one-to-one holds PVM2PGM(f) is one-to-one by Th34;
theorem
for G1, G2 being non-Dmulti _Graph, f being directed PVertexMapping of G1, G2
st f is one-to-one holds DPVM2PGM(f) is one-to-one by Th35;
theorem
for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2
st f is total one-to-one holds PVM2PGM(f) is weak_SG-embedding
proof
let G1, G2 be non-multi _Graph, f being PVertexMapping of G1, G2;
assume f is total one-to-one;
then PVM2PGM(f) is total one-to-one by Th32, Th34;
hence thesis;
end;
theorem
for G1, G2 being non-Dmulti _Graph, f being directed PVertexMapping of G1, G2
st f is total one-to-one holds DPVM2PGM(f) is weak_SG-embedding
proof
let G1, G2 be non-Dmulti _Graph, f being directed PVertexMapping of G1, G2;
assume f is total one-to-one;
then DPVM2PGM(f) is total one-to-one by Th33, Th35;
hence thesis;
end;
theorem
for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2
st f is total one-to-one continuous holds PVM2PGM(f) is strong_SG-embedding
proof
let G1, G2 be non-multi _Graph, f being PVertexMapping of G1, G2;
assume f is total one-to-one continuous;
then PVM2PGM(f) is total one-to-one continuous by Th32, Th34, Th39;
hence thesis;
end;
theorem Th47:
for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2
st f is isomorphism holds PVM2PGM(f) is isomorphism
proof
let G1, G2 be non-multi _Graph, f being PVertexMapping of G1, G2;
assume f is isomorphism;
then PVM2PGM(f) is total one-to-one onto by Th32, Th34, Th36;
hence thesis;
end;
theorem Th48:
for G1, G2 being non-Dmulti _Graph, f being directed PVertexMapping of G1, G2
st f is Disomorphism holds DPVM2PGM(f) is Disomorphism
proof
let G1, G2 be non-Dmulti _Graph, f be directed PVertexMapping of G1, G2;
assume f is Disomorphism;
then DPVM2PGM(f) is total one-to-one onto Dcontinuous
by Th33, Th35, Th37, Th41;
hence thesis;
end;
theorem
for G1, G2 being non-multi _Graph holds G2 is G1-isomorphic iff
ex f being PVertexMapping of G1, G2 st f is isomorphism
proof
let G1, G2 be non-multi _Graph;
hereby
assume G2 is G1-isomorphic;
then consider F being PGraphMapping of G1, G2 such that
A1: F is isomorphism by GLIB_010:def 23;
consider f being PVertexMapping of G1, G2 such that
A2: F_V = f & f is isomorphism by A1, Th25;
take f;
thus f is isomorphism by A2;
end;
given f being PVertexMapping of G1, G2 such that
A3: f is isomorphism;
PVM2PGM f is isomorphism by A3, Th47;
hence thesis by GLIB_010:def 23;
end;
theorem
for G1, G2 being non-Dmulti _Graph holds G2 is G1-Disomorphic iff
ex f being directed PVertexMapping of G1, G2 st f is Disomorphism
proof
let G1, G2 be non-Dmulti _Graph;
hereby
assume G2 is G1-Disomorphic;
then consider F being PGraphMapping of G1, G2 such that
A1: F is Disomorphism by GLIB_010:def 24;
consider f being directed PVertexMapping of G1, G2 such that
A2: F_V = f & f is Disomorphism by A1, Th26;
take f;
thus f is Disomorphism by A2;
end;
given f being directed PVertexMapping of G1, G2 such that
A3: f is Disomorphism;
DPVM2PGM f is Disomorphism by A3, Th48;
hence thesis by GLIB_010:def 24;
end;