:: About Regular Graphs
:: by Sebastian Koch
::
:: Received June 30, 2023
:: Copyright (c) 2023-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 SUBSET_1, RELAT_1, FUNCT_1, XXREAL_0, TARSKI, ARYTM_3, CARD_1,
XBOOLE_0, NAT_1, ARYTM_1, GLIB_000, PARTFUN1, FINSET_1, ZFMISC_1,
FUNCOP_1, GLIB_009, MOD_4, GLIB_006, GLIB_007, FUNCT_4, CARD_2, SCMYCIEL,
GLIB_010, SIMPLEX0, XCMPLX_0, GLIB_013, SETFAM_1, RELAT_2, REWRITE1,
ORDINAL1, FINSEQ_1, GLIB_012, GLIB_001, GLIB_002, WELLORD2, PBOOLE,
GRAPH_1, TAXONOM2, EQREL_1, CHORD, FUNCT_7, AOFA_I00, CARD_3, VALUED_0,
NUMBERS, AFINSQ_1, ABIAN, PRGCOR_2, INT_1, GLIB_014, GLUNIR00, GLIB_016,
CARD_5;
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,
FUNCT_3, FUNCOP_1, FUNCT_4, FINSET_1, CARD_1, PBOOLE, CARD_3, NUMBERS,
XCMPLX_0, XXREAL_0, ABIAN, VALUED_0, ORDERS_1, RELAT_2, NAT_D, CARD_2,
FINSEQ_1, EQREL_1, VALUED_1, RVSUM_1, AFINSQ_1, AFINSQ_2, GLIB_000,
TAXONOM2, GLIB_001, GLIB_002, CHORD, AOFA_I00, GLIB_006, GLIB_007,
GLIB_008, GLIB_009, GLIB_010, GLIB_012, GLIB_013, GLIB_014, GLUNIR00;
constructors DOMAIN_1, FUNCT_4, CARD_2, GLIB_002, CHORD, GLIB_007, GLIB_008,
GLIB_009, GLIB_010, GLIB_012, GLIB_013, NAT_D, TAXONOM2, CARD_3,
AFINSQ_2, WSIERP_1, RECDEF_1, RVSUM_4, GLIB_014, GLUNIR00;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XREAL_0, NAT_1,
GLIB_000, CARD_1, GLIB_002, GLIB_008, GLIB_010, GLIBPRE0, GLIB_013,
MSAFREE5, CARD_2, RELSET_1, GLIB_001, CARD_5, FUNCT_3, SUBSET_1, FUNCT_2,
FUNCOP_1, AFINSQ_1, AFINSQ_2, VALUED_0, FUNCT_4, GLUNIR00, RELAT_2,
GLIB_009, GLIB_012, COUNTERS, INT_1;
requirements ARITHM, BOOLE, NUMERALS, SUBSET, REAL;
equalities GLIB_000, GLUNIR00, ORDINAL1;
theorems TARSKI, XBOOLE_0, XBOOLE_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
ZFMISC_1, CARD_1, CARD_2, CARD_3, ABIAN, FUNCT_3, BINOP_1, XTUPLE_0,
FUNCT_4, ENUMSET1, TAXONOM2, MCART_1, NAT_1, NAT_D, XXREAL_0, XREAL_1,
POLYFORM, GLIB_000, GLIB_001, GLIB_002, CHORD, GLIB_008, GLIB_009,
GLIB_010, GLIBPRE0, GLIB_012, GLIB_013, FUNCOP_1, FUNCTOR0, ORDINAL1,
EQREL_1, SETFAM_1, SUBSET_1, PBOOLE, VALUED_0, VALUED_1, RVSUM_4,
AFINSQ_1, FINSEQ_3, NAT_2, NUMERAL1, AFINSQ_2, WELLORD2, GLIB_007,
ORDINAL2, ORDINAL6, RAMSEY_1, GLIB_006, GLIB_014, RELSET_1, GLUNIR00,
GLIBPRE1;
schemes FUNCT_1, PBOOLE, MSAFREE5, AFINSQ_2;
begin :: Directed-complete Graphs
definition
let G be _Graph;
attr G is Dcomplete means
:Def1:
for v,w being Vertex of G st v <> w ex e being object st e DJoins v,w,G;
end;
definition
let c be non empty Cardinal;
func canCompleteGraph(c) -> _Graph equals
createGraph(c, RelIncl c \ id c);
coherence;
func canDCompleteGraph(c) -> _Graph equals
createGraph(c, [: c, c :] \ id c);
coherence;
end;
registration
let c be non empty Cardinal;
reduce the_Vertices_of canCompleteGraph(c) to c;
correctness;
reduce the_Vertices_of canDCompleteGraph(c) to c;
correctness;
end;
registration
let c be non empty Cardinal;
cluster -> ordinal for Vertex of canCompleteGraph(c);
coherence;
cluster -> ordinal for Vertex of canDCompleteGraph(c);
coherence;
end;
registration
cluster -> natural for Vertex of canCompleteGraph(omega);
coherence;
cluster -> natural for Vertex of canDCompleteGraph(omega);
coherence;
let n be non zero Nat;
cluster canCompleteGraph(n) -> _finite;
coherence;
cluster canDCompleteGraph(n) -> _finite;
coherence;
cluster -> natural for Vertex of canCompleteGraph(n);
coherence
proof
let k be Vertex of canCompleteGraph(n);
k c= n by ORDINAL1:def 2;
hence thesis;
end;
cluster -> natural for Vertex of canDCompleteGraph(n);
coherence
proof
let k be Vertex of canDCompleteGraph(n);
k c= n by ORDINAL1:def 2;
hence thesis;
end;
end;
registration
let c be non empty Cardinal;
cluster canCompleteGraph(c) -> plain c-vertex simple complete;
coherence
proof
thus canCompleteGraph(c) is plain c-vertex;
RelIncl c \ id c misses id c by XBOOLE_1:79;
then RelIncl c \ id c is irreflexive by GLIBPRE0:11;
then canCompleteGraph(c) is loopless;
hence canCompleteGraph(c) is simple;
now
let v,w be Vertex of canCompleteGraph(c);
assume v <> w;
then A1: not [v,w] in id c & not [w,v] in id c by RELAT_1:def 10;
per cases by ORDINAL1:16;
suppose v c= w;
then [v,w] in RelIncl c by WELLORD2:def 1;
then [v,w] in RelIncl c \ id c by A1, XBOOLE_0:def 5;
then [v,w] DJoins v,w,canCompleteGraph(c) by GLUNIR00:63;
then [v,w] Joins v,w,canCompleteGraph(c) by GLIB_000:16;
hence v,w are_adjacent by CHORD:def 3;
end;
suppose w in v;
then w c= v by ORDINAL1:def 2;
then [w,v] in RelIncl c by WELLORD2:def 1;
then [w,v] in RelIncl c \ id c by A1, XBOOLE_0:def 5;
then [w,v] DJoins w,v,canCompleteGraph(c) by GLUNIR00:63;
then [w,v] Joins v,w,canCompleteGraph(c) by GLIB_000:16;
hence v,w are_adjacent by CHORD:def 3;
end;
end;
hence thesis by CHORD:def 6;
end;
cluster canDCompleteGraph(c) -> plain c-vertex Dsimple Dcomplete;
coherence
proof
thus canDCompleteGraph(c) is plain c-vertex;
[: c, c :] \ id c misses id c by XBOOLE_1:79;
then [: c, c :] \ id c is irreflexive by GLIBPRE0:11;
hence canDCompleteGraph(c) is Dsimple;
now
let v,w be Vertex of canDCompleteGraph(c);
assume v <> w;
then A2: not [v,w] in id c by RELAT_1:def 10;
reconsider e = [v,w] as object;
take e;
[v,w] in [: c, c :] \ id c by A2, XBOOLE_0:def 5;
hence e DJoins v,w,canDCompleteGraph(c) by GLUNIR00:63;
end;
hence thesis;
end;
end;
theorem Th1:
for c being non empty Cardinal, v being Vertex of canCompleteGraph(c)
holds v.inNeighbors() = v & v.outNeighbors() = c \ succ v
proof
let c be non empty Cardinal, v be Vertex of canCompleteGraph(c);
now
let x be object;
hereby
assume A1: x in v.inNeighbors();
then reconsider a = x as Ordinal;
consider e being object such that
A2: e DJoins x,v,canCompleteGraph(c) by A1, GLIB_000:69;
e = [x,v] by A2, GLUNIR00:64;
then [x,v] in RelIncl c \ id c by A2, GLUNIR00:63;
then [x,v] in RelIncl c by XBOOLE_0:def 5;
then A3: a c= v by ORDINAL6:8;
x <> v by A2, GLIB_000:136;
then not v c= a by A3, XBOOLE_0:def 10;
then a in v by ORDINAL1:16;
hence x in v;
end;
assume A4: x in v;
then reconsider a = x as Vertex of canCompleteGraph(c) by ORDINAL1:10;
a <> v
proof
assume a = v;
then v in v by A4;
hence contradiction;
end;
then a c= v & a <> v by A4, ORDINAL1:def 2;
then [a,v] in RelIncl c & not [a,v] in id c
by WELLORD2:def 1, RELAT_1:def 10;
then [a,v] in RelIncl c \ id c by XBOOLE_0:def 5;
hence x in v.inNeighbors() by GLIB_000:69, GLUNIR00:63;
end;
hence v.inNeighbors() = v by TARSKI:2;
now
let x be object;
hereby
assume A5: x in v.outNeighbors();
then reconsider a = x as Vertex of canCompleteGraph(c);
consider e being object such that
A6: e DJoins v,x,canCompleteGraph(c) by A5, GLIB_000:70;
e = [v,x] by A6, GLUNIR00:64;
then [v,x] in RelIncl c \ id c by A6, GLUNIR00:63;
then [v,x] in RelIncl c by XBOOLE_0:def 5;
then A7: v c= a by ORDINAL6:8;
x <> v by A6, GLIB_000:136;
then not a c= v by A7, XBOOLE_0:def 10;
then not succ a c= succ v by ORDINAL2:1;
then not a in succ v by ORDINAL1:21;
hence x in c \ succ v by XBOOLE_0:def 5;
end;
assume x in c \ succ v;
then A8: x in c & not x in succ v by XBOOLE_0:def 5;
then reconsider a = x as Vertex of canCompleteGraph(c);
not succ a c= succ v by A8, ORDINAL1:21;
then A9: v in a & v <> a by ORDINAL1:16, ORDINAL2:1;
then v c= a by ORDINAL1:def 2;
then [v,a] in RelIncl c & not [v,a] in id c
by A9, WELLORD2:def 1, RELAT_1:def 10;
then [v,a] in RelIncl c \ id c by XBOOLE_0:def 5;
hence x in v.outNeighbors() by GLIB_000:70, GLUNIR00:63;
end;
hence thesis by TARSKI:2;
end;
theorem
for v being Vertex of canCompleteGraph(omega)
holds v.inDegree() = v & v.outDegree() = omega
proof
let v be Vertex of canCompleteGraph(omega);
thus v.inDegree() = card v.inNeighbors() by GLIB_000:109
.= card v by Th1
.= v;
A1: omega \ succ v is infinite by RAMSEY_1:4;
thus v.outDegree() = card v.outNeighbors() by GLIB_000:110
.= card(omega\succ v) by Th1
.= omega by A1, RAMSEY_1:2;
end;
theorem
for n being non zero Nat, v being Vertex of canCompleteGraph(n)
holds v.inDegree() = v & v.outDegree() = n - v - 1
proof
let n be non zero Nat, v be Vertex of canCompleteGraph(n);
thus v.inDegree() = card v.inNeighbors() by GLIB_000:109
.= card v by Th1
.= v;
thus v.outDegree() = card v.outNeighbors() by GLIB_000:110
.= card(n\succ v) by Th1
.= n - card succ Segm v by ORDINAL1:21, CARD_2:44
.= n - card Segm(v+1) by NAT_1:38
.= n - v - 1;
end;
registration
let c be non empty Cardinal;
cluster simple c-vertex complete for _Graph;
existence
proof
take canCompleteGraph(c);
thus thesis;
end;
cluster Dsimple c-vertex Dcomplete for _Graph;
existence
proof
take canDCompleteGraph(c);
thus thesis;
end;
end;
registration
cluster Dcomplete -> complete for _Graph;
coherence
proof
let G be _Graph;
assume A1: G is Dcomplete;
now
let v,w be Vertex of G;
assume v <> w;
then consider e being object such that
A2: e DJoins v,w,G by A1;
e Joins v,w,G by A2, GLIB_000:16;
hence v,w are_adjacent by CHORD:def 3;
end;
hence thesis by CHORD:def 6;
end;
cluster _trivial -> Dcomplete for _Graph;
coherence by GLIB_000:116;
cluster non _trivial Dcomplete -> non non-multi non edgeless for _Graph;
coherence
proof
let G be _Graph;
assume A3: G is non _trivial Dcomplete;
then consider v,w being Vertex of G such that
A4: v <> w by GLIB_000:21;
consider e1 being object such that
A5: e1 DJoins v,w,G by A3, A4;
consider e2 being object such that
A6: e2 DJoins w,v,G by A3, A4;
A7: e1 <> e2
proof
assume e1 = e2;
then (the_Source_of G).e2 = v & (the_Source_of G).e2 = w
by A5, A6, GLIB_000:def 14;
hence contradiction by A4;
end;
e1 Joins v,w,G & e2 Joins v,w,G by A5, A6, GLIB_000:16;
hence thesis by A7, GLIB_000:def 20;
end;
end;
registration
cluster non Dcomplete for _Graph;
existence
proof
take the non-multi non _trivial _Graph;
thus thesis;
end;
end;
theorem Th4:
for G1, G2 being _Graph st G1 == G2 & G1 is Dcomplete holds G2 is Dcomplete
proof
let G1, G2 be _Graph;
assume A1: G1 == G2 & G1 is Dcomplete;
let v,w be Vertex of G2;
A2: v is Vertex of G1 & w is Vertex of G1 by A1, GLIB_000:def 34;
assume v <> w;
then consider e being object such that
A3: e DJoins v,w,G1 by A1, A2;
take e;
thus e DJoins v,w,G2 by A1, A3, GLIB_000:88;
end;
theorem Th5:
for G1 being _Graph, G2 being removeLoops of G1
holds G1 is Dcomplete iff G2 is Dcomplete
proof
let G1 be _Graph, G2 be removeLoops of G1;
hereby
assume A1: G1 is Dcomplete;
now
let v,w be Vertex of G2;
A2: v is Vertex of G1 & w is Vertex of G1 by GLIB_000:def 33;
assume A3: v <> w;
then consider e being object such that
A4: e DJoins v,w,G1 by A1, A2;
take e;
e Joins v,w,G1 by A4, GLIB_000:16;
then A5: not e in G1.loops() by A3, GLIB_009:46;
e in the_Edges_of G1 by A4, GLIB_000:def 14;
then e in the_Edges_of G1 \ G1.loops() by A5, XBOOLE_0:def 5;
then e in the_Edges_of G2 by GLIB_000:53;
hence e DJoins v,w,G2 by A4, GLIB_000:73;
end;
hence G2 is Dcomplete;
end;
assume A6: G2 is Dcomplete;
let v,w be Vertex of G1;
A7: v is Vertex of G2 & w is Vertex of G2 by GLIB_000:def 33;
assume v <> w;
then consider e being object such that
A8: e DJoins v,w,G2 by A6, A7;
take e;
thus e DJoins v,w,G1 by A8, GLIB_000:72;
end;
theorem Th6:
for G1 being _Graph, G2 being removeDParallelEdges of G1
holds G1 is Dcomplete iff G2 is Dcomplete
proof
let G1 be _Graph, G2 be removeDParallelEdges of G1;
hereby
assume A1: G1 is Dcomplete;
now
let v,w be Vertex of G2;
A2: v is Vertex of G1 & w is Vertex of G1 by GLIB_000:def 33;
assume v <> w;
then consider e0 being object such that
A3: e0 DJoins v,w,G1 by A1, A2;
consider E being RepDEdgeSelection of G1 such that
A4: G2 is inducedSubgraph of G1,the_Vertices_of G1,E by GLIB_009:def 8;
consider e being object such that
A5: e DJoins v,w,G1 & e in E and
for e9 being object st e9 DJoins v,w,G1 & e9 in E holds e9 = e
by A3, GLIB_009:def 6;
take e;
the_Vertices_of G1 c= the_Vertices_of G1;
then the_Vertices_of G1 is non empty Subset of the_Vertices_of G1 &
G1.edgesBetween(the_Vertices_of G1) = the_Edges_of G1 by GLIB_000:34;
then the_Edges_of G2 = E by A4, GLIB_000:def 37;
hence e DJoins v,w,G2 by A5, GLIB_000:73;
end;
hence G2 is Dcomplete;
end;
assume A6: G2 is Dcomplete;
let v,w be Vertex of G1;
A7: v is Vertex of G2 & w is Vertex of G2 by GLIB_000:def 33;
assume v <> w;
then consider e being object such that
A8: e DJoins v,w,G2 by A6, A7;
take e;
thus e DJoins v,w,G1 by A8, GLIB_000:72;
end;
theorem Th7:
for G1 being _Graph, G2 being DSimpleGraph of G1
holds G1 is Dcomplete iff G2 is Dcomplete
proof
let G1 be _Graph, G2 be DSimpleGraph of G1;
consider G9 being removeDParallelEdges of G1 such that
A1: G2 is removeLoops of G9 by GLIB_009:120;
hereby
assume G1 is Dcomplete;
then G9 is Dcomplete by Th6;
hence G2 is Dcomplete by A1, Th5;
end;
assume G2 is Dcomplete;
then G9 is Dcomplete by A1, Th5;
hence thesis by Th6;
end;
Lm1:
for G1 being _Graph, G2 being reverseEdgeDirections of G1
holds G1 is Dcomplete implies G2 is Dcomplete
proof
let G1 be _Graph, G2 be reverseEdgeDirections of G1;
assume A1: G1 is Dcomplete;
let v,w be Vertex of G2;
A2: v is Vertex of G1 & w is Vertex of G1 by GLIB_007:4;
assume v <> w;
then consider e being object such that
A3: e DJoins w,v,G1 by A1, A2;
take e;
e in the_Edges_of G1 by A3, GLIB_000:def 14;
hence e DJoins v,w,G2 by A3, GLIB_007:7;
end;
theorem Th8:
for G1 being _Graph, G2 being reverseEdgeDirections of G1
holds G1 is Dcomplete iff G2 is Dcomplete
proof
let G1 be _Graph, G2 be reverseEdgeDirections of G1;
thus G1 is Dcomplete implies G2 is Dcomplete by Lm1;
G1 is reverseEdgeDirections of G2, the_Edges_of G1 by GLIB_007:3;
then G1 is reverseEdgeDirections of G2 by GLIB_007:4;
hence thesis by Lm1;
end;
registration
let G be Dcomplete _Graph;
cluster -> Dcomplete for removeLoops of G;
coherence by Th5;
cluster -> Dcomplete for removeDParallelEdges of G;
coherence by Th6;
cluster -> Dcomplete for DSimpleGraph of G;
coherence by Th7;
cluster -> Dcomplete for reverseEdgeDirections of G;
coherence by Th8;
let V be set;
cluster -> Dcomplete for inducedSubgraph of G, V;
coherence
proof
let H be inducedSubgraph of G, V;
per cases;
suppose V is non empty Subset of the_Vertices_of G;
then A1: the_Vertices_of H = V & the_Edges_of H = G.edgesBetween(V)
by GLIB_000:def 37;
let v,w be Vertex of H;
assume A2: v <> w;
the_Vertices_of H c= the_Vertices_of G;
then reconsider v9 = v, w9 = w as Vertex of G by TARSKI:def 3;
consider e being object such that
A3: e DJoins v9,w9,G by A2, Def1;
take e;
e Joins v9,w9,G & v9 in V & w9 in V by A1, A3, GLIB_000:16;
then e in the_Edges_of H & e is set by A1, GLIB_000:32, TARSKI:1;
hence e DJoins v,w,H by A3, GLIB_000:73;
end;
suppose not(V is non empty Subset of the_Vertices_of G);
then G == H by GLIB_000:def 37;
hence thesis by Th4;
end;
end;
cluster -> Dcomplete for addLoops of G, V;
coherence
proof
let H be addLoops of G, V;
let v,w be Vertex of H;
reconsider v9=v, w9=w as Vertex of G by GLIB_012:15;
assume A4: v <> w;
then consider e being object such that
A5: e DJoins v9,w9,G by Def1;
take e;
thus e DJoins v,w,H by A4, A5, GLIB_012:16;
end;
end;
registration
let G be Dcomplete _Graph, v,e,w be object;
cluster -> Dcomplete for addEdge of G,v,e,w;
coherence
proof
let H be addEdge of G,v,e,w;
per cases;
suppose v in the_Vertices_of G & w in the_Vertices_of G &
not e in the_Edges_of G;
then A1: the_Vertices_of G = the_Vertices_of H by GLIB_006:def 11;
let v1,w1 be Vertex of H;
reconsider v2=v1, w2=w1 as Vertex of G by A1;
assume v1 <> w1;
then consider e being object such that
A2: e DJoins v2,w2,G by Def1;
take e;
thus e DJoins v1,w1,H by A2, GLIB_006:70;
end;
suppose not(v in the_Vertices_of G & w in the_Vertices_of G &
not e in the_Edges_of G);
then G == H by GLIB_006:def 11;
hence thesis by Th4;
end;
end;
end;
registration
let G be non Dcomplete _Graph;
cluster -> non Dcomplete for removeLoops of G;
coherence by Th5;
cluster -> non Dcomplete for removeDParallelEdges of G;
coherence by Th6;
cluster -> non Dcomplete for DSimpleGraph of G;
coherence by Th7;
cluster -> non Dcomplete for reverseEdgeDirections of G;
coherence by Th8;
cluster spanning -> non Dcomplete for Subgraph of G;
coherence
proof
let H be Subgraph of G;
consider v,w being Vertex of G such that
A1: v <> w & for e being object holds not e DJoins v,w,G by Def1;
assume H is spanning;
then reconsider v9=v, w9=w as Vertex of H by GLIB_000:def 33;
take v9,w9;
thus v9 <> w9 by A1;
let e be object;
thus not e DJoins v9,w9,H by A1, GLIB_000:72;
end;
end;
theorem Th9:
for G1, G2 being _Graph, F being PGraphMapping of G1,G2
st F is Dcontinuous strong_SG-embedding
holds G2 is Dcomplete implies G1 is Dcomplete
proof
let G1, G2 be _Graph, F be PGraphMapping of G1,G2;
assume A1: F is Dcontinuous strong_SG-embedding & G2 is Dcomplete;
let v,w be Vertex of G1;
assume A2: v <> w;
dom F_V = the_Vertices_of G1 by A1, GLIB_010:def 11;
then A3: v in dom F_V & w in dom F_V;
then A4: F_V.v = F_V/.v & F_V.w = F_V/.w by PARTFUN1:def 6;
then F_V/.v <> F_V/.w by A1, A2, A3, FUNCT_1:def 4;
then consider e9 being object such that
A5: e9 DJoins F_V/.v,F_V/.w,G2 by A1;
e9 DJoins F_V.v,F_V.w,G2 by A4, A5;
then consider e being object such that
A6: e DJoins v,w,G1 & e in dom F_E & F_E.e = e9 by A1, A3, GLIB_010:def 18;
take e;
thus thesis by A6;
end;
theorem Th10:
for G1, G2 being _Graph, F being PGraphMapping of G1,G2
st F is Disomorphism holds G1 is Dcomplete iff G2 is Dcomplete
proof
let G1, G2 be _Graph, F be PGraphMapping of G1,G2;
assume A1: F is Disomorphism;
then reconsider F0 = F as one-to-one PGraphMapping of G1, G2;
F0" is isomorphism Dcontinuous by A1, GLIB_010:74, GLIB_010:75;
hence G1 is Dcomplete implies G2 is Dcomplete by Th9;
thus G2 is Dcomplete implies G1 is Dcomplete by A1, Th9;
end;
registration
let G be Dcomplete _Graph;
cluster G-Disomorphic -> Dcomplete for _Graph;
coherence
proof
let H be _Graph;
assume H is G-Disomorphic;
then consider F being PGraphMapping of G, H such that
A1: F is Disomorphism by GLIB_010:def 24;
thus thesis by A1, Th10;
end;
end;
theorem Th11:
for G being Dcomplete _Graph, v being Vertex of G holds
the_Vertices_of G \ {v} c= v.inNeighbors() &
the_Vertices_of G \ {v} c= v.outNeighbors() &
the_Vertices_of G \ {v} c= v.allNeighbors()
proof
let G being Dcomplete _Graph, v be Vertex of G;
A1: now
let x be object;
assume x in the_Vertices_of G \ {v};
then A2: x in the_Vertices_of G & x <> v by ZFMISC_1:56;
then reconsider w = x as Vertex of G;
ex e being object st e DJoins w,v,G by A2, Def1;
hence x in v.inNeighbors() by GLIB_000:69;
consider e being object such that
A3: e DJoins v,w,G by A2, Def1;
thus x in v.outNeighbors() by A3, GLIB_000:70;
e Joins v,w,G by A3, GLIB_000:16;
hence x in v.allNeighbors() by GLIB_000:71;
end;
then for x being object st x in the_Vertices_of G \ {v}
holds x in v.inNeighbors();
hence the_Vertices_of G \ {v} c= v.inNeighbors() by TARSKI:def 3;
for x being object st x in the_Vertices_of G \ {v}
holds x in v.outNeighbors() by A1;
hence the_Vertices_of G \ {v} c= v.outNeighbors() by TARSKI:def 3;
for x being object st x in the_Vertices_of G \ {v}
holds x in v.allNeighbors() by A1;
hence the_Vertices_of G \ {v} c= v.allNeighbors() by TARSKI:def 3;
end;
theorem Th12:
for G being loopless Dcomplete _Graph, v being Vertex of G holds
v.inNeighbors() = the_Vertices_of G \ {v} &
v.outNeighbors() = the_Vertices_of G \ {v} &
v.allNeighbors() = the_Vertices_of G \ {v}
proof
let G be loopless Dcomplete _Graph, v be Vertex of G;
A1: the_Vertices_of G \ {v} c= v.inNeighbors() &
the_Vertices_of G \ {v} c= v.outNeighbors() &
the_Vertices_of G \ {v} c= v.allNeighbors() by Th11;
A2: v.inNeighbors() c= the_Vertices_of G \ {v} &
v.outNeighbors() c= the_Vertices_of G \ {v} &
v.allNeighbors() c= the_Vertices_of G \ {v} by GLIB_000:175;
thus v.inNeighbors() = the_Vertices_of G \ {v} by A1, A2, XBOOLE_0:def 10;
thus v.outNeighbors() = the_Vertices_of G \ {v} by A1, A2, XBOOLE_0:def 10;
thus v.allNeighbors() = the_Vertices_of G \ {v} by A1, A2, XBOOLE_0:def 10;
end;
theorem Th13:
for G being Dsimple Dcomplete _Graph, v being Vertex of G
holds v.inDegree()+`1 = G.order() & v.outDegree()+`1 = G.order()
proof
let G be Dsimple Dcomplete _Graph, v be Vertex of G;
v in {v} by TARSKI:def 1;
then A1: not v in the_Vertices_of G \ {v} by XBOOLE_0:def 5;
then not v in v.inNeighbors() by Th12;
then A2: v.inNeighbors() misses {v} by ZFMISC_1:50;
thus v.inDegree()+`1 = v.inDegree() +` card {v} by CARD_1:30
.= card v.inNeighbors() +` card {v} by GLIB_000:109
.= card (v.inNeighbors() \/ {v}) by A2, CARD_2:35
.= card (the_Vertices_of G \ {v} \/ {v}) by Th12
.= G.order() by ZFMISC_1:116;
not v in v.outNeighbors() by A1, Th12;
then A3: v.outNeighbors() misses {v} by ZFMISC_1:50;
thus v.outDegree()+`1 = v.outDegree() +` card {v} by CARD_1:30
.= card v.outNeighbors() +` card {v} by GLIB_000:110
.= card (v.outNeighbors() \/ {v}) by A3, CARD_2:35
.= card (the_Vertices_of G \ {v} \/ {v}) by Th12
.= G.order() by ZFMISC_1:116;
end;
:: more general version of GLIB_012:57
theorem Th14:
for G1 being _Graph, G2 being DLGraphComplement of G1
holds the_Edges_of G1 = G1.loops() iff G2 is Dcomplete
proof
let G1 be _Graph, G2 be DLGraphComplement of G1;
hereby
assume A1: the_Edges_of G1 = G1.loops();
now
let v2,w2 be Vertex of G2;
reconsider v1=v2,w1=w2 as Vertex of G1 by GLIB_012:def 6;
assume A2: v2 <> w2;
not ex e1 being object st e1 DJoins v1,w1,G1
proof
given e1 being object such that
A3: e1 DJoins v1,w1,G1;
e1 Joins v1,w1,G1 by A3, GLIB_000:16;
then not e1 in G1.loops() by A2, GLIB_009:46;
hence contradiction by A1, A3, GLIB_000:def 14;
end;
hence ex e2 being object st e2 DJoins v2,w2,G2 by GLIB_012:def 6;
end;
hence G2 is Dcomplete;
end;
assume A4: G2 is Dcomplete;
now
let e be object;
set v1 = (the_Source_of G1).e, w1 = (the_Target_of G1).e;
assume e in the_Edges_of G1;
then A5: e DJoins v1,w1,G1 by GLIB_000:def 14;
then e Joins v1,w1,G1 by GLIB_000:16;
then reconsider v1,w1 as Vertex of G1 by GLIB_000:13;
reconsider v2=v1, w2=w1 as Vertex of G2 by GLIB_012:def 6;
v1 = w1
proof
assume A6: v1 <> w1;
not ex e2 being object st e2 DJoins v2,w2,G2 by A5, GLIB_012:def 6;
hence contradiction by A4, A6;
end;
hence e in G1.loops() by A5, GLIB_009:45;
end;
then the_Edges_of G1 c= G1.loops() by TARSKI:def 3;
hence thesis by XBOOLE_0:def 10;
end;
registration
let G be edgeless _Graph;
cluster -> Dcomplete for DLGraphComplement of G;
coherence
proof
let H be DLGraphComplement of G;
the_Edges_of G = {} & G.loops() = {};
hence thesis by Th14;
end;
end;
:: directed version of GLIB_012:75
:: Proof copied from the reverse version and reordered
theorem Th15:
for G1 being _Graph, G2 being DLGraphComplement of G1
holds G1 is Dcomplete iff the_Edges_of G2 = G2.loops()
proof
let G1 be _Graph, G2 be DLGraphComplement of G1;
hereby
assume A1: G1 is Dcomplete;
now
let e be object;
set v1 = (the_Source_of G2).e, w1 = (the_Target_of G2).e;
assume e in the_Edges_of G2;
then A2: e DJoins v1,w1,G2 by GLIB_000:def 14;
then e Joins v1,w1,G2 by GLIB_000:16;
then reconsider v1,w1 as Vertex of G2 by GLIB_000:13;
reconsider v2=v1, w2=w1 as Vertex of G1 by GLIB_012:def 6;
v1 = w1
proof
assume A3: v1 <> w1;
not ex e2 being object st e2 DJoins v2,w2,G1
by A2, GLIB_012:def 6;
hence contradiction by A1, A3;
end;
hence e in G2.loops() by A2, GLIB_009:45;
end;
then the_Edges_of G2 c= G2.loops() by TARSKI:def 3;
hence the_Edges_of G2 = G2.loops() by XBOOLE_0:def 10;
end;
assume A4: the_Edges_of G2 = G2.loops();
now
let v2,w2 be Vertex of G1;
reconsider v1=v2,w1=w2 as Vertex of G2 by GLIB_012:def 6;
assume A5: v2 <> w2;
not ex e1 being object st e1 DJoins v1,w1,G2
proof
given e1 being object such that
A6: e1 DJoins v1,w1,G2;
e1 Joins v1,w1,G2 by A6, GLIB_000:16;
then not e1 in G2.loops() by A5, GLIB_009:46;
hence contradiction by A4, A6, GLIB_000:def 14;
end;
hence ex e2 being object st e2 DJoins v2,w2,G1 by GLIB_012:def 6;
end;
hence G1 is Dcomplete;
end;
registration
cluster loopfull Dcomplete for _Graph;
existence
proof
set G = the addLoops of the Dcomplete _Graph;
take G;
thus thesis;
end;
end;
registration
let G be loopfull Dcomplete _Graph;
cluster -> edgeless for DLGraphComplement of G;
coherence
proof
let H be DLGraphComplement of G;
H.loops() = {};
hence thesis by Th15;
end;
end;
:: more general version of GLIB_012:92
:: also directed version of second part of GLIB_012:113
theorem Th16:
for G1 being _Graph, G2 being DGraphComplement of G1
holds the_Edges_of G1 = G1.loops() iff G2 is Dcomplete
proof
let G1 be _Graph, G2 be DGraphComplement of G1;
consider G9 being DLGraphComplement of G1 such that
A1: G2 is removeLoops of G9 by GLIB_012:def 8;
hereby
assume the_Edges_of G1 = G1.loops();
then G9 is Dcomplete by Th14;
hence G2 is Dcomplete by A1;
end;
assume G2 is Dcomplete;
then G9 is Dcomplete by A1;
hence thesis by Th14;
end;
registration
let G be edgeless _Graph;
cluster -> Dcomplete for DGraphComplement of G;
coherence
proof
let H be DGraphComplement of G;
the_Edges_of G = {} & G.loops() = {};
hence thesis by Th16;
end;
end;
:: directed version of first part of GLIB_012:113
theorem Th17:
for G1 being _Graph, G2 being DGraphComplement of G1
holds G1 is Dcomplete iff G2 is edgeless
proof
let G1 be _Graph, G2 be DGraphComplement of G1;
consider G9 being DLGraphComplement of G1 such that
A1: G2 is removeLoops of G9 by GLIB_012:def 8;
hereby
assume G1 is Dcomplete;
then the_Edges_of G9 = G9.loops() by Th15;
hence G2 is edgeless by A1;
end;
assume G2 is edgeless;
then {} = the_Edges_of G2
.= the_Edges_of G9 \ G9.loops() by A1, GLIB_000:53;
then the_Edges_of G9 c= G9.loops() by XBOOLE_1:37;
hence G1 is Dcomplete by Th15, XBOOLE_0:def 10;
end;
registration
let G be Dcomplete _Graph;
cluster -> edgeless for DGraphComplement of G;
coherence by Th17;
end;
registration
let G be non Dcomplete _Graph;
cluster -> non edgeless for DGraphComplement of G;
coherence by Th17;
end;
registration
let G1 be _Graph, G2 be DLGraphComplement of G1;
cluster -> Dcomplete for GraphUnion of G1, G2;
coherence by GLIB_014:30;
end;
registration
let G1 be _Graph, G2 be DGraphComplement of G1;
cluster -> Dcomplete for GraphUnion of G1, G2;
coherence by GLIB_014:32;
end;
theorem
for G being _Graph holds G is Dcomplete iff
[: the_Vertices_of G, the_Vertices_of G :] \ id the_Vertices_of G
c= VertexDomRel(G)
proof
let G be _Graph;
set V = the_Vertices_of G;
hereby
assume A1: G is Dcomplete;
now
let v,w be Vertex of G;
assume [v,w] in [: V, V :] \ id V;
then not [v,w] in id V by XBOOLE_0:def 5;
then v <> w by RELAT_1:def 10;
then ex e being object st e DJoins v,w,G by A1;
hence [v,w] in VertexDomRel(G) by GLUNIR00:1;
end;
hence [: V, V :] \ id V c= VertexDomRel(G) by RELSET_1:def 1;
end;
assume A2: [: V, V :] \ id V c= VertexDomRel(G);
let v,w be Vertex of G;
assume v <> w;
then not [v,w] in id V by RELAT_1:def 10;
then [v,w] in [: V, V :] \ id V by XBOOLE_0:def 5;
hence thesis by A2, GLUNIR00:1;
end;
:: Proof mostly copied from previous one
theorem
for V being non empty set, E being Relation of V
holds createGraph(V,E) is Dcomplete iff [: V, V :] \ id V c= E
proof
let V be non empty set, E be Relation of V;
set G = createGraph(V,E);
hereby
assume A1: G is Dcomplete;
now
let v,w be Element of V;
assume [v,w] in [: V, V :] \ id V;
then not [v,w] in id V by XBOOLE_0:def 5;
then A2: v <> w by RELAT_1:def 10;
consider e being object such that
A3: e DJoins v,w,G by A1, A2;
e = [v,w] by A3, GLUNIR00:64;
hence [v,w] in E by A3, GLUNIR00:63;
end;
hence [: V, V :] \ id V c= E by RELSET_1:def 1;
end;
assume A4: [: V, V :] \ id V c= E;
let v,w be Vertex of G;
assume v <> w;
then not [v,w] in id V by RELAT_1:def 10;
then [v,w] in [: V, V :] \ id V by XBOOLE_0:def 5;
hence thesis by A4, GLUNIR00:63;
end;
begin :: Regular Graphs
reserve c,c1,c2 for Cardinal, G,G1,G2 for _Graph, v for Vertex of G;
definition
let c, G;
attr G is c-regular means
:Def4:
for v holds v.degree() = c;
end;
registration
let c;
cluster c-regular -> with_max_degree for _Graph;
coherence
proof
let G;
assume A1: G is c-regular;
set v = the Vertex of G;
now
let w be Vertex of G;
w.degree() = c by A1
.= v.degree() by A1;
hence w.degree() c= v.degree();
end;
hence thesis by GLIB_013:def 12;
end;
cluster (c+`1)-vertex simple complete -> c-regular for _Graph;
coherence
proof
let G;
assume A2: G is (c+`1)-vertex simple complete;
let v;
A3: v.degree()+`1 = G.order() by A2, GLIBPRE1:45
.= c+`1 by A2, GLIB_013:def 3;
per cases;
suppose A4: c is finite;
then reconsider n = c as Nat;
c+`1 is finite by A4;
then v.degree() is finite by A3;
then reconsider d = v.degree() as Nat;
n+`1 = n+1 & d+`1 = d+1;
then n+1 = d+1 by A3;
hence v.degree() = c;
end;
suppose A5: c is infinite;
then 1 in c by CARD_3:86;
then c+`1 = c by A5, CARD_2:76;
then A6: v.degree()+`1 = c by A3;
then A7: v.degree() is infinite by A5;
then 1 in v.degree() by CARD_3:86;
hence v.degree() = c by A6, A7, CARD_2:76;
end;
end;
cluster simple c-regular for _Graph;
existence
proof
take the simple (c+`1)-vertex complete _Graph;
thus thesis;
end;
end;
::$N Degree of regularity is unique.
theorem Th20:
G is c1-regular c2-regular implies c1 = c2
proof
assume A1: G is c1-regular c2-regular;
set v = the Vertex of G;
thus c1 = v.degree() by A1
.= c2 by A1;
end;
theorem Th21:
G is c-regular iff for C being Component of G holds C is c-regular
proof
thus G is c-regular implies for C being Component of G holds C is c-regular
proof
assume A1: G is c-regular;
let C be Component of G;
let w be Vertex of C;
the_Vertices_of C c= the_Vertices_of G;
then reconsider v = w as Vertex of G by TARSKI:def 3;
thus w.degree() = v.degree() by GLIBPRE0:44
.= c by A1;
end;
assume A2: for C being Component of G holds C is c-regular;
let v be Vertex of G;
set C = the inducedSubgraph of G, G.reachableFrom(v);
A3: the_Vertices_of C = G.reachableFrom(v) by GLIB_000:def 37;
A4: C is c-regular by A2;
v in G.reachableFrom(v) by GLIB_002:9;
then reconsider w = v as Vertex of C by A3;
thus v.degree() = w.degree() by GLIBPRE0:44
.= c by A4;
end;
registration
let c;
cluster non c-regular for _Graph;
existence
proof
per cases;
suppose c is finite;
then reconsider n = c as Nat;
take G = the (n+1)-regular _Graph;
assume G is c-regular;
then n = n+1 by Th20;
hence contradiction;
end;
suppose A1: c is infinite;
take G = the 0-regular _Graph;
assume G is c-regular;
hence contradiction by A1, Th20;
end;
end;
let G be c-regular _Graph;
cluster -> c-regular for Component of G;
coherence by Th21;
end;
theorem Th22:
for G being c-regular _Graph holds G.minDegree() = c & G.maxDegree() = c
proof
let G be c-regular _Graph;
now
set v = the Vertex of G;
take v;
thus A1: v.degree() = c by Def4;
let w be Vertex of G;
thus v.degree() c= w.degree() by A1, Def4;
end;
hence G.minDegree() = c by GLIB_013:36;
now
set v = the Vertex of G;
take v;
thus A2: v.degree() = c by Def4;
let w be Vertex of G;
thus w.degree() c= v.degree() by A2, Def4;
end;
hence G.maxDegree() = c by GLIB_013:48;
end;
theorem Th23:
G.minDegree() = c & G.supDegree() = c implies G is c-regular
proof
assume A1: G.minDegree() = c & G.supDegree() = c;
let v;
G.minDegree() c= v.degree() & v.degree() c= G.supDegree() by GLIB_013:35;
hence v.degree() = c by A1, XBOOLE_0:def 10;
end;
registration
let n be Nat;
cluster n-regular -> locally-finite for _Graph;
coherence
proof
let G;
assume G is n-regular;
then for v holds v.degree() is finite;
hence thesis by GLIB_013:23;
end;
cluster simple vertex-finite n-regular for _Graph;
existence
proof
take G = the simple (n+1)-vertex complete _Graph;
G is (n+`1)-vertex vertex-finite;
hence thesis;
end;
end;
theorem Th24:
G is edgeless iff G is 0-regular
proof
thus G is edgeless implies G is 0-regular;
assume A1: G is 0-regular;
assume G is non edgeless;
then consider e being object such that
A2: e in the_Edges_of G by XBOOLE_0:def 1;
A3: e Joins (the_Source_of G).e,(the_Target_of G).e,G by A2, GLIB_000:def 13;
then reconsider v = (the_Source_of G).e as Vertex of G by GLIB_000:13;
v.degree() <> 0 by A3, GLIB_000:143, GLIB_000:157;
hence contradiction by A1;
end;
registration
cluster edgeless -> 0-regular for _Graph;
coherence;
cluster 0-regular -> edgeless for _Graph;
coherence by Th24;
end;
registration
let c be non empty Cardinal;
cluster c-regular -> non edgeless for _Graph;
coherence
proof
let G;
assume A1: G is c-regular;
set v = the Vertex of G;
v.degree() = c by A1;
hence thesis;
end;
end;
:: this is just a special case of
:: cluster without_isolated_vertices edge-finite -> vertex-finite
:: and
:: cluster c-regular -> without_isolated_vertices
:: registration
:: let c be non empty Cardinal;
:: cluster c-regular edge-finite -> vertex-finite for _Graph;
:: coherence;
:: end;
theorem
for G being simple c-regular _Graph holds c c= G.order()
proof
let G be simple c-regular _Graph;
set v = the Vertex of G;
card v.allNeighbors() c= G.order() by CARD_1:11;
then v.degree() c= G.order() by GLIB_000:111;
hence thesis by Def4;
end;
theorem Th26:
for n being Nat, G1 being simple vertex-finite n-regular _Graph
for G2 being GraphComplement of G1
holds G2 is (G1.order()-'(n+1))-regular
proof
let n be Nat, G1 be simple vertex-finite n-regular _Graph;
let G2 be GraphComplement of G1;
let v2 be Vertex of G2;
reconsider v1 = v2 as Vertex of G1 by GLIB_012:98;
v1.degree() < G1.order() by GLIBPRE1:114;
then n < G1.order() by Def4;
then A1: n+1 <= G1.order() by NAT_1:13;
thus v2.degree() = G1.order()-(v1.degree()+1) by GLIBPRE1:112
.= G1.order()+0-(n+1) by Def4
.= G1.order()-'(n+1) by A1, NAT_D:37;
end;
theorem Th27:
(ex v st v is isolated) & G is c-regular implies c = 0
proof
assume A1: (ex v st v is isolated) & G is c-regular;
then consider v such that
A2: v is isolated;
thus c = v.degree() by A1
.= 0 by A2, GLIB_000:157;
end;
theorem Th28:
(ex v st v is endvertex) & G is c-regular implies c = 1
proof
assume A1: (ex v st v is endvertex) & G is c-regular;
then consider v such that
A2: v is endvertex;
thus c = v.degree() by A1
.= 1 by A2, GLIB_000:174;
end;
registration
let G be 1-regular _Graph;
cluster -> endvertex for Vertex of G;
coherence
proof
let v be Vertex of G;
v.degree() = 1 by Def4;
hence thesis by GLIB_000:174;
end;
end;
theorem Th29:
for G being 1-regular _Graph, T being Trail of G st T is non trivial
ex e being object st e Joins T.first(),T.last(),G &
T = G.walkOf(T.first(),e,T.last())
proof
let G be 1-regular _Graph, T be Trail of G;
assume T is non trivial;
then A1: 3 <= len T by GLIB_001:125;
now
assume len T <> 3;
then A2: 3 < len T by A1, XXREAL_0:1;
then A3: T.(3+1) Joins T.3,T.(3+2),G by GLIB_001:def 3, POLYFORM:6;
then reconsider v = T.3 as Vertex of G by GLIB_000:13;
consider e being object such that
A4: v.edgesInOut() = {e} & not e Joins v,v,G by GLIB_000:def 51;
T.4 in v.edgesInOut() by A3, GLIB_000:62;
then A5: T.4 = e by A4, TARSKI:def 1;
1 < len T by A1, XXREAL_0:2;
then T.(1+1) Joins T.1,T.(1+2),G by GLIB_001:def 3, POLYFORM:4;
then T.2 in v.edgesInOut() by GLIB_000:14, GLIB_000:62;
then A6: T.2 = T.4 by A4, A5, TARSKI:def 1;
3+1 < len T + 1 by A2, XREAL_1:8;
then 1 <= 2 & 2 < 4 & 4 <= len T by NAT_1:13;
hence contradiction by A6, GLIB_001:138, POLYFORM:5, POLYFORM:7;
end;
hence thesis by GLIBPRE1:28;
end;
::$INSERT The connected $1$-regular graph is $K_2$
registration
cluster 1-regular connected -> 2-vertex 1-edge complete for _Graph;
coherence
proof
let G;
assume A1: G is 1-regular connected;
set v = the Vertex of G;
consider e being object such that
A2: v.edgesInOut() = {e} & not e Joins v,v,G by A1, GLIB_000:def 51;
A3: e in v.edgesInOut() by A2, TARSKI:def 1;
then A4: e in the_Edges_of G;
ex w being Vertex of G st w <> v & e Joins v,w,G
proof
set x = (the_Source_of G).e, y = (the_Target_of G).e;
A5: e Joins x,y,G & e Joins y,x,G by A4, GLIB_000:def 13;
then reconsider x,y as Vertex of G by GLIB_000:13;
per cases by A3, GLIB_000:61;
suppose A6: v = x;
take y;
thus thesis by A2, A5, A6;
end;
suppose A7: v = y;
take x;
thus thesis by A2, A5, A7;
end;
end;
then consider w being Vertex of G such that
A8: w <> v & e Joins v,w,G;
now
let x be object;
hereby
assume x in the_Vertices_of G;
then reconsider u = x as Vertex of G;
assume A9: x <> v & x <> w;
consider W being Walk of G such that
A10: W is_Walk_from v, u by A1, GLIB_002:def 1;
set P = the Path of W;
P is_Walk_from v, u by A10, GLIB_001:160;
then A11: P.first() = v & P.last() = u by GLIB_001:def 23;
then A12: P is non trivial by A9, GLIB_001:127;
then consider e1 being object such that
e1 Joins P.first(),P.last(),G and
A13: P = G.walkOf(P.first(),e1,P.last()) by A1, Th29;
A14: P = G.walkOf(v,e1,u) by A11, A13;
G.walkOf(the Vertex of G) is trivial;
then A15: e1 Joins v,u,G by A12, A14, GLIB_001:def 5;
then e1 in v.edgesInOut() by GLIB_000:62;
then e1 = e by A2, TARSKI:def 1;
hence contradiction by A8, A9, A15, GLIB_000:15;
end;
assume x = v or x = w;
hence x in the_Vertices_of G;
end;
then A16: the_Vertices_of G = {v,w} by TARSKI:def 2;
then G.order() = 2 by A8, CARD_2:57;
hence G is 2-vertex by GLIB_013:def 3;
now
let x be object;
hereby
set y = (the_Source_of G).x, z = (the_Target_of G).x;
assume x in the_Edges_of G;
then A17: x Joins y,z,G by GLIB_000:def 13;
then y in {v,w} & z in {v,w} by A16, GLIB_000:13;
then per cases by TARSKI:def 2;
suppose y = v or z = v;
then x in v.edgesInOut() by A17, GLIB_000:14, GLIB_000:62;
hence x = e by A2, TARSKI:def 1;
end;
suppose y = w & z = w;
hence x = e by A1, A17, GLIB_000:146; :: by contradiction
end;
end;
assume x = e;
hence x in the_Edges_of G by A4;
end;
then the_Edges_of G = {e} by TARSKI:def 1;
then G.size() = 1 by CARD_1:30;
hence G is 1-edge by GLIB_013:def 4;
now
let x,y be Vertex of G;
assume A18: x <> y;
(x = v or x = w) & (y = v or y = w) by A16, TARSKI:def 2;
then (x = v & y = w) or (x = w & y = v) by A18;
hence x,y are_adjacent by A8, CHORD:def 3;
end;
hence thesis by CHORD:def 6;
end;
cluster simple 2-vertex connected -> 1-regular for _Graph;
coherence
proof
let G;
assume A19: G is simple 2-vertex connected;
then G.order() = 2 by GLIB_013:def 3;
then consider v,w being object such that
A20: v <> w & the_Vertices_of G = {v,w} by CARD_2:60;
reconsider v,w as Vertex of G by A20, TARSKI:def 2;
consider W being Walk of G such that
A21: W is_Walk_from v,w by A19, GLIB_002:def 1;
set P = the Path of W;
P is_Walk_from v,w by A21, GLIB_001:160;
then A22: P.first() = v & P.last() = w by GLIB_001:def 23;
then 3 <= len P & 1 < 3 by A20, GLIB_001:125, 127;
then 1 < len P by XXREAL_0:2;
then A23: P.(1+1) Joins P.1,P.(1+2),G by GLIB_001:def 3, POLYFORM:4;
then A24: P.3 in the_Vertices_of G by GLIB_000:13;
set e = P.2;
A25: P.1 = v by A22, GLIB_001:def 6;
then P.3 <> v by A19, A23, GLIB_000:18;
then A26: e Joins v,w,G by A20, A23, A24, A25, TARSKI:def 2;
now
let f be object;
hereby
assume f in v.edgesInOut();
then consider u being Vertex of G such that
A27: f Joins v,u,G by GLIB_000:64;
u <> v by A19, A27, GLIB_000:18;
then u = w by A20, TARSKI:def 2;
hence f = e by A19, A26, A27, GLIB_000:def 20;
end;
assume f = e;
hence f in v.edgesInOut() by A26, GLIB_000:62;
end;
then v.edgesInOut() = {e} by TARSKI:def 1;
then v is endvertex by A19, GLIB_000:18, GLIB_000:def 51;
then A28: v.degree() = 1 by GLIB_000:174;
now
let f be object;
hereby
assume f in w.edgesInOut();
then consider u being Vertex of G such that
A29: f Joins w,u,G by GLIB_000:64;
A30: f Joins u,w,G by A29, GLIB_000:14;
u <> w by A19, A29, GLIB_000:18;
then u = v by A20, TARSKI:def 2;
hence f = e by A19, A26, A30, GLIB_000:def 20;
end;
assume f = e;
hence f in w.edgesInOut() by A26, GLIB_000:14, GLIB_000:62;
end;
then w.edgesInOut() = {e} by TARSKI:def 1;
then w is endvertex by A19, GLIB_000:18, GLIB_000:def 51;
then A31: w.degree() = 1 by GLIB_000:174;
let u be Vertex of G;
per cases by A20, TARSKI:def 2;
suppose u = v;
hence u.degree() = 1 by A28;
end;
suppose u = w;
hence u.degree() = 1 by A31;
end;
end;
end;
Lm2:
for F being PGraphMapping of G1, G2 st F is isomorphism
holds G1 is c-regular implies G2 is c-regular
proof
let F be PGraphMapping of G1, G2;
assume A1: F is isomorphism & G1 is c-regular;
let v2 be Vertex of G2;
rng F_V = the_Vertices_of G2 by A1, GLIB_010:def 12;
then consider v1 being object such that
A2: v1 in dom F_V & F_V.v1 = v2 by FUNCT_1:def 3;
reconsider v1 as Vertex of G1 by A2;
F_V/.v1 = F_V.v1 by A2, PARTFUN1:def 6;
hence v2.degree() = v1.degree() by A1, A2, GLIBPRE0:93
.= c by A1;
end;
theorem Th30:
for F being PGraphMapping of G1, G2 st F is isomorphism
holds G1 is c-regular iff G2 is c-regular
proof
let F be PGraphMapping of G1, G2;
assume A1: F is isomorphism;
hence G1 is c-regular implies G2 is c-regular by Lm2;
reconsider F0 = F as one-to-one PGraphMapping of G1, G2 by A1;
F0" is isomorphism by A1, GLIB_010:75;
hence thesis by Lm2;
end;
theorem Th31:
G1 == G2 & G1 is c-regular implies G2 is c-regular
proof
assume G1 == G2;
then consider F being PGraphMapping of G1, G2 such that
A1: F = id G1 & F is Disomorphism by GLIBPRE0:75;
thus thesis by A1, Lm2;
end;
theorem Th32:
for E being set, G2 being reverseEdgeDirections of G1, E
holds G1 is c-regular iff G2 is c-regular
proof
let E be set, G2 be reverseEdgeDirections of G1, E;
consider F being PGraphMapping of G1, G2 such that
A1: F = id G1 & F is isomorphism by GLIBPRE0:77;
thus thesis by A1, Th30;
end;
:: The 1-regular graphs are sometimes called ladder graph or ladder rung graph
:: but since it is rarely used in the literature, it is omitted here.
:: If you think a definition is needed nonetheless, please use the
:: term "ladder-rung" rather than "ladder" cause the latter is more often used
:: to refer to P_n x P_2 instead of nP_2.
:: On the other hand cubic graphs are often used AND shorten the number of
:: characters needed for the attribute descriptor, hence they are defined here.
definition
let G be _Graph;
attr G is cubic means :: or trivalent
G is 3-regular;
end;
registration
cluster cubic -> 3-regular for _Graph;
coherence;
cluster 3-regular -> cubic for _Graph;
coherence;
end;
theorem
G is cubic iff for v holds v.degree() = 3 by Def4;
theorem
for F being PGraphMapping of G1, G2 st F is isomorphism
holds G1 is cubic iff G2 is cubic by Th30;
theorem
G1 == G2 & G1 is cubic implies G2 is cubic by Th31;
theorem
for E being set, G2 being reverseEdgeDirections of G1, E
holds G1 is cubic iff G2 is cubic by Th32;
definition
let G be _Graph;
attr G is regular means
:Def6:
ex c being Cardinal st G is c-regular;
end;
theorem
G is regular iff G.minDegree() = G.supDegree()
proof
hereby
assume G is regular;
then consider c being Cardinal such that
A1: G is c-regular;
thus G.minDegree() = c by A1, Th22
.= G.supDegree() by A1, Th22;
end;
assume G.minDegree() = G.supDegree();
then G is G.minDegree()-regular by Th23;
hence thesis;
end;
definition
let G be locally-finite _Graph;
redefine attr G is regular means :: redefines regular (GLIB_016, definition)
:Def7:
ex n being Nat st G is n-regular;
compatibility
proof
hereby
assume G is regular;
then consider c being Cardinal such that
A1: G is c-regular;
set v = the Vertex of G;
v.degree() = c & v.degree() is finite by A1;
then reconsider n = c as Nat;
take n;
thus G is n-regular by A1;
end;
thus (ex n being Nat st G is n-regular) implies G is regular;
end;
end;
registration
let c be Cardinal;
cluster c-regular -> regular for _Graph;
coherence;
end;
registration
cluster cubic -> regular for _Graph;
coherence;
cluster regular -> with_max_degree for _Graph;
coherence;
cluster simple non edgeless finite regular for _Graph;
existence
proof
take the simple finite 1-regular _Graph;
thus thesis;
end;
end;
registration
let G be regular _Graph;
cluster -> regular for Component of G;
coherence
proof
let C be Component of G;
consider c being Cardinal such that
A1: G is c-regular by Def6;
thus thesis by A1;
end;
end;
registration
let G be simple _finite regular _Graph;
cluster -> regular for GraphComplement of G;
coherence
proof
let H be GraphComplement of G;
consider n being Nat such that
A1: G is n-regular by Def7;
H is (G.order()-'(n+1))-regular by A1, Th26;
hence thesis;
end;
end;
theorem
(ex v st v is isolated) & G is regular implies G is edgeless
proof
assume A1: (ex v st v is isolated) & G is regular;
then consider c being Cardinal such that
A2: G is c-regular;
c = 0 by A1, A2, Th27;
hence thesis by A2;
end;
theorem
(ex v st v is endvertex) & G is regular implies G is 1-regular
proof
assume A1: (ex v st v is endvertex) & G is regular;
then consider c being Cardinal such that
A2: G is c-regular;
c = 1 by A1, A2, Th28;
hence thesis by A2;
end;
theorem Th40:
for F being PGraphMapping of G1, G2 st F is isomorphism
holds G1 is regular iff G2 is regular
proof
let F be PGraphMapping of G1, G2;
assume A1: F is isomorphism;
hereby
assume G1 is regular;
then consider c being Cardinal such that
A2: G1 is c-regular;
G2 is c-regular by A1, A2, Th30;
hence G2 is regular;
end;
assume G2 is regular;
then consider c being Cardinal such that
A3: G2 is c-regular;
G1 is c-regular by A1, A3, Th30;
hence G1 is regular;
end;
theorem
G1 == G2 & G1 is regular implies G2 is regular
proof
assume G1 == G2;
then consider F being PGraphMapping of G1, G2 such that
A1: F = id G1 & F is Disomorphism by GLIBPRE0:75;
thus thesis by A1, Th40;
end;
theorem
for E being set, G2 being reverseEdgeDirections of G1, E
holds G1 is regular iff G2 is regular
proof
let E be set, G2 be reverseEdgeDirections of G1, E;
consider F being PGraphMapping of G1, G2 such that
A1: F = id G1 & F is isomorphism by GLIBPRE0:77;
thus thesis by A1, Th40;
end;
begin :: Directed-regular Graphs
definition
let c, G;
attr G is c-Dregular means
:Def8:
for v holds v.inDegree() = c & v.outDegree() = c;
end;
registration
let c;
cluster c-Dregular -> with_max_in_degree with_max_out_degree for _Graph;
coherence
proof
let G;
assume A1: G is c-Dregular;
set v = the Vertex of G;
now
let w be Vertex of G;
w.inDegree() = c by A1
.= v.inDegree() by A1;
hence w.inDegree() c= v.inDegree();
end;
hence G is with_max_in_degree by GLIB_013:def 13;
now
let w be Vertex of G;
w.outDegree() = c by A1
.= v.outDegree() by A1;
hence w.outDegree() c= v.outDegree();
end;
hence G is with_max_out_degree by GLIB_013:def 14;
end;
cluster (c+`1)-vertex Dsimple Dcomplete -> c-Dregular for _Graph;
coherence
proof
let G be _Graph;
assume A2: G is (c+`1)-vertex Dsimple Dcomplete;
let v be Vertex of G;
A3: v.inDegree()+`1 = G.order() by A2, Th13
.= c+`1 by A2, GLIB_013:def 3;
A4: v.outDegree()+`1 = G.order() by A2, Th13
.= c+`1 by A2, GLIB_013:def 3;
per cases;
suppose A5: c is finite;
then reconsider n = c as Nat;
c+`1 is finite by A5;
then v.inDegree() is finite & v.outDegree() is finite by A3, A4;
then reconsider d1 = v.inDegree(), d2 = v.outDegree() as Nat;
n+`1 = n+1 & d1+`1 = d1+1 & d2+`1 = d2+1;
then n+1 = d1+1 & n+1 = d2+1 by A3, A4;
hence v.inDegree() = c & v.outDegree() = c;
end;
suppose A6: c is infinite;
then 1 in c by CARD_3:86;
then c+`1 = c by A6, CARD_2:76;
then A7: v.inDegree()+`1 = c & v.outDegree()+`1 = c by A3, A4;
then A8: v.inDegree() is infinite & v.outDegree() is infinite by A6;
then A9: 1 in v.inDegree() & 1 in v.outDegree() by CARD_3:86;
hence v.inDegree() = c by A7, A8, CARD_2:76;
thus v.outDegree() = c by A7, A8, A9, CARD_2:76;
end;
end;
cluster Dsimple c-Dregular for _Graph;
existence
proof
take G = canDCompleteGraph(c+`1);
thus thesis;
end;
end;
::$N Degree of directed regularity is unique.
theorem Th43:
G is c1-Dregular c2-Dregular implies c1 = c2
proof
assume A1: G is c1-Dregular c2-Dregular;
set v = the Vertex of G;
thus c1 = v.inDegree() by A1
.= c2 by A1;
end;
registration
let c;
cluster non c-Dregular for _Graph;
existence
proof
per cases;
suppose c is finite;
then reconsider n = c as Nat;
take G = the (n+1)-Dregular _Graph;
assume G is c-Dregular;
then n = n+1 by Th43;
hence contradiction;
end;
suppose A1: c is infinite;
take G = the 0-Dregular _Graph;
assume G is c-Dregular;
hence contradiction by A1, Th43;
end;
end;
let G be c-Dregular _Graph;
cluster -> c-Dregular for Component of G;
coherence
proof
let C be Component of G;
let w be Vertex of C;
the_Vertices_of C c= the_Vertices_of G;
then reconsider v = w as Vertex of G by TARSKI:def 3;
thus w.inDegree() = v.inDegree() by GLIBPRE0:44
.= c by Def8;
thus w.outDegree() = v.outDegree() by GLIBPRE0:44
.= c by Def8;
end;
end;
theorem Th44:
for G being c-Dregular _Graph holds
G.minInDegree() = c & G.minOutDegree() = c &
G.maxInDegree() = c & G.maxOutDegree() = c
proof
let G be c-Dregular _Graph;
now
set v = the Vertex of G;
take v;
thus A1: v.inDegree() = c by Def8;
let w be Vertex of G;
thus v.inDegree() c= w.inDegree() by A1, Def8;
end;
hence G.minInDegree() = c by GLIB_013:37;
now
set v = the Vertex of G;
take v;
thus A2: v.outDegree() = c by Def8;
let w be Vertex of G;
thus v.outDegree() c= w.outDegree() by A2, Def8;
end;
hence G.minOutDegree() = c by GLIB_013:38;
now
set v = the Vertex of G;
take v;
thus A3: v.inDegree() = c by Def8;
let w be Vertex of G;
thus w.inDegree() c= v.inDegree() by A3, Def8;
end;
hence G.maxInDegree() = c by GLIB_013:49;
now
set v = the Vertex of G;
take v;
thus A4: v.outDegree() = c by Def8;
let w be Vertex of G;
thus w.outDegree() c= v.outDegree() by A4, Def8;
end;
hence G.maxOutDegree() = c by GLIB_013:50;
end;
theorem Th45:
G.minInDegree() = c & G.minOutDegree() = c &
G.supInDegree() = c & G.supOutDegree() = c implies G is c-Dregular
proof
assume A1: G.minInDegree() = c & G.minOutDegree() = c &
G.supInDegree() = c & G.supOutDegree() = c;
let v;
G.minInDegree() c= v.inDegree() & v.inDegree() c= G.supInDegree()
by GLIB_013:35;
hence v.inDegree() = c by A1, XBOOLE_0:def 10;
G.minOutDegree() c= v.outDegree() & v.outDegree() c= G.supOutDegree()
by GLIB_013:35;
hence v.outDegree() = c by A1, XBOOLE_0:def 10;
end;
theorem Th46:
for n being Nat holds G is n-Dregular implies G is 2*n-regular
proof
let n be Nat;
assume A1: G is n-Dregular;
let v;
thus v.degree() = v.inDegree() +` n by A1
.= n+`n by A1
.= 2*n;
end;
registration
let n be Nat;
cluster n-Dregular -> 2*n-regular locally-finite for _Graph;
coherence
proof
let G;
assume G is n-Dregular;
hence G is 2*n-regular by Th46;
hence thesis;
end;
cluster Dsimple _finite n-Dregular for _Graph;
existence
proof
take G = canDCompleteGraph(n+1);
n+1 = n+`1;
hence thesis;
end;
end;
registration
let c be infinite Cardinal;
cluster c-Dregular -> c-regular for _Graph;
coherence
proof
let G;
assume A1: G is c-Dregular;
now
let v;
thus v.degree() = v.inDegree() +` c by A1
.= c+`c by A1
.= c by CARD_2:75;
end;
hence G is c-regular;
end;
end;
theorem Th47:
G is edgeless iff G is 0-Dregular
proof
thus G is edgeless implies G is 0-Dregular;
assume G is 0-Dregular;
then G is 2*0-regular by Th46;
hence thesis;
end;
registration
cluster edgeless -> 0-Dregular for _Graph;
coherence;
cluster 0-Dregular -> edgeless for _Graph;
coherence by Th47;
end;
registration
let c be non empty Cardinal;
cluster c-Dregular -> non edgeless for _Graph;
coherence
proof
let G;
assume A1: G is c-Dregular;
set v = the Vertex of G;
v.inDegree() = c by A1;
hence thesis;
end;
end;
:: same as above
:: registration
:: let c be non empty Cardinal;
:: cluster c-Dregular edge-finite -> vertex-finite for _Graph;
:: coherence;
:: end;
theorem
for G being Dsimple c-Dregular _Graph holds c c= G.order()
proof
let G be Dsimple c-Dregular _Graph;
set v = the Vertex of G;
card v.inNeighbors() c= G.order() by CARD_1:11;
then v.inDegree() c= G.order() by GLIB_000:109;
hence thesis by Def8;
end;
theorem Th49:
for n being Nat, G1 being Dsimple vertex-finite n-Dregular _Graph
for G2 being DGraphComplement of G1
holds G2 is (G1.order()-'(n+1))-Dregular
proof
let n be Nat, G1 be Dsimple vertex-finite n-Dregular _Graph;
let G2 be DGraphComplement of G1;
let v2 be Vertex of G2;
reconsider v1 = v2 as Vertex of G1 by GLIB_012:80;
v1.inDegree() < G1.order() by GLIBPRE1:113;
then n < G1.order() by Def8;
then A1: n+1 <= G1.order() by NAT_1:13;
thus v2.inDegree() = G1.order()-(v1.inDegree()+1) by GLIBPRE1:111
.= G1.order()+0-(n+1) by Def8
.= G1.order()-'(n+1) by A1, NAT_D:37;
thus v2.outDegree() = G1.order()-(v1.outDegree()+1) by GLIBPRE1:111
.= G1.order()+0-(n+1) by Def8
.= G1.order()-'(n+1) by A1, NAT_D:37;
end;
theorem
(ex v st v is isolated) & G is c-Dregular implies c = 0
proof
assume A1: (ex v st v is isolated) & G is c-Dregular;
then consider v such that
A2: v is isolated;
thus c = v.inDegree() by A1
.= 0 by A2, GLIB_000:156;
end;
registration
let c; let G be c-Dregular _Graph;
cluster -> non endvertex for Vertex of G;
coherence
proof
let v be Vertex of G;
assume v is endvertex;
then A1: v.degree() = 1 by GLIB_000:174;
per cases;
suppose A2: c is infinite;
then G is c-regular;
hence contradiction by A1, A2;
end;
suppose c is finite;
then reconsider n = c as Nat;
G is 2*n-regular by Th46;
hence contradiction by A1, POLYFORM:4, ABIAN:def 2;
end;
end;
end;
:: A connected 1-Dregular graph is either K2 with an additional edge in
:: the other direction, the trivial graph with 1 loop or a collection
:: of directed cycles or directed double rays (the latter two not shown here).
registration
cluster 2-edge 2-vertex Dsimple -> 1-Dregular complete for _Graph;
coherence
proof
let G;
assume A1: G is 2-edge 2-vertex Dsimple;
then G.order() = 2 by GLIB_013:def 3;
then consider v,w being object such that
A2: v <> w & {v,w} = the_Vertices_of G by CARD_2:60;
reconsider v,w as Vertex of G by A2, TARSKI:def 2;
:: to shorten the Proof the case distinction is done in a sub Proof
ex e,f being object
st e <> f & {e,f} = the_Edges_of G & e DJoins v,w,G & f DJoins w,v,G
proof
G.size() = 2 by A1, GLIB_013:def 4;
then consider e1,e2 being object such that
A3: e1 <> e2 & {e1,e2} = the_Edges_of G by CARD_2:60;
A4: e1 in the_Edges_of G & e2 in the_Edges_of G by A3, TARSKI:def 2;
set x1 = (the_Source_of G).e1, y1 = (the_Target_of G).e1;
set x2 = (the_Source_of G).e2, y2 = (the_Target_of G).e2;
A5: e1 DJoins x1,y1,G & e2 DJoins x2,y2,G by A4, GLIB_000:def 14;
then A6: e1 Joins x1,y1,G & e2 Joins x2,y2,G by GLIB_000:16;
then reconsider x1,y1,x2,y2 as Vertex of G by GLIB_000:13;
A7: x1 <> y1 & x2 <> y2 by A1, A6, GLIB_000:18;
A8: x1 <> x2 or y1 <> y2 by A1, A3, A5, GLIB_000:def 21;
A9: (x1=v or x1=w)&(y1=v or y1=w)&(x2=v or x2=w)&(y2=v or y2=w)
by A2, TARSKI:def 2;
then per cases by A7;
suppose A10: x1=v & y1=w;
take e1,e2;
thus e1 <> e2 & {e1,e2} = the_Edges_of G by A3;
x2=w & y2=v by A7, A8, A9, A10;
hence e1 DJoins v,w,G & e2 DJoins w,v,G by A5, A10;
end;
suppose A11: x1=w & y1=v;
take e2,e1;
thus e2 <> e1 & {e2,e1} = the_Edges_of G by A3;
x2=v & y2=w by A7, A8, A9, A11;
hence e2 DJoins v,w,G & e1 DJoins w,v,G by A5, A11;
end;
end;
then consider e,f being object such that
A12: e <> f & {e,f} = the_Edges_of G & e DJoins v,w,G & f DJoins w,v,G;
:: next is to calculate edgesIn/Out for v and w, all four cases very similar
now
let x be object;
hereby
assume x in v.edgesIn();
then consider z being set such that
A13: x DJoins z,v,G by GLIB_000:57;
x Joins z,v,G by A13, GLIB_000:16;
then z in {v,w} by A2, GLIB_000:13;
then z = v or z = w by TARSKI:def 2;
then z = w by A1, A13, GLIB_000:136;
hence x = f by A1, A12, A13, GLIB_000:def 21;
end;
assume x = f;
then x = f & f is set by TARSKI:1;
hence x in v.edgesIn() by A12, GLIB_000:57;
end;
then v.edgesIn() = {f} by TARSKI:def 1;
then A14: v.inDegree() = 1 by CARD_1:30;
now
let x be object;
hereby
assume x in v.edgesOut();
then consider z being set such that
A15: x DJoins v,z,G by GLIB_000:59;
x Joins v,z,G by A15, GLIB_000:16;
then z in {v,w} by A2, GLIB_000:13;
then z = v or z = w by TARSKI:def 2;
then z = w by A1, A15, GLIB_000:136;
hence x = e by A1, A12, A15, GLIB_000:def 21;
end;
assume x = e;
then x = e & e is set by TARSKI:1;
hence x in v.edgesOut() by A12, GLIB_000:59;
end;
then v.edgesOut() = {e} by TARSKI:def 1;
then A16: v.outDegree() = 1 by CARD_1:30;
now
let x be object;
hereby
assume x in w.edgesIn();
then consider z being set such that
A17: x DJoins z,w,G by GLIB_000:57;
x Joins z,w,G by A17, GLIB_000:16;
then z in {v,w} by A2, GLIB_000:13;
then z = v or z = w by TARSKI:def 2;
then z = v by A1, A17, GLIB_000:136;
hence x = e by A1, A12, A17, GLIB_000:def 21;
end;
assume x = e;
then x = e & e is set by TARSKI:1;
hence x in w.edgesIn() by A12, GLIB_000:57;
end;
then w.edgesIn() = {e} by TARSKI:def 1;
then A18: w.inDegree() = 1 by CARD_1:30;
now
let x be object;
hereby
assume x in w.edgesOut();
then consider z being set such that
A19: x DJoins w,z,G by GLIB_000:59;
x Joins w,z,G by A19, GLIB_000:16;
then z in {v,w} by A2, GLIB_000:13;
then z = v or z = w by TARSKI:def 2;
then z = v by A1, A19, GLIB_000:136;
hence x = f by A1, A12, A19, GLIB_000:def 21;
end;
assume x = f;
then x = f & f is set by TARSKI:1;
hence x in w.edgesOut() by A12, GLIB_000:59;
end;
then w.edgesOut() = {f} by TARSKI:def 1;
then A20: w.outDegree() = 1 by CARD_1:30;
:: show the desired properties
now
let u be Vertex of G;
per cases by A2, TARSKI:def 2;
suppose u = v;
hence u.inDegree() = 1 & u.outDegree() = 1 by A14, A16;
end;
suppose u = w;
hence u.inDegree() = 1 & u.outDegree() = 1 by A18, A20;
end;
end;
hence G is 1-Dregular;
now
let x,y be Vertex of G;
assume A21: x <> y;
x in {v,w} & y in {v,w} by A2;
then (x=v or x=w) & (y=v or y=w) by TARSKI:def 2;
then e Joins x,y,G by A21, A12, GLIB_000:16;
hence x,y are_adjacent by CHORD:def 3;
end;
hence G is complete by CHORD:def 6;
end;
cluster _trivial 1-edge -> 1-Dregular for _Graph;
coherence
proof
let G be _Graph;
assume A22: G is _trivial 1-edge;
then G.order() = 1 by GLIB_000:26;
then consider v being Vertex of G such that
A23: the_Vertices_of G = {v} by GLIB_000:27;
G.size() = 1 by A22, GLIB_013:def 4;
then G.size() = card {{}} by CARD_1:30;
then consider e being object such that
A24: the_Edges_of G = {e} by CARD_1:29;
A25: v.edgesIn() c= {e} & v.edgesOut() c= {e} by A24;
e in the_Edges_of G by A24, TARSKI:def 1;
then A26: e Joins (the_Source_of G).e,(the_Target_of G).e,G
by GLIB_000:def 13;
then (the_Source_of G).e in {v} & (the_Target_of G).e in {v}
by A23, GLIB_000:13;
then (the_Source_of G).e = v & (the_Target_of G).e = v by TARSKI:def 1;
then e DJoins v,v,G & e is set by A26, GLIB_000:16, TARSKI:1;
then e in v.edgesIn() & e in v.edgesOut() by GLIB_000:57, GLIB_000:59;
then {e} c= v.edgesIn() & {e} c= v.edgesOut() by ZFMISC_1:31;
then {e} = v.edgesIn() & {e} = v.edgesOut() by A25, XBOOLE_0:def 10;
then A27: v.inDegree() = 1 & v.outDegree() = 1 by CARD_1:30;
let u be Vertex of G;
u in {v} by A23;
hence thesis by A27, TARSKI:def 1;
end;
end;
Lm3:
for F being PGraphMapping of G1, G2 st F is Disomorphism
holds G1 is c-Dregular implies G2 is c-Dregular
proof
let F be PGraphMapping of G1, G2;
assume A1: F is Disomorphism & G1 is c-Dregular;
let v2 be Vertex of G2;
rng F_V = the_Vertices_of G2 by A1, GLIB_010:def 12;
then consider v1 being object such that
A2: v1 in dom F_V & F_V.v1 = v2 by FUNCT_1:def 3;
reconsider v1 as Vertex of G1 by A2;
A3: F_V/.v1 = F_V.v1 by A2, PARTFUN1:def 6;
hence v2.inDegree() = v1.inDegree() by A1, A2, GLIBPRE0:92
.= c by A1;
thus v2.outDegree() = v1.outDegree() by A1, A2, A3, GLIBPRE0:92
.= c by A1;
end;
theorem Th51:
for F being PGraphMapping of G1, G2 st F is Disomorphism
holds G1 is c-Dregular iff G2 is c-Dregular
proof
let F be PGraphMapping of G1, G2;
assume A1: F is Disomorphism;
hence G1 is c-Dregular implies G2 is c-Dregular by Lm3;
reconsider F0 = F as one-to-one PGraphMapping of G1, G2 by A1;
F0" is semi-Dcontinuous isomorphism by A1, GLIB_010:75;
hence thesis by Lm3;
end;
theorem
G1 == G2 & G1 is c-Dregular implies G2 is c-Dregular
proof
assume G1 == G2;
then consider F being PGraphMapping of G1, G2 such that
A1: F = id G1 & F is Disomorphism by GLIBPRE0:75;
thus thesis by A1, Lm3;
end;
definition
let G be _Graph;
attr G is Dregular means
:Def9:
ex c being Cardinal st G is c-Dregular;
end;
theorem
G is Dregular iff G.minInDegree() = G.supInDegree() &
G.minOutDegree() = G.supOutDegree() & G.minInDegree() = G.minOutDegree()
proof
hereby
assume G is Dregular;
then consider c being Cardinal such that
A1: G is c-Dregular;
thus G.minInDegree() = c by A1, Th44
.= G.supInDegree() by A1, Th44;
thus G.minOutDegree() = c by A1, Th44
.= G.supOutDegree() by A1, Th44;
thus G.minInDegree() = c by A1, Th44
.= G.minOutDegree() by A1, Th44;
end;
assume G.minInDegree() = G.supInDegree() &
G.minOutDegree() = G.supOutDegree() & G.minInDegree() = G.minOutDegree();
then G is G.minInDegree()-Dregular by Th45;
hence thesis;
end;
definition
let G be locally-finite _Graph;
redefine attr G is Dregular means :: redefines Dregular (GLIB_016, definition)
:Def10:
ex n being Nat st G is n-Dregular;
compatibility
proof
hereby
assume G is Dregular;
then consider c being Cardinal such that
A1: G is c-Dregular;
set v = the Vertex of G;
v.inDegree() = c & v.inDegree() is finite by A1;
then reconsider n = c as Nat;
take n;
thus G is n-Dregular by A1;
end;
thus (ex n being Nat st G is n-Dregular) implies G is Dregular;
end;
end;
registration
let c be Cardinal;
cluster c-Dregular -> Dregular for _Graph;
coherence;
end;
registration
cluster Dregular -> with_max_degree for _Graph;
coherence;
cluster Dsimple non edgeless finite Dregular for _Graph;
existence
proof
take the Dsimple finite 1-Dregular _Graph;
thus thesis;
end;
end;
registration
let G be Dregular _Graph;
cluster -> Dregular for Component of G;
coherence
proof
let C be Component of G;
consider c being Cardinal such that
A1: G is c-Dregular by Def9;
thus thesis by A1;
end;
end;
registration
let G be Dsimple _finite Dregular _Graph;
cluster -> Dregular for DGraphComplement of G;
coherence
proof
let H be DGraphComplement of G;
consider n being Nat such that
A1: G is n-Dregular by Def10;
H is (G.order()-'(n+1))-Dregular by A1, Th49;
hence thesis;
end;
end;
registration
let G be Dregular _Graph;
cluster -> non endvertex for Vertex of G;
coherence
proof
consider c being Cardinal such that
A1: G is c-Dregular by Def9;
thus thesis by A1;
end;
end;
theorem Th54:
for F being PGraphMapping of G1, G2 st F is Disomorphism
holds G1 is Dregular iff G2 is Dregular
proof
let F be PGraphMapping of G1, G2;
assume A1: F is Disomorphism;
hereby
assume G1 is Dregular;
then consider c being Cardinal such that
A2: G1 is c-Dregular;
G2 is c-Dregular by A1, A2, Th51;
hence G2 is Dregular;
end;
assume G2 is Dregular;
then consider c being Cardinal such that
A3: G2 is c-Dregular;
G1 is c-Dregular by A1, A3, Th51;
hence G1 is Dregular;
end;
theorem
G1 == G2 & G1 is Dregular implies G2 is Dregular
proof
assume G1 == G2;
then consider F being PGraphMapping of G1, G2 such that
A1: F = id G1 & F is Disomorphism by GLIBPRE0:75;
thus thesis by A1, Th54;
end;
begin :: Counting the Edges
:: basically infinite version of GROUP_2:156
theorem Th56:
for P being set, c being Cardinal
st P is mutually-disjoint & for A being set st A in P holds card A = c
holds card union P = c*`card P
proof
let P be set, c be Cardinal;
assume A1: P is mutually-disjoint & for A being set st A in P holds card A=c;
per cases;
suppose A2: P <> {} & c <> 0;
:: first recognize P as a partition of its union
now
set A0 = the Element of P, a0 = the Element of A0;
A3: A0 in P by A2;
card A0 <> 0 by A1, A2;
then A0 <> {};
then a0 in union P by A3, TARSKI:def 4;
hence union P <> {};
end;
then reconsider X = union P as non empty set;
now
let x be object;
reconsider x0 = x as set by TARSKI:1;
assume x in P;
then x0 c= union P by SETFAM_1:41;
hence x in bool X;
end;
then reconsider p = P as Subset-Family of X by TARSKI:def 3;
now
let A be Subset of X;
assume A4: A in p;
then card A = c by A1;
hence A <> {} by A2;
let B be Subset of X;
assume A5: B in p;
assume A <> B;
hence A misses B by A1, A4, A5, TAXONOM2:def 5;
end;
then reconsider p as a_partition of X by EQREL_1:def 4;
:: next we construct the bijection and show the properties
deffunc G(set) = the Enumeration of $1;
deffunc C(object) = EqClass(In($1,X),p);
deffunc F(object) = [G(C($1)).$1, C($1)];
consider f being Function such that
A6: dom f = X & for x being object st x in X holds f.x = F(x)
from FUNCT_1:sch 3;
:: onto
now
let y be object;
hereby
assume y in [: c, P :];
then consider d, A being object such that
A7: d in c & A in P & y = [d,A] by ZFMISC_1:def 2;
reconsider A as set by A7;
reconsider x = G(A)".d as object;
take x;
card A <> {} by A1, A7;
then A8: A = dom G(A) by FUNCT_2:def 1
.= rng(G(A)") by FUNCT_1:33;
A9: c = card A by A1, A7
.= rng G(A) by FUNCT_2:def 3;
then c = dom(G(A)") by FUNCT_1:33;
then A10: x in A by A7, A8, FUNCT_1:3;
hence A11: x in dom f by A6, A7;
A c= X by A7, SETFAM_1:41;
then In(x,X) = x & A is Subset of X by A6, A11, SUBSET_1:def 8;
then A12: C(x) = A by A7, A10, EQREL_1:def 6;
thus f.x = [G(A).x, A] by A6, A11, A12
.= y by A7, A9, FUNCT_1:35;
end;
given x being object such that
A13: x in dom f & f.x = y;
In(x,X) = x by A6, A13, SUBSET_1:def 8;
then A14: x in C(x) & C(x) in p by EQREL_1:def 6;
then x in dom G(C(x)) by FUNCT_2:def 1;
then G(C(x)).x in rng G(C(x)) by FUNCT_1:3;
then G(C(x)).x in card C(x);
then A15: G(C(x)).x in c by A1, A14;
y = [G(C(x)).x, C(x)] by A6, A13;
hence y in [: c, P :] by A14, A15, ZFMISC_1:def 2;
end;
then A16: rng f = [: c, P :] by FUNCT_1:def 3;
:: one-to-one
now
let x1,x2 be object;
assume A17: x1 in dom f & x2 in dom f & f.x1 = f.x2;
then A18: f.x1=[G(C(x1)).x1,C(x1)] & f.x2=[G(C(x2)).x2,C(x2)] by A6;
then A19: C(x1) = C(x2) by A17, XTUPLE_0:1;
In(x1,X) = x1 & In(x2,X) = x2 by A6, A17, SUBSET_1:def 8;
then A20: x1 in C(x1) & C(x1) in p & x2 in C(x1) by A19, EQREL_1:def 6;
then A21: dom G(C(x1)) = C(x1) by FUNCT_2:def 1;
G(C(x1)).x1 = G(C(x1)).x2 by A17, A18, A19, XTUPLE_0:1;
hence x1 = x2 by A20, A21, FUNCT_1:def 4;
end;
:: conclusion
hence card union P = card rng f by A6, FUNCT_1:def 4, CARD_1:70
.= card [: c, card P :] by A16, CARD_2:7
.= c*`card P by CARD_2:def 2;
end;
suppose A22: P <> {} & c = 0;
now
let x,y be object;
reconsider X=x, Y=y as set by TARSKI:1;
assume x in P & y in P;
then card X = 0 & card Y = 0 by A1, A22;
then X = {} & Y = {};
hence x = y;
end;
then consider x being object such that
A23: P = {x} by A22, ZFMISC_1:def 10, ZFMISC_1:131;
reconsider X = x as set by TARSKI:1;
X in P by A23, TARSKI:def 1;
then card X = 0 by A1, A22;
then X = {};
then union P = {} by A23, ZFMISC_1:25;
hence thesis by A22, CARD_2:20;
end;
suppose P = {};
hence thesis by CARD_2:20, ZFMISC_1:2;
end;
end;
theorem
for X being non empty set, P being a_partition of X, c being Cardinal
st for x being Element of X holds card EqClass(x,P) = c
holds card X = c*`card P
proof
let X be non empty set, P be a_partition of X, c be Cardinal;
assume A1: for x being Element of X holds card EqClass(x,P) = c;
for A, B being set st A in P & B in P & A <> B holds A misses B
by EQREL_1:def 4;
then A2: P is mutually-disjoint by TAXONOM2:def 5;
now
let A be set;
set a = the Element of A;
assume A3: A in P;
then A4: A is Subset of X;
A <> {} by A3, EQREL_1:def 4;
then A5: a in A;
then reconsider a as Element of X by A4;
A = EqClass(a,P) by A3, A5, EQREL_1:def 6;
hence card A = c by A1;
end;
then card union P = c*`card P by A2, Th56;
hence thesis by EQREL_1:def 4;
end;
registration
let f be Function, X be set;
cluster <: f, id X :> -> one-to-one;
coherence
proof
set h = <: f, id X :>;
now
let x1,x2 be object;
assume A1: x1 in dom h & x2 in dom h & h.x1 = h.x2;
then h.x1 = [f.x1,(id X).x1] & h.x2 = [f.x2,(id X).x2] by FUNCT_3:def 7;
then A2: (id X).x1 = (id X).x2 by A1, XTUPLE_0:1;
x1 in dom f /\ dom id X & x2 in dom f /\ dom id X by A1, FUNCT_3:def 7;
then (id X).x1 = x1 & (id X).x2 = x2 by FUNCT_1:18;
hence x1 = x2 by A2;
end;
hence thesis by FUNCT_1:def 4;
end;
end;
registration
let f be one-to-one Function;
cluster f~ -> one-to-one;
coherence
proof
now
let x1,x2 be object;
assume A1: x1 in dom(f~) & x2 in dom(f~) & f~.x1 = f~.x2;
then A2: x1 in dom f & x2 in dom f by FUNCOP_1:def 1;
then per cases by FUNCOP_1:def 1;
suppose A3: f.x1 = f~.x1 & not ex y1,z1 being object st f.x1 = [y1,z1];
per cases by A2, FUNCOP_1:def 1;
suppose f.x2 = f~.x2;
hence x1 = x2 by A1, A2, A3, FUNCT_1:def 4;
end;
suppose ex y2,z2 being object st f.x2 = [y2,z2];
then consider y2,z2 being object such that
A4: f.x2 = [y2,z2];
f~.x2 = [z2,y2] by A2, A4, FUNCOP_1:def 1;
hence x1 = x2 by A1, A3; :: by contradiction, a pair has been found
end;
end;
suppose ex y1,z1 being object st f.x1 = [y1,z1];
then consider y1,z1 being object such that
A5: f.x1 = [y1,z1];
A6: f~.x1 = [z1,y1] by A2, A5, FUNCOP_1:def 1;
per cases by A2, FUNCOP_1:def 1;
suppose f.x2 = f~.x2 & not ex y2,z2 being object st f.x2 = [y2,z2];
hence x1 = x2 by A1, A6; :: by contradiction, a pair has been found
end;
suppose ex y2,z2 being object st f.x2 = [y2,z2];
then consider y2,z2 being object such that
A7: f.x2 = [y2,z2];
f~.x2 = [z2,y2] by A2, A7, FUNCOP_1:def 1;
then z1 = z2 & y1 = y2 by A1, A6, XTUPLE_0:1;
hence x1 = x2 by A2, A5, A7, FUNCT_1:def 4;
end;
end;
end;
hence thesis by FUNCT_1:def 4;
end;
cluster ~f -> one-to-one;
coherence by FUNCTOR0:8;
end;
registration
let X be set, f be Function;
cluster <: id X, f :> -> one-to-one;
coherence
proof
<: id X, f :> = <: f, id X :>~ by FUNCOP_1:2;
hence thesis;
end;
end;
:: F is the function that sends [e,0] to [S.e,e,0] and [e,1] to [T.e,e,1]
:: so by partitioning rng F via first coordinate we count all edges in
:: each vertex (loops double) and dom F tells us that we counted each edge
:: twice, which is just the canonical, combinatorial Proof. The formalization
:: gets a bit technical, but does exactly that.
deffunc H0(_Graph) = <: the_Source_of $1, id the_Edges_of $1 :>;
deffunc H1(_Graph) = <: the_Target_of $1, id the_Edges_of $1 :>;
deffunc F0(_Graph) = [: H0($1), id {0} :];
deffunc F1(_Graph) = [: H1($1), id {1} :];
deffunc F(_Graph) = F0($1) +* F1($1);
deffunc E0(_Graph, Vertex of $1) = [: {$2}, $2.edgesOut(), {0} :];
deffunc E1(_Graph, Vertex of $1) = [: {$2}, $2.edgesIn(), {1} :];
deffunc P(_Graph) = { E0($1,v) \/ E1($1,v)
where v is Vertex of $1 : v is non isolated };
Lm4:
dom H0(G) = the_Edges_of G & dom H1(G) = the_Edges_of G
proof
thus dom H0(G) = dom the_Source_of G /\dom id the_Edges_of G by FUNCT_3:def 7
.= the_Edges_of G /\ the_Edges_of G by FUNCT_2:def 1
.= the_Edges_of G;
thus dom H1(G) = dom the_Target_of G /\dom id the_Edges_of G by FUNCT_3:def 7
.= the_Edges_of G /\ the_Edges_of G by FUNCT_2:def 1
.= the_Edges_of G;
end;
Lm5:
dom F0(G) = [: the_Edges_of G, {0} :] & dom F1(G) = [: the_Edges_of G, {1} :]
proof
thus dom F0(G) = [: dom H0(G), dom id{0} :] by FUNCT_3:def 8
.= [: the_Edges_of G, {0} :] by Lm4;
thus dom F1(G) = [: dom H1(G), dom id{1} :] by FUNCT_3:def 8
.= [: the_Edges_of G, {1} :] by Lm4;
end;
Lm6:
dom F0(G) misses dom F1(G)
proof
{0} misses {1} by ZFMISC_1:11;
then [: the_Edges_of G, {0} :] misses [: the_Edges_of G, {1} :]
by ZFMISC_1:104;
then dom F0(G) misses [: the_Edges_of G, {1} :] by Lm5;
hence thesis by Lm5;
end;
Lm7:
rng F0(G) misses rng F1(G)
proof
assume rng F0(G) meets rng F1(G);
then consider z being object such that
A1: z in rng F0(G) & z in rng F1(G) by XBOOLE_0:3;
consider z0 being object such that
A2: z0 in dom F0(G) & F0(G).z0 = z by A1, FUNCT_1:def 3;
consider z1 being object such that
A3: z1 in dom F1(G) & F1(G).z1 = z by A1, FUNCT_1:def 3;
z0 in [: the_Edges_of G, {0} :] by A2, Lm5;
then consider x0,y0 being object such that
A4: x0 in the_Edges_of G & y0 in {0} & z0=[x0,y0] by ZFMISC_1:def 2;
z1 in [: the_Edges_of G, {1} :] by A3, Lm5;
then consider x1,y1 being object such that
A5: x1 in the_Edges_of G & y1 in {1} & z1=[x1,y1] by ZFMISC_1:def 2;
A6: x0 in dom H0(G) & y0 in dom id {0} by A4, Lm4;
A7: x1 in dom H1(G) & y1 in dom id {1} by A5, Lm4;
A8: [ H0(G).x0, (id {0}).y0 ] = F0(G).(x0,y0) by A6, FUNCT_3:def 8
.= z by A2, A4, BINOP_1:def 1
.= F1(G).(x1,y1) by A3, A5, BINOP_1:def 1
.= [ H1(G).x1, (id {1}).y1 ] by A7, FUNCT_3:def 8;
A9: y0 = 0 & y1 = 1 by A4, A5, TARSKI:def 1;
then 0 = (id {0}).y0 by A4, FUNCT_1:18
.= (id {1}).y1 by A8, XTUPLE_0:1
.= 1 by A5, A9, FUNCT_1:18;
hence contradiction;
end;
Lm8:
F(G) is one-to-one
proof
rng F0(G) misses rng F1(G) by Lm7;
hence thesis by FUNCT_4:92;
end;
Lm9:
dom F(G) = [: the_Edges_of G, {0,1} :]
proof
thus dom F(G) = dom F0(G) \/ dom F1(G) by FUNCT_4:def 1
.= dom F0(G) \/ [: the_Edges_of G, {1} :] by Lm5
.= [: the_Edges_of G, {0} :] \/ [: the_Edges_of G, {1} :] by Lm5
.= [: the_Edges_of G, {0} \/ {1} :] by ZFMISC_1:97
.= [: the_Edges_of G, {0,1} :] by ENUMSET1:1;
end;
Lm10:
for v0, v1 being Vertex of G holds E0(G,v0) misses E1(G,v1)
proof
let v0, v1 be Vertex of G;
assume E0(G,v0) meets E1(G,v1);
then consider z being object such that
A1: z in E0(G,v0) & z in E1(G,v1) by XBOOLE_0:3;
E0(G,v0) = [: [: {v0}, v0.edgesOut() :], {0} :] by ZFMISC_1:def 3;
then consider z0,y0 being object such that
A2: z0 in [: {v0}, v0.edgesOut() :] & y0 in {0} & z = [z0,y0]
by A1, ZFMISC_1:def 2;
E1(G,v1) = [: [: {v1}, v1.edgesIn() :], {1} :] by ZFMISC_1:def 3;
then consider z1,y1 being object such that
A3: z1 in [: {v1}, v1.edgesIn() :] & y1 in {1} & z = [z1,y1]
by A1, ZFMISC_1:def 2;
y0 = 0 & y1 = 1 by A2, A3, TARSKI:def 1;
hence contradiction by A2, A3, XTUPLE_0:1;
end;
Lm11:
for G being c-regular _Graph, v being Vertex of G
holds card(E0(G,v) \/ E1(G,v)) = c
proof
let G be c-regular _Graph, v be Vertex of G;
thus card(E0(G,v) \/ E1(G,v))
= card E0(G,v) +` card E1(G,v) by Lm10, CARD_2:35
.= card E0(G,v) +` card [: [:{v}, v.edgesIn():],{1} :] by ZFMISC_1:def 3
.= card E0(G,v) +` card [: {v}, v.edgesIn() :] by CARD_1:69
.= card E0(G,v) +` card [: v.edgesIn(), {v} :] by CARD_2:4
.= card E0(G,v) +` v.inDegree() by CARD_1:69
.= card [: [:{v}, v.edgesOut():],{0} :] +` v.inDegree() by ZFMISC_1:def 3
.= card [: {v}, v.edgesOut() :] +` v.inDegree() by CARD_1:69
.= card [: v.edgesOut(), {v} :] +` v.inDegree() by CARD_2:4
.= v.degree() by CARD_1:69
.= c by Def4;
end;
Lm12:
for v, w being Vertex of G st E0(G,v) meets E0(G,w) holds v = w
proof
let v,w be Vertex of G;
assume E0(G,v) meets E0(G,w);
then consider z being object such that
A1: z in E0(G,v) & z in E0(G,w) by XBOOLE_0:3;
consider w0,x0,y0 being object such that
A2: w0 in {v} & x0 in v.edgesOut() & y0 in {0} & z = [w0,x0,y0]
by A1, MCART_1:68;
consider w1,x1,y1 being object such that
A3: w1 in {w} & x1 in w.edgesOut() & y1 in {0} & z = [w1,x1,y1]
by A1, MCART_1:68;
w0 = v & w1 = w by A2, A3, TARSKI:def 1;
hence thesis by A2, A3, XTUPLE_0:3;
end;
Lm13:
for v, w being Vertex of G st E1(G,v) meets E1(G,w) holds v = w
proof
let v,w be Vertex of G;
assume E1(G,v) meets E1(G,w);
then consider z being object such that
A1: z in E1(G,v) & z in E1(G,w) by XBOOLE_0:3;
consider w0,x0,y0 being object such that
A2: w0 in {v} & x0 in v.edgesIn() & y0 in {1} & z = [w0,x0,y0]
by A1, MCART_1:68;
consider w1,x1,y1 being object such that
A3: w1 in {w} & x1 in w.edgesIn() & y1 in {1} & z = [w1,x1,y1]
by A1, MCART_1:68;
w0 = v & w1 = w by A2, A3, TARSKI:def 1;
hence thesis by A2, A3, XTUPLE_0:3;
end;
Lm14:
P(G) is mutually-disjoint
proof
now
let x,y be set;
assume A1: x in P(G) & y in P(G) & x <> y;
then consider v being Vertex of G such that
A2: x = E0(G,v) \/ E1(G,v) & v is non isolated;
consider w being Vertex of G such that
A3: y = E0(G,w) \/ E1(G,w) & w is non isolated by A1;
assume x meets y;
then consider z being object such that
A4: z in x & z in y by XBOOLE_0:3;
per cases by A2, A3, A4, XBOOLE_0:def 3;
suppose z in E0(G,v) & z in E0(G,w);
then v = w by Lm12, XBOOLE_0:3;
hence contradiction by A1, A2, A3;
end;
suppose z in E0(G,v) & z in E1(G,w);
hence contradiction by Lm10, XBOOLE_0:3;
end;
suppose z in E1(G,v) & z in E0(G,w);
hence contradiction by Lm10, XBOOLE_0:3;
end;
suppose z in E1(G,v) & z in E1(G,w);
then v = w by Lm13, XBOOLE_0:3;
hence contradiction by A1, A2, A3;
end;
end;
hence thesis by TAXONOM2:def 5;
end;
:: holds more generally for graphs without isolated vertices
Lm15:
for c being non empty Cardinal, G being c-regular _Graph
holds card P(G) = G.order()
proof
let c be non empty Cardinal, G be c-regular _Graph;
set V = the_Vertices_of G;
deffunc G(object) = E0(G,In($1,V)) \/ E1(G,In($1,V));
consider g being Function such that
A1: dom g = V & for x being object st x in V holds g.x = G(x)
from FUNCT_1:sch 3;
now
let y be object;
hereby
assume y in rng g;
then consider v being object such that
A2: v in dom g & g.v = y by FUNCT_1:def 3;
reconsider v as Vertex of G by A1, A2;
A3: g.v = E0(G,In(v,V)) \/ E1(G,In(v,V)) by A1
.= E0(G,v) \/ E1(G,v);
v.degree() = c by Def4;
then v is non isolated by GLIB_000:157;
hence y in P(G) by A2, A3;
end;
assume y in P(G);
then consider v being Vertex of G such that
A4: y = E0(G,v) \/ E1(G,v) & v is non isolated;
A5: v in dom g by A1;
g.v = E0(G,In(v,V)) \/ E1(G,v) by A1
.= y by A4;
hence y in rng g by A5, FUNCT_1:3;
end;
then A6: rng g = P(G) by TARSKI:2;
now
let x1,x2 be object;
assume A7: x1 in dom g & x2 in dom g & g.x1 = g.x2;
assume A8: x1 <> x2;
reconsider x1,x2 as Vertex of G by A1, A7;
A9: g.x1 = E0(G,In(x1,V)) \/ E1(G,In(x1,V)) by A1
.= E0(G,x1) \/ E1(G,x1);
A10: g.x2 = E0(G,In(x2,V)) \/ E1(G,In(x2,V)) by A1
.= E0(G,x2) \/ E1(G,x2);
E0(G,x1) misses E0(G,x2) & E1(G,x1) misses E1(G,x2) by A8, Lm12, Lm13;
then A11: E0(G,x1) = E1(G,x2) & E1(G,x1) = E0(G,x2)
by A7, A9, A10, XBOOLE_1:72;
E0(G,x1) misses E1(G,x2) & E1(G,x1) misses E0(G,x2) by Lm10;
then A12: E0(G,x1) = {} & E1(G,x1) = {} by A11, XBOOLE_1:66;
x1.degree() <> 0 by Def4;
then per cases by GLIB_000:155, GLIB_000:157;
suppose x1.edgesIn() <> {};
then consider e being object such that
A13: e in x1.edgesIn() by XBOOLE_0:def 1;
x1 in {x1} & 1 in {1} by TARSKI:def 1;
then [x1,e,1] in E1(G,x1) by A13, MCART_1:69;
hence contradiction by A12;
end;
suppose x1.edgesOut() <> {};
then consider e being object such that
A14: e in x1.edgesOut() by XBOOLE_0:def 1;
x1 in {x1} & 0 in {0} by TARSKI:def 1;
then [x1,e,0] in E0(G,x1) by A14, MCART_1:69;
hence contradiction by A12;
end;
end;
hence thesis by A1, A6, FUNCT_1:def 4, CARD_1:70;
end;
Lm16:
rng F(G) = union P(G)
proof
:: check definition of rng
now
let y be object;
hereby
assume y in union P(G);
then consider Y being set such that
A1: y in Y & Y in P(G) by TARSKI:def 4;
consider v being Vertex of G such that
A2: Y = E0(G,v) \/ E1(G,v) & v is non isolated by A1;
:: y is either of the form [v,e,0] or [v,e,1], check both
thus ex x being object st x in dom F(G) & y = F(G).x
proof
:: symmetric cases
per cases by A1, A2, XBOOLE_0:def 3;
suppose y in E0(G,v);
then consider v0,e0,y0 being object such that
A3: v0 in {v} & e0 in v.edgesOut() & y0 in {0} & y = [v0,e0,y0]
by MCART_1:68;
take [e0,0];
A4: e0 in the_Edges_of G & 0 in {0,1} by A3, TARSKI:def 2;
dom F(G) = [: the_Edges_of G, {0,1} :] by Lm9;
hence [e0,0] in dom F(G) by A4, ZFMISC_1:def 2;
A5: y0 = 0 by A3, TARSKI:def 1;
dom F0(G) = [: the_Edges_of G, {0} :]
& dom F1(G) = [: the_Edges_of G, {1} :] by Lm5;
then A6: [e0,0] in dom F0(G) by A3, A5, ZFMISC_1:def 2;
A7: dom H0(G) = the_Edges_of G by Lm4;
v0 = v by A3, TARSKI:def 1;
then A8: (the_Source_of G).e0 = v0 by A3, GLIB_000:58;
A9: dom the_Source_of G = the_Edges_of G by FUNCT_2:def 1;
A10: dom id the_Edges_of G = the_Edges_of G & dom id {0} = {0};
A11: dom F0(G) misses dom F1(G) by Lm6;
thus y = [[v0,e0],0] by A3, A5, XTUPLE_0:def 4
.= [[(the_Source_of G).e0,(id the_Edges_of G).e0],0]
by A4, A8, FUNCT_1:18
.= [H0(G).e0,0] by A4, A9, A10, FUNCT_3:49
.= [H0(G).e0,(id{0}).y0] by A3, A5, FUNCT_1:18
.= F0(G).(e0,y0) by A3, A7, A10, FUNCT_3:def 8
.= F0(G).[e0,0] by A5, BINOP_1:def 1
.= F(G).[e0,0] by A6, A11, FUNCT_4:16;
end;
suppose y in E1(G,v);
then consider v1,e1,y1 being object such that
A12: v1 in {v} & e1 in v.edgesIn() & y1 in {1} & y = [v1,e1,y1]
by MCART_1:68;
take [e1,1];
A13: e1 in the_Edges_of G & 1 in {0,1} by A12, TARSKI:def 2;
dom F(G) = [: the_Edges_of G, {0,1} :] by Lm9;
hence [e1,1] in dom F(G) by A13, ZFMISC_1:def 2;
A14: y1 = 1 by A12, TARSKI:def 1;
dom F0(G) = [: the_Edges_of G, {0} :]
& dom F1(G) = [: the_Edges_of G, {1} :] by Lm5;
then A15: [e1,1] in dom F1(G) by A12, A14, ZFMISC_1:def 2;
A16: dom H1(G) = the_Edges_of G by Lm4;
v1 = v by A12, TARSKI:def 1;
then A17: (the_Target_of G).e1 = v1 by A12, GLIB_000:56;
A18: dom the_Target_of G = the_Edges_of G by FUNCT_2:def 1;
A19: dom id the_Edges_of G = the_Edges_of G & dom id {1} = {1};
thus y = [[v1,e1],1] by A12, A14, XTUPLE_0:def 4
.= [[(the_Target_of G).e1,(id the_Edges_of G).e1],1]
by A13, A17, FUNCT_1:18
.= [H1(G).e1,1] by A13, A18, A19, FUNCT_3:49
.= [H1(G).e1,(id{1}).y1] by A12, A14, FUNCT_1:18
.= F1(G).(e1,y1) by A12, A16, A19, FUNCT_3:def 8
.= F1(G).[e1,1] by A14, BINOP_1:def 1
.= F(G).[e1,1] by A15, FUNCT_4:13;
end;
end;
end;
given x being object such that
A20: x in dom F(G) & y = F(G).x;
x in [: the_Edges_of G, {0,1} :] by A20, Lm9;
then consider e,z being object such that
A21: e in the_Edges_of G & z in {0,1} & x = [e,z] by ZFMISC_1:def 2;
:: symmetric cases
per cases by A21, TARSKI:def 2;
suppose A22: z = 0;
then A23: z in {0} & z in dom id {0} by TARSKI:def 1;
A24: dom H0(G) = the_Edges_of G by Lm4;
A25: dom id the_Edges_of G = the_Edges_of G &
dom the_Source_of G = the_Edges_of G by FUNCT_2:def 1;
[e,z] in [: the_Edges_of G, {0} :] by A21, A23, ZFMISC_1:def 2;
then [e,z] in dom F0(G) & dom F0(G) misses dom F1(G)
by Lm5, Lm6;
then A26: y = F0(G).[e,z] by A20, A21, FUNCT_4:16
.= F0(G).(e,z) by BINOP_1:def 1
.= [H0(G).e,(id{0}).z] by A21, A23, A24, FUNCT_3:def 8
.= [H0(G).e,z] by A23, FUNCT_1:18
.= [[(the_Source_of G).e,(id the_Edges_of G).e],0]
by A21, A22, A25, FUNCT_3:49
.= [[(the_Source_of G).e,e],0] by A21, FUNCT_1:18
.= [(the_Source_of G).e,e,0] by XTUPLE_0:def 4;
(the_Source_of G).e in rng the_Source_of G by A21, A25, FUNCT_1:3;
then reconsider v = (the_Source_of G).e as Vertex of G;
A27: v in {v} & e in v.edgesOut() by A21, GLIB_000:58, TARSKI:def 1;
then A28: v is non isolated by GLIB_000:155;
[v,e,0] in E0(G,v) by A22, A23, A27, MCART_1:69;
then A29: y in E0(G,v) \/ E1(G,v) by A26, XBOOLE_0:def 3;
E0(G,v) \/ E1(G,v) in P(G) by A28;
hence y in union P(G) by A29, TARSKI:def 4;
end;
suppose A30: z = 1;
then A31: z in {1} & z in dom id {1} by TARSKI:def 1;
A32: dom H1(G) = the_Edges_of G by Lm4;
A33: dom id the_Edges_of G = the_Edges_of G &
dom the_Target_of G = the_Edges_of G by FUNCT_2:def 1;
[e,z] in [: the_Edges_of G, {1} :] by A21, A31, ZFMISC_1:def 2;
then [e,z] in dom F1(G) by Lm5;
then A34: y = F1(G).[e,z] by A20, A21, FUNCT_4:13
.= F1(G).(e,z) by BINOP_1:def 1
.= [H1(G).e,(id{1}).z] by A21, A31, A32, FUNCT_3:def 8
.= [H1(G).e,z] by A31, FUNCT_1:18
.= [[(the_Target_of G).e,(id the_Edges_of G).e],1]
by A21, A30, A33, FUNCT_3:49
.= [[(the_Target_of G).e,e],1] by A21, FUNCT_1:18
.= [(the_Target_of G).e,e,1] by XTUPLE_0:def 4;
(the_Target_of G).e in rng the_Target_of G by A21, A33, FUNCT_1:3;
then reconsider v = (the_Target_of G).e as Vertex of G;
A35: v in {v} & e in v.edgesIn() by A21, GLIB_000:56, TARSKI:def 1;
then A36: v is non isolated by GLIB_000:155;
[v,e,1] in E1(G,v) by A30, A31, A35, MCART_1:69;
then A37: y in E0(G,v) \/ E1(G,v) by A34, XBOOLE_0:def 3;
E0(G,v) \/ E1(G,v) in P(G) by A36;
hence y in union P(G) by A37, TARSKI:def 4;
end;
end;
hence thesis by FUNCT_1:def 3;
end;
theorem
for G being c-regular _Graph holds 2*`G.size() = c*`G.order()
proof
let G be c-regular _Graph;
per cases;
suppose c is empty;
then A1: c*`G.order() = 0 & G is edgeless by CARD_2:20;
then G.size() = 0;
hence thesis by A1, CARD_2:20;
end;
suppose A2: c is non empty;
A3: for A being set st A in P(G) holds card A = c
proof
let A be set;
assume A in P(G);
then consider v being Vertex of G such that
A4: A = E0(G,v) \/ E1(G,v) & v is non isolated;
thus thesis by A4, Lm11;
end;
thus 2*`G.size() = G.size()*`card {0,1} by CARD_2:57
.= card [: card the_Edges_of G, card {0,1} :] by CARD_2:def 2
.= card [: the_Edges_of G, {0,1} :] by CARD_2:7
.= card dom F(G) by Lm9
.= card rng F(G) by Lm8, CARD_1:70
.= card union P(G) by Lm16
.= c*`card P(G) by A3, Lm14, Th56
.= c*`G.order() by A2, Lm15;
end;
end;
begin :: The Degree Map and Degree Sequence
definition
let G be _Graph;
func G.degreeMap() -> ManySortedSet of the_Vertices_of G means
:Def11:
for v being Vertex of G holds it.v = v.degree();
existence
proof
deffunc F(object) = In($1,the_Vertices_of G).degree();
consider f being ManySortedSet of the_Vertices_of G such that
A1: for v being object st v in the_Vertices_of G holds f.v = F(v)
from PBOOLE:sch 4;
take f;
let v be Vertex of G;
thus f.v = In(v,the_Vertices_of G).degree() by A1
.= v.degree();
end;
uniqueness
proof
let f1, f2 be ManySortedSet of the_Vertices_of G;
assume that
A2: for v being Vertex of G holds f1.v = v.degree() and
A3: for v being Vertex of G holds f2.v = v.degree();
now
let v be object;
assume v in the_Vertices_of G;
then reconsider v0 = v as Vertex of G;
thus f1.v = v0.degree() by A2
.= f2.v by A3;
end;
hence thesis by PBOOLE:3;
end;
func G.inDegreeMap() -> ManySortedSet of the_Vertices_of G means
:Def12:
for v being Vertex of G holds it.v = v.inDegree();
existence
proof
deffunc F(object) = In($1,the_Vertices_of G).inDegree();
consider f being ManySortedSet of the_Vertices_of G such that
A4: for v being object st v in the_Vertices_of G holds f.v = F(v)
from PBOOLE:sch 4;
take f;
let v be Vertex of G;
thus f.v = In(v,the_Vertices_of G).inDegree() by A4
.= v.inDegree();
end;
uniqueness
proof
let f1, f2 be ManySortedSet of the_Vertices_of G;
assume that
A5: for v being Vertex of G holds f1.v = v.inDegree() and
A6: for v being Vertex of G holds f2.v = v.inDegree();
now
let v be object;
assume v in the_Vertices_of G;
then reconsider v0 = v as Vertex of G;
thus f1.v = v0.inDegree() by A5
.= f2.v by A6;
end;
hence thesis by PBOOLE:3;
end;
func G.outDegreeMap() -> ManySortedSet of the_Vertices_of G means
:Def13:
for v being Vertex of G holds it.v = v.outDegree();
existence
proof
deffunc F(object) = In($1,the_Vertices_of G).outDegree();
consider f being ManySortedSet of the_Vertices_of G such that
A7: for v being object st v in the_Vertices_of G holds f.v = F(v)
from PBOOLE:sch 4;
take f;
let v be Vertex of G;
thus f.v = In(v,the_Vertices_of G).outDegree() by A7
.= v.outDegree();
end;
uniqueness
proof
let f1, f2 be ManySortedSet of the_Vertices_of G;
assume that
A8: for v being Vertex of G holds f1.v = v.outDegree() and
A9: for v being Vertex of G holds f2.v = v.outDegree();
now
let v be object;
assume v in the_Vertices_of G;
then reconsider v0 = v as Vertex of G;
thus f1.v = v0.outDegree() by A8
.= f2.v by A9;
end;
hence thesis by PBOOLE:3;
end;
end;
registration
let G be _Graph;
cluster G.degreeMap() -> Cardinal-yielding;
coherence
proof
now
let x be object;
assume x in dom G.degreeMap();
then reconsider v = x as Vertex of G;
G.degreeMap().x = v.degree() by Def11;
hence G.degreeMap().x is Cardinal;
end;
hence thesis by CARD_3:def 1;
end;
cluster G.inDegreeMap() -> Cardinal-yielding;
coherence
proof
now
let x be object;
assume x in dom G.inDegreeMap();
then reconsider v = x as Vertex of G;
G.inDegreeMap().x = v.inDegree() by Def12;
hence G.inDegreeMap().x is Cardinal;
end;
hence thesis by CARD_3:def 1;
end;
cluster G.outDegreeMap() -> Cardinal-yielding;
coherence
proof
now
let x be object;
assume x in dom G.outDegreeMap();
then reconsider v = x as Vertex of G;
G.outDegreeMap().x = v.outDegree() by Def13;
hence G.outDegreeMap().x is Cardinal;
end;
hence thesis by CARD_3:def 1;
end;
end;
theorem Th59:
for G being _Graph holds card G.degreeMap() = G.order() &
card G.inDegreeMap() = G.order() & card G.outDegreeMap() = G.order()
proof
let G be _Graph;
dom G.degreeMap() = the_Vertices_of G &
dom G.inDegreeMap() = the_Vertices_of G &
dom G.outDegreeMap() = the_Vertices_of G by PARTFUN1:def 2;
hence thesis by CARD_1:62;
end;
theorem Th60:
for G being _Graph, v being Vertex of G
holds G.degreeMap().v = G.inDegreeMap().v +` G.outDegreeMap().v
proof
let G be _Graph, v be Vertex of G;
thus G.degreeMap().v = v.degree() by Def11
.= G.inDegreeMap().v +` v.outDegree() by Def12
.= G.inDegreeMap().v +` G.outDegreeMap().v by Def13;
end;
registration
let G be locally-finite _Graph;
cluster G.degreeMap() -> natural-valued;
coherence
proof
now
let x be object;
assume x in dom G.degreeMap();
then reconsider v = x as Vertex of G;
G.degreeMap().x = v.degree() by Def11;
hence G.degreeMap().x is natural;
end;
hence thesis by VALUED_0:def 12;
end;
cluster G.inDegreeMap() -> natural-valued;
coherence
proof
now
let x be object;
assume x in dom G.inDegreeMap();
then reconsider v = x as Vertex of G;
G.inDegreeMap().x = v.inDegree() by Def12;
hence G.inDegreeMap().x is natural;
end;
hence thesis by VALUED_0:def 12;
end;
cluster G.outDegreeMap() -> natural-valued;
coherence
proof
now
let x be object;
assume x in dom G.outDegreeMap();
then reconsider v = x as Vertex of G;
G.outDegreeMap().x = v.outDegree() by Def13;
hence G.outDegreeMap().x is natural;
end;
hence thesis by VALUED_0:def 12;
end;
end;
definition
let G be locally-finite _Graph;
redefine func G.degreeMap() -> Function of the_Vertices_of G, NAT; :: redefines .degreeMap() (GLIB_016, definition)
coherence
proof
A1: dom G.degreeMap() = the_Vertices_of G by PARTFUN1:def 2;
rng G.degreeMap() c= NAT by VALUED_0:def 6;
hence thesis by A1, FUNCT_2:2;
end;
redefine func G.inDegreeMap() -> Function of the_Vertices_of G, NAT; :: redefines .inDegreeMap() (GLIB_016, definition)
coherence
proof
A2: dom G.inDegreeMap() = the_Vertices_of G by PARTFUN1:def 2;
rng G.inDegreeMap() c= NAT by VALUED_0:def 6;
hence thesis by A2, FUNCT_2:2;
end;
redefine func G.outDegreeMap() -> Function of the_Vertices_of G, NAT; :: redefines .outDegreeMap() (GLIB_016, definition)
coherence
proof
A3: dom G.outDegreeMap() = the_Vertices_of G by PARTFUN1:def 2;
rng G.outDegreeMap() c= NAT by VALUED_0:def 6;
hence thesis by A3, FUNCT_2:2;
end;
end;
registration
let G be vertex-finite _Graph;
cluster G.degreeMap() -> finite;
coherence
proof
card G.degreeMap() = G.order() by Th59;
hence thesis;
end;
cluster G.inDegreeMap() -> finite;
coherence
proof
card G.inDegreeMap() = G.order() by Th59;
hence thesis;
end;
cluster G.outDegreeMap() -> finite;
coherence
proof
card G.outDegreeMap() = G.order() by Th59;
hence thesis;
end;
end;
theorem Th61:
for c being Cardinal, G being _trivial c-edge _Graph, v being Vertex of G
holds G.inDegreeMap() = v .--> c & G.outDegreeMap() = v .--> c &
G.degreeMap() = v .--> (2*`c)
proof
let c be Cardinal, G be _trivial c-edge _Graph, v be Vertex of G;
consider v0 being Vertex of G such that
A1: the_Vertices_of G = {v0} by GLIB_000:22;
set f = v .--> c;
A2: v = v0 by A1, TARSKI:def 1;
dom f = dom({v}-->c) by FUNCOP_1:def 9
.= the_Vertices_of G by A1, A2;
then A3: dom f = dom G.inDegreeMap() & dom f = dom G.outDegreeMap()
by PARTFUN1:def 2;
now
let x be object;
assume x in dom G.inDegreeMap();
then reconsider w = x as Vertex of G;
A4: w = v by A1, A2, TARSKI:def 1;
hence f.x = c by FUNCOP_1:72
.= G.size() by GLIB_013:def 4
.= v.inDegree() by GLIB_000:149
.= G.inDegreeMap().x by A4, Def12;
end;
hence G.inDegreeMap() = f by A3, FUNCT_1:2;
now
let x be object;
assume x in dom G.outDegreeMap();
then reconsider w = x as Vertex of G;
A5: w = v by A1, A2, TARSKI:def 1;
hence f.x = c by FUNCOP_1:72
.= G.size() by GLIB_013:def 4
.= v.outDegree() by GLIB_000:149
.= G.outDegreeMap().x by A5, Def13;
end;
hence G.outDegreeMap() = f by A3, FUNCT_1:2;
set g = v .--> (2*`c);
A6: dom g = dom({v}-->2*`c) by FUNCOP_1:def 9
.= dom G.degreeMap() by A1, A2, PARTFUN1:def 2;
now
let x be object;
assume x in dom G.degreeMap();
then reconsider w = x as Vertex of G;
A7: w = v by A1, A2, TARSKI:def 1;
hence g.x = 2*`c by FUNCOP_1:72
.= c +` c by CARD_2:23
.= G.size() +` c by GLIB_013:def 4
.= G.size() +` G.size() by GLIB_013:def 4
.= v.degree() by GLIB_000:149
.= G.degreeMap().x by A7, Def11;
end;
hence thesis by A6, FUNCT_1:2;
end;
registration
let G be _trivial _Graph;
cluster G.degreeMap() -> trivial;
coherence
proof
G is G.size()-edge by GLIB_013:def 4;
then G.degreeMap() = (the Vertex of G) .--> (2*`G.size()) by Th61;
hence thesis;
end;
cluster G.inDegreeMap() -> trivial;
coherence
proof
G is G.size()-edge by GLIB_013:def 4;
then G.inDegreeMap() = (the Vertex of G) .--> G.size() by Th61;
hence thesis;
end;
cluster G.outDegreeMap() -> trivial;
coherence
proof
G is G.size()-edge by GLIB_013:def 4;
then G.outDegreeMap() = (the Vertex of G) .--> G.size() by Th61;
hence thesis;
end;
end;
:: theorem
:: for G1, G2 being _Graph, f being PVertexMapping of G1, G2
:: st f is isomorphism holds G2.degreeMap() = G1.degreeMap() * f;
::
:: theorem
:: for G1, G2 being _Graph, f being PVertexMapping of G1, G2
:: st f is Disomorphism holds
:: G2.inDegreeMap() = G1.inDegreeMap() * f &
:: G2.outDegreeMap() = G1.outDegreeMap() * f;
::
:: theorem
:: for G1, G2 being _Graph st G1 == G2 holds
:: G1.degreeMap() = G2.degreeMap() & G1.inDegreeMap() = G2.inDegreeMap() &
:: G1.outDegreeMap() = G2.outDegreeMap();
::
:: theorem
:: for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
:: holds G1.degreeMap() = G2.degreeMap();
theorem
for G2 being _Graph, V being set, G1 being addVertices of G2, V
holds G1.degreeMap() = G2.degreeMap() +* ((V\the_Vertices_of G2) --> 0) &
G1.inDegreeMap() = G2.inDegreeMap() +* ((V\the_Vertices_of G2) --> 0) &
G1.outDegreeMap() = G2.outDegreeMap() +* ((V\the_Vertices_of G2) --> 0)
proof
let G2 be _Graph, V be set, G1 be addVertices of G2, V;
set f = (V\the_Vertices_of G2) --> 0;
A1: dom G2.degreeMap() = the_Vertices_of G2 & dom G2.inDegreeMap()
= the_Vertices_of G2 & dom G2.outDegreeMap() = the_Vertices_of G2
by PARTFUN1:def 2;
A2: the_Vertices_of G1 = the_Vertices_of G2 \/ V by GLIB_006:def 10;
A3: the_Vertices_of G2 \/ (V \ the_Vertices_of G2)
= the_Vertices_of G1 by A2, XBOOLE_1:39;
A4: dom G1.degreeMap()
= dom G2.degreeMap() \/ dom f by A1, A3, PARTFUN1:def 2
.= dom(G2.degreeMap() +* f) by FUNCT_4:def 1;
now
let x be object;
assume x in dom G1.degreeMap();
then reconsider v = x as Vertex of G1;
per cases;
suppose A5: v in dom f;
then A6: v is isolated by GLIB_006:88;
thus G1.degreeMap().x = v.degree() by Def11
.= 0 by A6, GLIB_000:157
.= f.x
.= (G2.degreeMap() +* f).x by A5, FUNCT_4:13;
end;
suppose A7: not v in dom f;
then not v in V or v in the_Vertices_of G2 by XBOOLE_0:def 5;
then reconsider v9 = v as Vertex of G2 by A2, XBOOLE_0:def 3;
thus G1.degreeMap().x = v.degree() by Def11
.= v9.degree() by GLIBPRE0:45
.= G2.degreeMap().x by Def11
.= (G2.degreeMap() +* f).x by A7, FUNCT_4:11;
end;
end;
hence G1.degreeMap() = G2.degreeMap() +* f by A4, FUNCT_1:2;
A8: dom G1.inDegreeMap()
= dom G2.inDegreeMap() \/ dom f by A1, A3, PARTFUN1:def 2
.= dom(G2.inDegreeMap() +* f) by FUNCT_4:def 1;
now
let x be object;
assume x in dom G1.inDegreeMap();
then reconsider v = x as Vertex of G1;
per cases;
suppose A9: v in dom f;
then A10: v is isolated by GLIB_006:88;
thus G1.inDegreeMap().x = v.inDegree() by Def12
.= 0 by A10, GLIB_000:156
.= f.x
.= (G2.inDegreeMap() +* f).x by A9, FUNCT_4:13;
end;
suppose A11: not v in dom f;
then not v in V or v in the_Vertices_of G2 by XBOOLE_0:def 5;
then reconsider v9 = v as Vertex of G2 by A2, XBOOLE_0:def 3;
thus G1.inDegreeMap().x = v.inDegree() by Def12
.= v9.inDegree() by GLIBPRE0:45
.= G2.inDegreeMap().x by Def12
.= (G2.inDegreeMap() +* f).x by A11, FUNCT_4:11;
end;
end;
hence G1.inDegreeMap() = G2.inDegreeMap() +* f by A8, FUNCT_1:2;
A12: dom G1.outDegreeMap()
= dom G2.outDegreeMap() \/ dom f by A1, A3, PARTFUN1:def 2
.= dom(G2.outDegreeMap() +* f) by FUNCT_4:def 1;
now
let x be object;
assume x in dom G1.outDegreeMap();
then reconsider v = x as Vertex of G1;
per cases;
suppose A13: v in dom f;
then A14: v is isolated by GLIB_006:88;
thus G1.outDegreeMap().x = v.outDegree() by Def13
.= 0 by A14, GLIB_000:156
.= f.x
.= (G2.outDegreeMap() +* f).x by A13, FUNCT_4:13;
end;
suppose A15: not v in dom f;
then not v in V or v in the_Vertices_of G2 by XBOOLE_0:def 5;
then reconsider v9 = v as Vertex of G2 by A2, XBOOLE_0:def 3;
thus G1.outDegreeMap().x = v.outDegree() by Def13
.= v9.outDegree() by GLIBPRE0:45
.= G2.outDegreeMap().x by Def13
.= (G2.outDegreeMap() +* f).x by A15, FUNCT_4:11;
end;
end;
hence G1.outDegreeMap() = G2.outDegreeMap() +* f by A12, FUNCT_1:2;
end;
theorem
for G being _Graph, C being Component of G holds
C.degreeMap() = G.degreeMap() | the_Vertices_of C &
C.inDegreeMap() = G.inDegreeMap() | the_Vertices_of C &
C.outDegreeMap() = G.outDegreeMap() | the_Vertices_of C
proof
let G be _Graph, C be Component of G;
A1: the_Vertices_of C c= the_Vertices_of G;
A2: dom C.degreeMap() = the_Vertices_of C by PARTFUN1:def 2
.= (the_Vertices_of C) /\ the_Vertices_of G by XBOOLE_1:28
.= (dom G.degreeMap()) /\ the_Vertices_of C by PARTFUN1:def 2
.= dom(G.degreeMap() | the_Vertices_of C) by RELAT_1:61;
now
let x be object;
assume A3: x in dom C.degreeMap();
then reconsider v2 = x as Vertex of C;
reconsider v1 = v2 as Vertex of G by A1, TARSKI:def 3;
thus C.degreeMap().x = v2.degree() by Def11
.= v1.degree() by GLIBPRE0:44
.= G.degreeMap().x by Def11
.= (G.degreeMap() | the_Vertices_of C).x by A3, FUNCT_1:49;
end;
hence C.degreeMap() = G.degreeMap() | the_Vertices_of C by A2, FUNCT_1:2;
A4: dom C.inDegreeMap() = the_Vertices_of C by PARTFUN1:def 2
.= (the_Vertices_of C) /\ the_Vertices_of G by XBOOLE_1:28
.= (dom G.inDegreeMap()) /\ the_Vertices_of C by PARTFUN1:def 2
.= dom(G.inDegreeMap() | the_Vertices_of C) by RELAT_1:61;
now
let x be object;
assume A5: x in dom C.inDegreeMap();
then reconsider v2 = x as Vertex of C;
reconsider v1 = v2 as Vertex of G by A1, TARSKI:def 3;
thus C.inDegreeMap().x = v2.inDegree() by Def12
.= v1.inDegree() by GLIBPRE0:44
.= G.inDegreeMap().x by Def12
.= (G.inDegreeMap() | the_Vertices_of C).x by A5, FUNCT_1:49;
end;
hence C.inDegreeMap() = G.inDegreeMap() | the_Vertices_of C by A4, FUNCT_1:2;
A6: dom C.outDegreeMap() = the_Vertices_of C by PARTFUN1:def 2
.= (the_Vertices_of C) /\ the_Vertices_of G by XBOOLE_1:28
.= (dom G.outDegreeMap()) /\ the_Vertices_of C by PARTFUN1:def 2
.= dom(G.outDegreeMap() | the_Vertices_of C) by RELAT_1:61;
now
let x be object;
assume A7: x in dom C.outDegreeMap();
then reconsider v2 = x as Vertex of C;
reconsider v1 = v2 as Vertex of G by A1, TARSKI:def 3;
thus C.outDegreeMap().x = v2.outDegree() by Def13
.= v1.outDegree() by GLIBPRE0:44
.= G.outDegreeMap().x by Def13
.= (G.outDegreeMap() | the_Vertices_of C).x by A7, FUNCT_1:49;
end;
hence thesis by A6, FUNCT_1:2;
end;
registration
let G be _Graph, v being Denumeration of the_Vertices_of G;
cluster G.degreeMap()*v -> Sequence-like G.order()-element;
coherence
proof
dom G.degreeMap() = the_Vertices_of G by PARTFUN1:def 2
.= rng v by FUNCT_2:def 3;
then A1: dom(G.degreeMap()*v) = dom v by RELAT_1:27
.= G.order() by FUNCT_2:def 1;
then card dom(G.degreeMap()*v) = G.order();
then card(G.degreeMap()*v) = G.order() by CARD_1:62;
hence thesis by A1, ORDINAL1:def 7, CARD_1:def 7;
end;
cluster G.inDegreeMap()*v -> Sequence-like G.order()-element;
coherence
proof
dom G.inDegreeMap() = the_Vertices_of G by PARTFUN1:def 2
.= rng v by FUNCT_2:def 3;
then A2: dom(G.inDegreeMap()*v) = dom v by RELAT_1:27
.= G.order() by FUNCT_2:def 1;
then card dom(G.inDegreeMap()*v) = G.order();
then card(G.inDegreeMap()*v) = G.order() by CARD_1:62;
hence thesis by A2, ORDINAL1:def 7, CARD_1:def 7;
end;
cluster G.outDegreeMap()*v -> Sequence-like G.order()-element;
coherence
proof
dom G.outDegreeMap() = the_Vertices_of G by PARTFUN1:def 2
.= rng v by FUNCT_2:def 3;
then A3: dom(G.outDegreeMap()*v) = dom v by RELAT_1:27
.= G.order() by FUNCT_2:def 1;
then card dom(G.outDegreeMap()*v) = G.order();
then card(G.outDegreeMap()*v) = G.order() by CARD_1:62;
hence thesis by A3, ORDINAL1:def 7, CARD_1:def 7;
end;
end;
theorem Th64:
for G being _finite _Graph, v being Denumeration of the_Vertices_of G
holds G.degreeMap()*v = G.inDegreeMap()*v + G.outDegreeMap()*v
proof
let G be _finite _Graph, v be Denumeration of the_Vertices_of G;
dom G.degreeMap() = the_Vertices_of G by PARTFUN1:def 2
.= rng v by FUNCT_2:def 3;
then A1: dom(G.degreeMap()*v) = dom v by RELAT_1:27;
dom G.inDegreeMap() = the_Vertices_of G by PARTFUN1:def 2
.= rng v by FUNCT_2:def 3;
then A2: dom(G.inDegreeMap()*v) = dom v by RELAT_1:27;
dom G.outDegreeMap() = the_Vertices_of G by PARTFUN1:def 2
.= rng v by FUNCT_2:def 3;
then dom(G.outDegreeMap()*v) = dom v by RELAT_1:27;
then A3: dom(G.degreeMap()*v)=dom(G.inDegreeMap()*v)/\dom(G.outDegreeMap()*v)
by A1, A2;
now
let c be object;
assume c in dom(G.degreeMap()*v);
then A4: c in dom v by A1;
then v.c in rng v by FUNCT_1:3;
then reconsider w = v.c as Vertex of G;
thus (G.degreeMap()*v).c = G.degreeMap().w by A4, FUNCT_1:13
.= G.inDegreeMap().w +` G.outDegreeMap().w by Th60
.= (G.inDegreeMap()*v).c + G.outDegreeMap().w by A4, FUNCT_1:13
.= (G.inDegreeMap()*v).c + (G.outDegreeMap()*v).c by A4, FUNCT_1:13;
end;
hence thesis by A3, VALUED_1:def 1;
end;
theorem Th65:
for G being _finite _Graph, v being Denumeration of the_Vertices_of G
holds G.size() = Sum(G.inDegreeMap()*v) & G.size() = Sum(G.outDegreeMap()*v)
proof
let G be _finite _Graph, v be Denumeration of the_Vertices_of G;
:: first part
deffunc I1(object) = E1(G,v/.$1);
set f1 = XFS2FS(G.inDegreeMap()*v), S1 = {I1(i) where i is Nat : i < len f1};
:: we show that (obviously) card union S1 = Sum f1
:: by using a scheme from MSAFREE5
A1: now
let i,j be Nat;
assume A2: i < len f1 & j < len f1 & i <> j;
then i < len(G.inDegreeMap()*v) & j < len(G.inDegreeMap()*v)
by AFINSQ_1:def 9;
then i in dom(G.inDegreeMap()*v) & j in dom(G.inDegreeMap()*v)
by AFINSQ_1:86;
then i in dom v & j in dom v by FUNCT_1:11;
then v.i<>v.j & v.i=v/.i & v.j=v/.j by A2, FUNCT_1:def 4, PARTFUN1:def 6;
hence I1(i) misses I1(j) by Lm13;
end;
A3: now
let i be Nat;
assume i < len f1;
then i < len(G.inDegreeMap()*v) by AFINSQ_1:def 9;
then A4: i in dom(G.inDegreeMap()*v) by AFINSQ_1:86;
then A5: i in dom v by FUNCT_1:11;
i+1 in dom f1 by A4, AFINSQ_1:95;
then 1 <= i+1 & i+1 <= len f1 by FINSEQ_3:25;
then A6: 1 <= i+1 & i+1 <= len(G.inDegreeMap()*v) by AFINSQ_1:def 9;
thus card I1(i)
= card [:[:{v/.i}, (v/.i).edgesIn():],{1}:] by ZFMISC_1:def 3
.= card [:{v/.i}, (v/.i).edgesIn():] by CARD_1:69
.= card [:(v/.i).edgesIn(), {v/.i}:] by CARD_2:4
.= (v/.i).inDegree() by CARD_1:69
.= G.inDegreeMap().(v/.i) by Def12
.= G.inDegreeMap().(v.i) by A5, PARTFUN1:def 6
.= (G.inDegreeMap()*v).i by A4, FUNCT_1:12
.= (G.inDegreeMap()*v).(i+1-1)
.= f1.(i+1) by A6, AFINSQ_1:def 9;
end;
A7: card union S1 = Sum f1 from MSAFREE5:sch 1(A1,A3);
:: union S1 = rng F1(G) is obvious, if a bit lengthy to prove
:: after that, basic cardinality considerations show the desired result
now
let y be object;
hereby
assume y in union S1;
then consider Y being set such that
A8: y in Y & Y in S1 by TARSKI:def 4;
consider i being Nat such that
A9: Y = I1(i) & i < len f1 by A8;
consider x1,x2,x3 being object such that
A10: x1 in {v/.i} & x2 in (v/.i).edgesIn() & x3 in {1} & y=[x1,x2,x3]
by A8, A9, MCART_1:68;
A11: x1 = v/.i by A10, TARSKI:def 1;
reconsider x = [x2,x3] as object;
take x;
A12: x2 in the_Edges_of G by A10;
then A13: x2 in dom H1(G) & x3 in dom id {1} by A10, Lm4;
x in [: the_Edges_of G, {1} :] by A10, ZFMISC_1:def 2;
hence x in dom F1(G) by Lm5;
thus y = [[x1,x2],x3] by A10, XTUPLE_0:def 4
.= [[(the_Target_of G).x2,x2],x3] by A10, A11, GLIB_000:56
.= [[(the_Target_of G).x2,(id the_Edges_of G).x2],x3]
by A12, FUNCT_1:18
.= [H1(G).x2,x3] by A13, FUNCT_3:def 7
.= [H1(G).x2,(id {1}).x3] by A10, FUNCT_1:18
.= F1(G).(x2,x3) by A13, FUNCT_3:def 8
.= F1(G).x by BINOP_1:def 1;
end;
given x being object such that
A14: x in dom F1(G) & y = F1(G).x;
x in [: the_Edges_of G, {1} :] by A14, Lm5;
then consider x2,x3 being object such that
A15: x2 in the_Edges_of G & x3 in {1} & x = [x2,x3] by ZFMISC_1:def 2;
A16: x2 in dom H1(G) & x3 in dom id {1} by A15, Lm4;
set x1 = (the_Target_of G).x2, i = v".x1;
A17: y = F1(G).(x2,x3) by A14, A15, BINOP_1:def 1
.= [H1(G).x2,(id {1}).x3] by A16, FUNCT_3:def 8
.= [H1(G).x2,x3] by A16, FUNCT_1:18
.= [[x1,(id the_Edges_of G).x2],x3] by A16, FUNCT_3:def 7
.= [[x1,x2],x3] by A15, FUNCT_1:18
.= [x1,x2,x3] by XTUPLE_0:def 4;
x2 in dom the_Target_of G by A15, FUNCT_2:def 1;
then x1 in rng the_Target_of G by FUNCT_1:3;
then reconsider x1 as Vertex of G;
x1 in the_Vertices_of G;
then x1 in rng v by FUNCT_2:def 3;
then A18: v.i = x1 & x1 in dom(v") by FUNCT_1:33, FUNCT_1:35;
then i in rng(v") by FUNCT_1:3;
then A19: i in dom v by FUNCT_1:33;
then A20: i in G.order();
then reconsider i as Ordinal;
i c= G.order() by A20, ORDINAL1:def 2;
then reconsider i as Nat;
dom G.inDegreeMap() = the_Vertices_of G by PARTFUN1:def 2;
then x1 in dom G.inDegreeMap();
then i < len(G.inDegreeMap()*v) by A18, A19, FUNCT_1:11, AFINSQ_1:86;
then i < len f1 by AFINSQ_1:def 9;
then A21: I1(i) in S1 & v/.i = x1 by A18, A19, PARTFUN1:def 6;
x1 in {x1} & x2 in x1.edgesIn() by A15, TARSKI:def 1, GLIB_000:56;
then y in E1(G,x1) by A15, A17, MCART_1:69;
hence y in union S1 by A21, TARSKI:def 4;
end;
then A22: union S1 = rng F1(G) by FUNCT_1:def 3;
reconsider g = G.inDegreeMap()*v as complex-valued XFinSequence;
thus G.size() = card [: the_Edges_of G, {1} :] by CARD_1:69
.= card dom F1(G) by Lm5
.= Sum f1 by A7, A22, CARD_1:70
.= Sum(G.inDegreeMap()*v) by RVSUM_4:64;
:: second part, analogously to first part
deffunc I0(object) = E0(G,v/.$1);
set f0 = XFS2FS(G.outDegreeMap()*v),S0 = {I0(i) where i is Nat : i < len f0};
:: we show that (obviously) card union S0 = Sum f0
:: by using a scheme from MSAFREE5
A23: now
let i,j be Nat;
assume A24: i < len f0 & j < len f0 & i <> j;
then i < len(G.outDegreeMap()*v) & j < len(G.outDegreeMap()*v)
by AFINSQ_1:def 9;
then i in dom(G.outDegreeMap()*v) & j in dom(G.outDegreeMap()*v)
by AFINSQ_1:86;
then i in dom v & j in dom v by FUNCT_1:11;
then v.i<>v.j & v.i=v/.i & v.j=v/.j by A24, FUNCT_1:def 4, PARTFUN1:def 6;
hence I0(i) misses I0(j) by Lm12;
end;
A25: now
let i be Nat;
assume i < len f0;
then i < len(G.outDegreeMap()*v) by AFINSQ_1:def 9;
then A26: i in dom(G.outDegreeMap()*v) by AFINSQ_1:86;
then A27: i in dom v by FUNCT_1:11;
i+1 in dom f0 by A26, AFINSQ_1:95;
then 1 <= i+1 & i+1 <= len f0 by FINSEQ_3:25;
then A28: 1 <= i+1 & i+1 <= len(G.outDegreeMap()*v) by AFINSQ_1:def 9;
thus card I0(i)
= card [:[:{v/.i}, (v/.i).edgesOut():],{0}:] by ZFMISC_1:def 3
.= card [:{v/.i}, (v/.i).edgesOut():] by CARD_1:69
.= card [:(v/.i).edgesOut(), {v/.i}:] by CARD_2:4
.= (v/.i).outDegree() by CARD_1:69
.= G.outDegreeMap().(v/.i) by Def13
.= G.outDegreeMap().(v.i) by A27, PARTFUN1:def 6
.= (G.outDegreeMap()*v).i by A26, FUNCT_1:12
.= (G.outDegreeMap()*v).(i+1-1)
.= f0.(i+1) by A28, AFINSQ_1:def 9;
end;
A29: card union S0 = Sum f0 from MSAFREE5:sch 1(A23,A25);
:: union S0 = rng F0(G) is obvious, if a bit lengthy to prove
:: after that, basic cardinality considerations show the desired result
now
let y be object;
hereby
assume y in union S0;
then consider Y being set such that
A30: y in Y & Y in S0 by TARSKI:def 4;
consider i being Nat such that
A31: Y = I0(i) & i < len f0 by A30;
consider x1,x2,x3 being object such that
A32: x1 in {v/.i} & x2 in (v/.i).edgesOut() & x3 in {0} & y=[x1,x2,x3]
by A30, A31, MCART_1:68;
A33: x1 = v/.i by A32, TARSKI:def 1;
reconsider x = [x2,x3] as object;
take x;
A34: x2 in the_Edges_of G by A32;
then A35: x2 in dom H0(G) & x3 in dom id {0} by A32, Lm4;
x in [: the_Edges_of G, {0} :] by A32, ZFMISC_1:def 2;
hence x in dom F0(G) by Lm5;
thus y = [[x1,x2],x3] by A32, XTUPLE_0:def 4
.= [[(the_Source_of G).x2,x2],x3] by A32, A33, GLIB_000:58
.= [[(the_Source_of G).x2,(id the_Edges_of G).x2],x3]
by A34, FUNCT_1:18
.= [H0(G).x2,x3] by A35, FUNCT_3:def 7
.= [H0(G).x2,(id {0}).x3] by A32, FUNCT_1:18
.= F0(G).(x2,x3) by A35, FUNCT_3:def 8
.= F0(G).x by BINOP_1:def 1;
end;
given x being object such that
A36: x in dom F0(G) & y = F0(G).x;
x in [: the_Edges_of G, {0} :] by A36, Lm5;
then consider x2,x3 being object such that
A37: x2 in the_Edges_of G & x3 in {0} & x = [x2,x3] by ZFMISC_1:def 2;
A38: x2 in dom H0(G) & x3 in dom id {0} by A37, Lm4;
set x1 = (the_Source_of G).x2, i = v".x1;
A39: y = F0(G).(x2,x3) by A36, A37, BINOP_1:def 1
.= [H0(G).x2,(id {0}).x3] by A38, FUNCT_3:def 8
.= [H0(G).x2,x3] by A38, FUNCT_1:18
.= [[x1,(id the_Edges_of G).x2],x3] by A38, FUNCT_3:def 7
.= [[x1,x2],x3] by A37, FUNCT_1:18
.= [x1,x2,x3] by XTUPLE_0:def 4;
x2 in dom the_Source_of G by A37, FUNCT_2:def 1;
then x1 in rng the_Source_of G by FUNCT_1:3;
then reconsider x1 as Vertex of G;
x1 in the_Vertices_of G;
then x1 in rng v by FUNCT_2:def 3;
then A40: v.i = x1 & x1 in dom(v") by FUNCT_1:33, FUNCT_1:35;
then i in rng(v") by FUNCT_1:3;
then A41: i in dom v by FUNCT_1:33;
then A42: i in G.order();
then reconsider i as Ordinal;
i c= G.order() by A42, ORDINAL1:def 2;
then reconsider i as Nat;
dom G.outDegreeMap() = the_Vertices_of G by PARTFUN1:def 2;
then x1 in dom G.outDegreeMap();
then i < len(G.outDegreeMap()*v) by A40, A41, FUNCT_1:11, AFINSQ_1:86;
then i < len f0 by AFINSQ_1:def 9;
then A43: I0(i) in S0 & v/.i = x1 by A40, A41, PARTFUN1:def 6;
x1 in {x1} & x2 in x1.edgesOut() by A37, TARSKI:def 1, GLIB_000:58;
then y in E0(G,x1) by A37, A39, MCART_1:69;
hence y in union S0 by A43, TARSKI:def 4;
end;
then A44: union S0 = rng F0(G) by FUNCT_1:def 3;
reconsider g = G.outDegreeMap()*v as complex-valued XFinSequence;
thus G.size() = card [: the_Edges_of G, {0} :] by CARD_1:69
.= card dom F0(G) by Lm5
.= Sum f0 by A29, A44, CARD_1:70
.= Sum(G.outDegreeMap()*v) by RVSUM_4:64;
end;
theorem Th66:
for G being _finite _Graph, v being Denumeration of the_Vertices_of G
holds 2*G.size() = Sum(G.degreeMap()*v)
proof
let G be _finite _Graph, v be Denumeration of the_Vertices_of G;
thus 2*G.size() = G.size() + G.size()
.= Sum(G.inDegreeMap()*v) + G.size() by Th65
.= Sum(G.inDegreeMap()*v) + Sum(G.outDegreeMap()*v) by Th65
.= Sum(G.inDegreeMap()*v + G.outDegreeMap()*v) by RVSUM_4:49
.= Sum(G.degreeMap()*v) by Th64;
end;
::#MR Handshaking Lemma
theorem
for G being _finite _Graph, k being Nat
st k = card {w where w is Vertex of G : w.degree() is non even}
holds k is even
proof
let G be _finite _Graph, k be Nat;
set W = {w where w is Vertex of G : w.degree() is non even};
assume A1: k = card W;
now
let x be object;
assume x in W;
then consider w being Vertex of G such that
A2: x = w & w.degree() is non even;
thus x in the_Vertices_of G by A2;
end;
then A3: W c= the_Vertices_of G by TARSKI:def 3;
set v = the Denumeration of the_Vertices_of G;
reconsider v9 = W|`v as one-to-one Function by FUNCT_1:58;
set f = v9";
deffunc M(Nat) = (G.degreeMap()*v).$1 mod 2;
consider m being XFinSequence of NAT such that
A4: len m = len(G.degreeMap()*v) and
A5: for k being Nat st k in len(G.degreeMap()*v) holds m.k = M(k)
from AFINSQ_2:sch 1;
A6: dom(G.degreeMap()*v) = dom m &
for i being Nat st i in dom(G.degreeMap()*v)
holds m.i = (G.degreeMap()*v).i mod 2 by A4, A5;
A7: dom f = rng(v9) by FUNCT_1:33
.= rng v /\ W by RELAT_1:88
.= the_Vertices_of G /\ W by FUNCT_2:def 3
.= W by A3, XBOOLE_1:28;
now
let y be object;
hereby
assume y in m"{1};
then A8: y in dom m & m.y in {1} by FUNCT_1:def 7;
reconsider x = v.y as object;
take x;
A9: y in dom v by A4, A8, FUNCT_1:11;
1 = m.y by A8, TARSKI:def 1
.= (G.degreeMap()*v).y mod 2 by A8, A4, A5
.= G.degreeMap().(v.y) mod 2 by A9, FUNCT_1:13
.= G.degreeMap().(v/.y) mod 2 by A9, PARTFUN1:def 6
.= (v/.y).degree() mod 2 by Def11;
then (v/.y).degree() is non even by NAT_2:21;
then (v/.y) in W;
then A10: x in W by A9, PARTFUN1:def 6;
x in rng v by A9, FUNCT_1:3;
then x in rng v9 by A10, RELAT_1:84;
hence x in dom f by FUNCT_1:33;
thus y = v".x by A9, FUNCT_1:34
.= (v"|W).x by A10, FUNCT_1:49
.= f.x by GLIB_009:5;
end;
given x being object such that
A11: x in dom f & y = f.x;
x in rng v9 by A11, FUNCT_1:33;
then A12: x in rng v & x in W by RELAT_1:84;
then consider w being Vertex of G such that
A13: x = w & w.degree() is non even;
A14: x in dom(v") by A12, FUNCT_1:33;
A15: y = (v"|W).x by A11, GLIB_009:5
.= v".x by A12, FUNCT_1:49;
then y in rng(v") by A14, FUNCT_1:3;
then A16: y in dom v by FUNCT_1:33;
A17: v.y = x by A12, A15, FUNCT_1:35;
x in the_Vertices_of G by A13;
then x in dom G.degreeMap() by PARTFUN1:def 2;
then A18: y in dom m by A4, A16, A17, FUNCT_1:11;
then m.y = (G.degreeMap()*v).y mod 2 by A4, A5
.= G.degreeMap().x mod 2 by A16, A17, FUNCT_1:13
.= w.degree() mod 2 by A13, Def11
.= 1 by A13, NAT_2:22;
then m.y in {1} by TARSKI:def 1;
hence y in m"{1} by A18, FUNCT_1:def 7;
end;
then A19: rng f = m"{1} by FUNCT_1:def 3;
now
let y be object;
assume y in rng m;
then consider x being object such that
A20: x in dom m & y = m.x by FUNCT_1:def 3;
A21: x in len(G.degreeMap()*v) by A4, A20;
then reconsider x as Ordinal;
x c= len(G.degreeMap()*v) by A21, ORDINAL1:def 2;
then reconsider x as Nat;
y = (G.degreeMap()*v).x mod 2 by A5, A20, A21;
then y = 0 or y = 1 by NAT_D:12;
hence y in {0,1} by TARSKI:def 2;
end;
then A22: rng m c= {0,1} by TARSKI:def 3;
k = 1*card(m"{1}) by A1, A7, A19, CARD_1:70
.= Sum m by A22, AFINSQ_2:68;
then k mod 2 = Sum((G.degreeMap()*v)) mod 2 by A6, NUMERAL1:3
.= (2*G.size()) mod 2 by Th66
.= 0;
hence thesis by NAT_2:21;
end;