:: Underlying Simple Graphs
:: by Sebastian Koch
::
:: Received August 29, 2019
:: Copyright (c) 2019-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FINSEQ_1, SUBSET_1, RELAT_1, FUNCT_1, XXREAL_0, TARSKI,
ARYTM_3, CARD_1, XBOOLE_0, NAT_1, ARYTM_1, GLIB_000, ZFMISC_1, RELAT_2,
GLIB_002, FUNCOP_1, GLIB_001, ABIAN, GLIB_003, GLIB_009, INT_1, RCOMP_1,
EQREL_1, GLIB_006, GLIB_007, FUNCT_4, CHORD, SCMYCIEL, SGRAPH1, GRAPH_1,
ORDINAL4, XCMPLX_0, REWRITE1;
notations TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1,
FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1,
SETWISEO, EQREL_1, FUNCOP_1, FUNCT_4, PARTFUN2, CARD_1, PBOOLE, CARD_3,
NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, VALUED_0, NAT_D,
FINSEQ_1, BSPACE, FINSEQ_4, ABIAN, GLIB_000, STRUCT_0, ALGSTR_0, GROUP_1,
GROUP_2, GROUP_6, GLIB_001, GLIB_002, GLIB_003, CHORD, GLIB_006,
GLIB_007, GLIB_008, FUNCT_7;
constructors DOMAIN_1, FUNCT_4, XXREAL_0, NAT_1, NAT_D, BINOP_2, CARD_2,
FINSEQ_4, PBOOLE, ORDINAL3, WELLORD2, PARTFUN1, RELSET_1, GLIB_000,
STRUCT_0, RELAT_1, FUNCT_1, FUNCT_2, ALGSTR_0, GROUP_1, GLIB_001, ABIAN,
CARD_3, FINSEQ_1, GLIB_002, GLIB_003, SETFAM_1, EQREL_1, GROUP_2,
GROUP_6, GLIB_006, GLIB_007, PARTFUN2, BSPACE, SETWISEO, CHORD, RAT_1,
GLIB_008, FUNCT_7;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XREAL_0, NAT_1,
FINSEQ_1, GLIB_000, GLIB_003, INT_1, CARD_1, FUNCT_2, PARTFUN1, RELSET_1,
GLIB_001, ABIAN, FINSEQ_4, GLIB_006, GLIB_008, CHORD;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
theorems TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XBOOLE_1, CARD_1, RELAT_1,
FUNCT_1, FUNCT_2, FUNCOP_1, FINSEQ_1, FINSEQ_3, FINSEQ_4, NAT_1, NAT_2,
INT_1, NAT_D, POLYFORM, XREAL_1, XXREAL_0, ABIAN, GLIB_000, GLIB_001,
GLIB_002, GLIB_003, GLIB_006, GLIB_007, WELLORD2, EQREL_1, FUNCT_4,
ORDINAL1, CHORD, GLIB_008, MFOLD_2;
schemes SUBSET_1, EQREL_1, FUNCT_1, FINSEQ_1, NAT_1;
begin :: Preliminaries
:: into XBOOLE_1 ?
theorem Th1:
for X, Y being set st Y c= X holds X \ (X \ Y) = Y
proof
let X, Y be set;
assume A1: Y c= X;
thus X \ (X \ Y) = X /\ Y by XBOOLE_1:48
.= Y by A1, XBOOLE_1:28;
end;
:: into RELAT_1 ?
Lm1:
for R being Relation, X being set holds (R|X)~ = X|`(R~)
proof
let R be Relation, X be set;
for a,b being object holds [a,b] in (R|X)~ iff [a,b] in X|`(R~)
proof
let a,b be object;
hereby
assume [a,b] in (R|X)~;
then [b,a] in R|X by RELAT_1:def 7;
then b in X & [b,a] in R by RELAT_1:def 11;
then b in X & [a,b] in R~ by RELAT_1:def 7;
hence [a,b] in X|`(R~) by RELAT_1:def 12;
end;
assume [a,b] in X|`(R~);
then b in X & [a,b] in R~ by RELAT_1:def 12;
then b in X & [b,a] in R by RELAT_1:def 7;
then [b,a] in R|X by RELAT_1:def 11;
hence [a,b] in (R|X)~ by RELAT_1:def 7;
end;
hence thesis by RELAT_1:def 2;
end;
:: into RELAT_1 ?
theorem Th2:
for R being Relation, X being set holds (R|X)~ = X|`(R~) & (X|`R)~ = (R~)|X
proof
let R be Relation, X be set;
thus (R|X)~ = X|`(R~) by Lm1;
((R~)|X)~ = X|`((R~)~) by Lm1;
hence thesis;
end;
::$CT
:: into FUNCT_1 ?
:: reformulation of FUNCT_1:113
theorem
for f being Function, Y being set holds Y|`f = f|dom(Y|`f)
proof
let f be Function, Y be set;
thus Y|`f = f|f"Y by FUNCT_1:113
.= f|dom(Y|`f) by MFOLD_2:1;
end;
:: into FUNCT_1 ?
theorem
for f being one-to-one Function, X being set
holds (f|X)" = X|`(f") & (X|`f)" = (f")|X
proof
let f be one-to-one Function, X be set;
f|X is one-to-one & X|`f is one-to-one by FUNCT_1:52, FUNCT_1:58;
then f" = (f qua Relation)~ & (f|X)" = ((f|X) qua Relation)~ &
(X|`f)" = ((X|`f) qua Relation)~ by FUNCT_1:def 5;
hence thesis by Th2;
end;
::$CT 18
:: into GLIB_001 ?
theorem Th24:
for G being _Graph, v being Vertex of G
holds G.walkOf(v).edgeSeq() = <*>the_Edges_of G
proof
let G be _Graph, v be Vertex of G;
set W = G.walkOf(v);
len W = 2*len W.edgeSeq()+1 by GLIB_001:def 15;
then 1-1 = 2*len W.edgeSeq()+1-1 by GLIB_001:13;
hence thesis;
end;
:: into GLIB_001 ?
theorem Th25:
for G being _Graph, v being Vertex of G
holds G.walkOf(v).edges() = {}
proof
let G be _Graph, v be Vertex of G;
A1: G.walkOf(v).edgeSeq() = <*>the_Edges_of G by Th24 .= {};
thus G.walkOf(v).edges() = rng {} by A1, GLIB_001:def 17
.= {};
end;
:: into GLIB_001
registration
let G be _Graph, W be trivial Walk of G;
cluster W.edges() -> empty trivial;
coherence
proof
ex v being Vertex of G st W = G.walkOf(v) by GLIB_001:128;
hence thesis by Th25;
end;
end;
:: into GLIB_001 ?
registration
let G be _Graph, W be Walk of G;
cluster W.vertices() -> non empty;
coherence
proof
1 <= len W.vertexSeq() by GLIB_001:67;
then W.vertexSeq() <> {};
then rng W.vertexSeq() <> {};
hence thesis by GLIB_001:def 16;
end;
end;
:: into GLIB_001 ?
theorem
for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
st W1.vertexSeq() = W2.vertexSeq() & W1.edgeSeq() = W2.edgeSeq()
holds W1 = W2
proof
let G1, G2 be _Graph, W1 be Walk of G1, W2 be Walk of G2;
assume A1: W1.vertexSeq() = W2.vertexSeq() & W1.edgeSeq() = W2.edgeSeq();
A2: len W1 + 1 = 2 * len W2.vertexSeq() by A1, GLIB_001:def 14
.= len W2 + 1 by GLIB_001:def 14;
for n being Nat st 1 <= n & n <= len W1 holds W1.n = W2.n
proof
let n be Nat;
assume A3: 1 <= n & n <= len W1;
per cases;
suppose n is odd;
then reconsider m=n as odd Element of NAT by ORDINAL1:def 12;
thus W1.n = W1.vertexAt(m) by A3, GLIB_001:def 8
.= W1.vertexSeq().((m+1) div 2) by A3, GLIB_001:72
.= W2.vertexAt(m) by A1, A2, A3, GLIB_001:72
.= W2.n by A2, A3, GLIB_001:def 8;
end;
suppose n is even;
then reconsider m=n as even Element of NAT by ORDINAL1:def 12;
thus W1.n = W1.edgeSeq().(m div 2) by A3, GLIB_001:77
.= W2.n by A1, A2, A3, GLIB_001:77;
end;
end;
hence thesis by A2, FINSEQ_1:def 18;
end;
:: into GLIB_001 ?
theorem
for G being _Graph, p being FinSequence of the_Vertices_of G,
q being FinSequence of the_Edges_of G
st len p = 1 + len q & for n being Element of NAT
st 1 <= n & n+1 <= len p holds q.n Joins p.n, p.(n+1), G
holds ex W being Walk of G st W.vertexSeq() = p & W.edgeSeq() = q
proof
let G be _Graph, p be FinSequence of the_Vertices_of G;
let q be FinSequence of the_Edges_of G;
assume that
A1: len p = 1 + len q and
A2: for n being Element of NAT
st 1 <= n & n+1 <= len p holds q.n Joins p.n, p.(n+1), G;
:: construct the walk
defpred P[object,object] means ex m being Nat st m = $1 &
(m is odd implies $2 = p.((m+1) div 2)) &
(m is even implies $2 = q.(m div 2));
A3: for k being Nat st k in Seg (len p + len q)
ex x being Element of the_Vertices_of G \/ the_Edges_of G st P[k,x]
proof
let k be Nat;
assume k in Seg (len p + len q);
then A4: 1 <= k & k <= len p + len q by FINSEQ_1:1;
per cases;
suppose A5: k is odd;
k+0 <= len p + len q + 1 by A4, XREAL_1:7;
then A6: k <= 2 * len p by A1;
1+1 <= k+1 by A5, ABIAN:12, XREAL_1:6;
then 1 <= (k+1) div 2 by NAT_2:13;
then (k+1) div 2 in dom p by A6, FINSEQ_3:25, NAT_2:25;
then p.((k+1) div 2) in rng p by FUNCT_1:3;
then reconsider x = p.((k+1) div 2) as
Element of the_Vertices_of G \/ the_Edges_of G by XBOOLE_0:def 3;
take x;
take k;
thus k = k;
thus k is odd implies x = p.((k+1) div 2);
thus k is even implies x = q.(k div 2) by A5;
end;
suppose A7: k is even;
A8: k-1 = k-'1 by A4, XREAL_1:233;
reconsider r = k-1 as Nat by A8;
r <= 1 + 2*len q - 1 by A1, A4, XREAL_1:9;
then A9: (r+1) div 2 <= len q by NAT_2:25;
2 <= k
proof
assume A10: k < 2;
consider s being Nat such that
A11: k = 2*s by A7, ABIAN:def 2;
2*s/2 < 1*2/2 by A10, A11, XREAL_1:81;
then s = 0 by NAT_1:14;
hence contradiction by A4, A11;
end;
then 1 <= k div 2 by NAT_2:13;
then k div 2 in dom q by A9, FINSEQ_3:25;
then q.(k div 2) in rng q by FUNCT_1:3;
then reconsider x = q.(k div 2) as
Element of the_Vertices_of G \/ the_Edges_of G by XBOOLE_0:def 3;
take x;
take k;
thus k = k;
thus k is odd implies x = p.((k+1) div 2) by A7;
thus k is even implies x = q.(k div 2);
end;
end;
:: walk construction finished, start with its attributes
consider W being FinSequence of the_Vertices_of G \/ the_Edges_of G such that
A12: dom W = Seg (len p + len q) and
A13: for k being Nat st k in Seg (len p + len q) holds P[k,W.k]
from FINSEQ_1:sch 5(A3);
A14: len W = 2*len q + 1 by A1, A12, FINSEQ_1:def 3;
A15: W.1 in the_Vertices_of G
proof
1+0 <= 1+(len q + len q) by XREAL_1:7;
then consider m being Nat such that
A16: m = 1 and
A17: m is odd implies W.1 = p.((m+1) div 2) and
m is even implies W.1 = q.(m div 2) by A1, A13, FINSEQ_1:1;
A18: W.1 = p.((m+1) div 2) by A16, A17
.= p.1 by A16, NAT_2:3;
1 + 0 <= 1 + len q by XREAL_1:7;
then 1 in dom p by A1, FINSEQ_3:25;
then p.1 in rng p by FUNCT_1:3;
hence thesis by A18;
end;
:: infer the Join property of the walk from A2
for n being odd Element of
NAT st n < len W holds W.(n+1) Joins W.n, W.(n+2), G
proof
let n be odd Element of NAT;
assume A19: n < len W;
set m = (n+1) div 2;
1+1 <= n+1 by ABIAN:12, XREAL_1:6;
then A20: 1 <= (n+1) div 2 by NAT_2:13;
reconsider m as Nat;
A21: 1+0 <= n+1 & 1+0 <= n+2 by XREAL_1:7;
A22: n+2 <= len W by A14, A19, GLIB_001:1;
n+0 <= n+2 & n+1 <= n+2 by XREAL_1:7;
then n <= len W & n+1 <= len W by A22, XXREAL_0:2;
then A23: n in dom W & n+1 in dom W & n+2 in dom W
by A21, A22, ABIAN:12, FINSEQ_3:25;
A24: ((n+2)+1) div 2 = ((n+1)+2) div 2 .= m + 1 by NAT_2:14;
consider n0 being Nat such that
A25: n0 = n and
A26: (n0 is odd implies W.n = p.((n0+1) div 2)) and
(n0 is even implies W.n = q.(n0 div 2)) by A12, A13, A23;
consider n1 being Nat such that
A27: n1 = n+1 and
(n1 is odd implies W.(n+1) = p.((n1+1) div 2)) and
A28: (n1 is even implies W.(n+1) = q.(n1 div 2)) by A12, A13, A23;
consider n2 being Nat such that
A29: n2 = n+2 and
A30: (n2 is odd implies W.(n+2) = p.((n2+1) div 2)) and
(n2 is even implies W.(n+2) = q.(n2 div 2)) by A12, A13, A23;
A31: W.n = p.m by A25, A26;
A32: W.(n+1) = q.m by A27, A28;
A33: W.(n+2) = p.(m+1) by A24, A29, A30;
A34: n+2 <= len p - 1 + len p by A1, A12, A22, FINSEQ_1:def 3;
2*len p - 1 <= 2*len p - 0 by XREAL_1:13;
then n+2 <= 2*len p by A34, XXREAL_0:2;
then ((n+2)+1) div 2 <= len p by NAT_2:25;
then ((n+1)+2) div 2 <= len p;
then m + 1 <= len p by NAT_2:14;
hence thesis by A2, A20, A31, A32, A33;
end;
:: walk is recognized
then reconsider W as Walk of G by A14, A15, GLIB_001:def 3;
take W;
:: show rest of theorem
A35: 2*len W.vertexSeq() = len W + 1 by GLIB_001:def 14
.= len p + len q + 1 by A12, FINSEQ_1:def 3
.= 2*len p by A1;
for k being Nat st 1 <= k & k <= len p holds p.k = W.vertexSeq().k
proof
let k be Nat;
assume A36: 1 <= k & k <= len p;
2*k <= 2*len p by A36, XREAL_1:64;
then A37: 2*k-1 <= len p + 1 + len q - 1 by A1, XREAL_1:9;
2*1 <= 2*k by A36, XREAL_1:64;
then A38: 1+1-1 <= 2*k-1 by XREAL_1:9;
then 2*k-1 in NAT by INT_1:3;
then consider m being Nat such that
A39: m = 2*k-1 and
A40: (m is odd implies W.(2*k-1) = p.((m+1) div 2)) and
(m is even implies W.(2*k-1) = q.(m div 2)) by A13, A37, A38, FINSEQ_1:1;
W.(2*k-1) = p.k by A39, A40;
hence thesis by A35, A36, GLIB_001:def 14;
end;
hence W.vertexSeq() = p by A35, FINSEQ_1:def 18;
A41: 2*len W.edgeSeq() + 1 = 2*len q + 1 by A14, GLIB_001:def 15;
for k being Nat st 1 <= k & k <= len q holds q.k = W.edgeSeq().k
proof
let k be Nat;
assume A42: 1 <= k & k <= len q;
then A43: W.edgeSeq().k = W.(2*k) by A41, GLIB_001:def 15;
2*k <= 2*len q by A42, XREAL_1:64;
then A44: 2*k + 0 <= len q + len q + 1 by XREAL_1:7;
1*1 <= 2*k by A42, XREAL_1:66;
then consider m being Nat such that
A45: m = 2*k and
(m is odd implies W.(2*k) = p.((m+1) div 2)) and
A46: (m is even implies W.(2*k) = q.(m div 2))
by A1, A13, A44, FINSEQ_1:1;
thus thesis by A43, A45, A46;
end;
hence thesis by A41, FINSEQ_1:def 18;
end;
::: into GLIB_001 ?
::: generalization of GLIB_001:113
Lm2:
for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
holds len W1 = len W2 iff W1.length() = W2.length()
proof
let G1, G2 be _Graph, W1 be Walk of G1, W2 be Walk of G2;
hereby
assume A1: len W1 = len W2;
2*W1.length()+1 = len W1 by GLIB_001:112
.= 2*W2.length()+1 by A1, GLIB_001:112;
hence W1.length() = W2.length();
end;
assume A2: W1.length() = W2.length();
thus len W1 = 2*W1.length()+1 by GLIB_001:112
.= len W2 by A2, GLIB_001:112;
end;
:: into GLIB_001 ?
theorem
for G being _Graph, W being Walk of G holds len W.vertexSeq() = W.length()+1
proof
let G be _Graph, W be Walk of G;
2*len W.vertexSeq() = len W +1 by GLIB_001:def 14
.= 2*W.length()+1 +1 by GLIB_001:112
.= 2*(W.length()+1);
hence thesis;
end;
:: into GLIB_001 ?
Lm3:
for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
st W1.vertexSeq() = W2.vertexSeq() holds len W1 = len W2
proof
let G1, G2 be _Graph, W1 be Walk of G1, W2 be Walk of G2;
assume A1: W1.vertexSeq() = W2.vertexSeq();
len W1 + 1 = 2 * len W1.vertexSeq() by GLIB_001:def 14
.= len W2 + 1 by A1, GLIB_001:def 14;
hence len W1 = len W2;
end;
:: into GLIB_001 ?
theorem Th29:
for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
for n being odd Nat st W1.vertexSeq() = W2.vertexSeq() holds W1.n = W2.n
proof
let G1, G2 be _Graph, W1 be Walk of G1, W2 be Walk of G2;
let n be odd Nat;
assume A1: W1.vertexSeq() = W2.vertexSeq();
then A2: len W1 = len W2 by Lm3;
reconsider m = n as odd Element of NAT by ORDINAL1:def 12;
per cases;
suppose A3: n <= len W1;
hence W1.n = W1.vertexAt(n) by GLIB_001:def 8
.= W2.vertexSeq().((m+1) div 2) by A1, A3, GLIB_001:72
.= W2.vertexAt(n) by A2, A3, GLIB_001:72
.= W2.n by A2, A3, GLIB_001:def 8;
end;
suppose n > len W1;
then not n in dom W1 & not n in dom W2 by A2, FINSEQ_3:25;
then W1.n = {} & W2.n = {} by FUNCT_1:def 2;
hence thesis;
end;
end;
:: into GLIB_001 ?
theorem Th30:
for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
st W1.vertexSeq() = W2.vertexSeq() holds
len W1 = len W2 & W1.length() = W2.length() &
W1.first() = W2.first() & W1.last() = W2.last() &
W2 is_Walk_from W1.first(),W1.last()
proof
let G1, G2 be _Graph, W1 be Walk of G1, W2 be Walk of G2;
assume A1: W1.vertexSeq() = W2.vertexSeq();
hence len W1 = len W2 by Lm3;
hence W1.length() = W2.length() by Lm2;
thus A2: W1.first() = W1.1 by GLIB_001:def 6
.= W2.1 by A1, Th29, POLYFORM:4
.= W2.first() by GLIB_001:def 6;
thus W1.last() = W1.len W1 by GLIB_001:def 7
.= W1.len W2 by A1, Lm3
.= W2.len W2 by A1, Th29
.= W2.last() by GLIB_001:def 7;
hence thesis by A2, GLIB_001:def 23;
end;
:: into GLIB_001 ?
theorem Th31:
for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
st W1.vertexSeq() = W2.vertexSeq() holds
(W1 is non trivial implies W2 is non trivial) &
(W1 is closed implies W2 is closed)
proof
let G1, G2 be _Graph, W1 be Walk of G1, W2 be Walk of G2;
assume A1: W1.vertexSeq() = W2.vertexSeq();
hereby
assume W1 is non trivial;
then W1.length() <> 0 by GLIB_001:def 26;
then W2.length() <> 0 by A1, Th30;
hence W2 is non trivial by GLIB_001:def 26;
end;
hereby
assume W1 is closed;
then W1.first() = W1.last() by GLIB_001:def 24;
then W1.first() = W2.last() by A1, Th30;
then W2.first() = W2.last() by A1, Th30;
hence W2 is closed by GLIB_001:def 24;
end;
end;
:: into GLIB_001 ?
:: in the case len W1 = 5, W1 could be the Path in a dipole visiting both
:: edges while W2 goes back on the same edge it came from
theorem Th32:
for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
st W1.vertexSeq() = W2.vertexSeq() & len W1 <> 5 holds
(W1 is Path-like implies W2 is Path-like) &
(W1 is Cycle-like implies W2 is Cycle-like)
proof
let G1, G2 be _Graph, W1 be Walk of G1, W2 be Walk of G2;
assume A1: W1.vertexSeq() = W2.vertexSeq();
assume A2: len W1 <> 5;
thus A3: W1 is Path-like implies W2 is Path-like
proof
assume A4: W1 is Path-like;
A5: W2 is Trail-like
proof
assume W2 is non Trail-like;
then consider m1,n1 being even Element of NAT such that
A6: 1 <= m1 & m1 < n1 & n1 <= len W2 & W2.m1 = W2.n1 by GLIB_001:138;
m1 is non zero & n1 is non zero by A6;
then m1-1 is Nat & n1-1 is Nat by CHORD:1;
then reconsider m = m1-1, n = n1-1 as odd Element of NAT
by ORDINAL1:def 12;
A7: W1.n = W2.n & W1.m = W2.m & W1.(n+2) = W2.(n+2) & W1.(m+2) =W2.(m+2)
by A1, Th29;
A8: m < n by A6, XREAL_1:9;
A9: n < len W2 - 0 by A6, XREAL_1:15;
then A10: W2.(n+1) Joins W2.n, W2.(n+2),G2 by GLIB_001:def 3;
A11: m < len W2 by A8, A9, XXREAL_0:2;
then A12: W2.(m+1) Joins W2.m, W2.(m+2),G2 by GLIB_001:def 3;
n+2 <= len W2 by A9, CHORD:4;
then A13: n+2 <= len W1 + 0 by A1, Th30;
per cases by A6, A10, A12, GLIB_000:15;
suppose W2.n = W2.m & W2.(n+2) = W2.(m+2);
then W1.n = W1.m & n <= len W1 by A1, A7, A9, Th30;
then n = len W1 by A4, A8, GLIB_001:def 28;
hence contradiction by A13, XREAL_1:6;
end;
suppose A14: W2.n = W2.(m+2) & W2.(n+2) = W2.m;
then W1.m = W1.(n+2) & m+0 < n+2 by A7, A8, XREAL_1:8;
then A15: m = 1 & n+2 = len W1 by A4, A13, GLIB_001:def 28;
per cases by XXREAL_0:1;
suppose n = m+2;
hence contradiction by A2, A15;
end;
suppose m+2 < n;
then m+2 < n & n <= len W1 by A1, A9, Th30;
hence contradiction by A4, A7, A14, A15, GLIB_001:def 28;
end;
suppose n < m+2;
then n < m+2 & m+2 <= len W2 by A11, CHORD:4;
then n < m+2 & m+2 <= len W1 by A1, Th30;
then n = 1 by A4, A7, A14, GLIB_001:def 28;
hence contradiction by A8, A15;
end;
end;
end;
now
let m,n be odd Element of NAT;
assume A16: m < n & n <= len W2 & W2.m = W2.n;
W1.m = W2.m & W1.n = W2.n & len W1 = len W2 by A1, Th30, Th29;
hence m = 1 & n = len W2 by A4, A16, GLIB_001:def 28;
end;
hence W2 is Path-like by A5, GLIB_001:def 28;
end;
hereby
assume W1 is Cycle-like;
then W2 is closed Path-like non trivial by A1, A3, Th31;
hence W2 is Cycle-like;
end;
end;
:: into GLIB_001 ?
scheme
IndWalk {G() -> _Graph, P[Walk of G()]} : for W being Walk of G() holds P[W]
provided
A1: for W being trivial Walk of G() holds P[W] and
A2: for W being Walk of G(), e being object st e in W.last().edgesInOut() &
P[W] holds P[W.addEdge(e)]
proof
defpred Q[Nat] means for W being Walk of G() st W.length() = $1 holds P[W];
A3: Q[0]
proof
let W be Walk of G();
assume W.length() = 0;
then W is trivial by GLIB_001:def 26;
hence thesis by A1;
end;
A4: for k being Nat st Q[k] holds Q[k+1]
proof
let k be Nat;
assume A5: Q[k];
let W being Walk of G();
assume A6: W.length() = k+1;
then consider L being odd Element of NAT such that
A7: L = len W - 2 & W.cut(1,L).addEdge(W.(L+1)) = W
by GLIB_001:def 26, GLIB_001:133;
set W0 = W.cut(1,L);
A8: L+0 <= len W - 2 + 2 by A7, XREAL_1:6;
then L = len W0 by GLIB_001:45
.= 2*W0.length() + 1 by GLIB_001:112;
then W0.length() = (len W - 2 - 1)/2 by A7
.= (2*W.length() + 1 - 2 - 1)/2 by GLIB_001:112
.= k+1-1 by A6;
then A9: P[W0] by A5;
W.(L+1) in the_Edges_of G() & ((the_Source_of G()).(W.(L+1)) = W0.last() or
(the_Target_of G()).(W.(L+1)) = W0.last())
proof
L + 0 < len W - 2 + 2 by A7, XREAL_1:8;
then A10: W.(L+1) Joins W.L,W.(L+2),G() by GLIB_001:def 3;
A11: L = len W0 by A8, GLIB_001:45;
then A12: W0.L = W0.last() by GLIB_001:def 7;
1 <= L by ABIAN:12;
then L in dom W0 by A11, FINSEQ_3:25;
then W.L = W0.last() by A8, A12, GLIB_001:46;
hence thesis by A10, GLIB_000:def 13;
end;
then W.(L+1) in W0.last().edgesInOut() by GLIB_000:61;
hence thesis by A2, A7, A9;
end;
A13: for k being Nat holds Q[k] from NAT_1:sch 2(A3,A4);
let W be Walk of G();
Q[W.length()] by A13;
hence thesis;
end;
:: into GLIB_001 ?
scheme
IndDWalk {G() -> _Graph, P[Walk of G()]} :
for W being DWalk of G() holds P[W]
provided
A1: for W being trivial DWalk of G() holds P[W] and
A2: for W being DWalk of G(), e being object
st e in W.last().edgesOut() & P[W] holds P[W.addEdge(e)]
proof
defpred Q[Nat] means for W being DWalk of G()
st W.length() = $1 holds P[W];
A3: Q[0]
proof
let W be DWalk of G();
assume W.length() = 0;
then W is trivial by GLIB_001:def 26;
hence thesis by A1;
end;
A4: for k being Nat st Q[k] holds Q[k+1]
proof
let k be Nat;
assume A5: Q[k];
let W be DWalk of G();
assume A6: W.length() = k+1;
then consider L being odd Element of NAT such that
A7: L = len W - 2 & W.cut(1,L).addEdge(W.(L+1)) = W
by GLIB_001:def 26, GLIB_001:133;
set W0 = W.cut(1,L);
A8: L+0 <= len W - 2 + 2 by A7, XREAL_1:6;
then L = len W0 by GLIB_001:45
.= 2*W0.length() + 1 by GLIB_001:112;
then W0.length() = (len W - 2 - 1)/2 by A7
.= (2*W.length() + 1 - 2 - 1)/2 by GLIB_001:112
.= k+1-1 by A6;
then A9: P[W0] by A5;
W.(L+1) in the_Edges_of G() & (the_Source_of G()).(W.(L+1)) = W0.last()
proof
A10: L + 0 < len W - 2 + 2 by A7, XREAL_1:8;
then W.(L+1) Joins W.L,W.(L+2),G() by GLIB_001:def 3;
hence W.(L+1) in the_Edges_of G() by GLIB_000:def 13;
A11: L = len W0 by A8, GLIB_001:45;
then A12: W0.L = W0.last() by GLIB_001:def 7;
1 <= L by ABIAN:12;
then L in dom W0 by A11, FINSEQ_3:25;
then W.L = W0.last() by A8, A12, GLIB_001:46;
hence thesis by A10, GLIB_001:def 25;
end;
then W.(L+1) in W0.last().edgesOut() by GLIB_000:58;
hence thesis by A2, A7, A9;
end;
A13: for k being Nat holds Q[k] from NAT_1:sch 2(A3,A4);
let W be DWalk of G();
Q[W.length()] by A13;
hence thesis;
end;
:: into GLIB_002 ?
theorem Th33:
for G1 being _Graph, E being Subset of the_Edges_of G1
for G2 being inducedSubgraph of G1, the_Vertices_of G1, E
st G2 is connected holds G1 is connected
proof
let G1 be _Graph, E be Subset of the_Edges_of G1;
let G2 be inducedSubgraph of G1, the_Vertices_of G1, E;
assume A1: G2 is connected;
now
let v1,w1 be Vertex of G1;
E c= the_Edges_of G1;
then E c= G1.edgesBetween(the_Vertices_of G1) &
the_Vertices_of G1 c= the_Vertices_of G1 by GLIB_000:34;
then reconsider v2 = v1, w2 = w1 as Vertex of G2 by GLIB_000:def 37;
consider W2 being Walk of G2 such that
A2: W2 is_Walk_from v2,w2 by A1, GLIB_002:def 1;
reconsider W1 = W2 as Walk of G1 by GLIB_001:167;
take W1;
thus W1 is_Walk_from v1,w1 by A2, GLIB_001:19;
end;
hence thesis by GLIB_002:def 1;
end;
:: into GLIB_002 ?
theorem
for G1 being _Graph, E being set, G2 being removeEdges of G1, E
st G2 is connected holds G1 is connected by Th33;
:: into GLIB_002 ?
registration
let G1 be non connected _Graph, E be set;
cluster -> non connected for removeEdges of G1, E;
coherence by Th33;
end;
:: into GLIB_002 ?
theorem Th35:
for G1 being _Graph, G2 being Subgraph of G1
st (for W1 being Walk of G1 ex W2 being Walk of G2
st W2 is_Walk_from W1.first(),W1.last())
holds
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2)
proof
let G1 be _Graph, G2 be Subgraph of G1;
assume A1: for W1 being Walk of G1 ex W2 being Walk of G2
st W2 is_Walk_from W1.first(),W1.last();
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A2: v1 = v2;
for w being object holds
w in G1.reachableFrom(v1) implies w in G2.reachableFrom(v2)
proof
let w be object;
assume w in G1.reachableFrom(v1);
then consider W1 being Walk of G1 such that
A3: W1 is_Walk_from v1,w by GLIB_002:def 5;
W1.first() = v1 & W1.last() = w by A3, GLIB_001:def 23;
then consider W2 being Walk of G2 such that
A4: W2 is_Walk_from v1,w by A1;
thus thesis by A2, A4, GLIB_002:def 5;
end;
then A5: G1.reachableFrom(v1) c= G2.reachableFrom(v2) by TARSKI:def 3;
G2.reachableFrom(v2) c= G1.reachableFrom(v1) by A2, GLIB_002:14;
hence thesis by A5, XBOOLE_0:def 10;
end;
:: into GLIB_002 ?
theorem Th36:
for G1 being _Graph, G2 being Subgraph of G1
st (for W1 being Walk of G1 ex W2 being Walk of G2
st W2 is_Walk_from W1.first(),W1.last())
holds G1 is connected implies G2 is connected
proof
let G1 be _Graph, G2 be Subgraph of G1;
assume A1: for W1 being Walk of G1 ex W2 being Walk of G2
st W2 is_Walk_from W1.first(),W1.last();
assume A2: G1 is connected;
now
let v2,w2 be Vertex of G2;
the_Vertices_of G2 c= the_Vertices_of G1;
then reconsider v1=v2, w1=w2 as Vertex of G1 by TARSKI:def 3;
consider W1 being Walk of G1 such that
A3: W1 is_Walk_from v1,w1 by A2, GLIB_002:def 1;
W1.first() = v1 & W1.last() = w1 by A3, GLIB_001:def 23;
then consider W2 being Walk of G2 such that
A4: W2 is_Walk_from v1,w1 by A1;
take W2;
thus W2 is_Walk_from v2,w2 by A4;
end;
hence thesis by GLIB_002:def 1;
end;
:: into GLIB_002 ?
theorem Th37:
for G1 being _Graph, G2 being spanning Subgraph of G1
st (for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2))
holds G1.componentSet() = G2.componentSet()
proof
let G1 be _Graph, G2 be spanning Subgraph of G1;
assume A1: for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2);
for C being object holds C in G1.componentSet() iff C in G2.componentSet()
proof
let C be object;
hereby
assume C in G1.componentSet();
then consider v1 being Vertex of G1 such that
A2: C = G1.reachableFrom(v1) by GLIB_002:def 8;
reconsider v2 = v1 as Vertex of G2 by GLIB_000:def 33;
C = G2.reachableFrom(v2) by A1, A2;
hence C in G2.componentSet() by GLIB_002:def 8;
end;
assume C in G2.componentSet();
then consider v2 being Vertex of G2 such that
A3: C = G2.reachableFrom(v2) by GLIB_002:def 8;
reconsider v1 = v2 as Vertex of G1 by GLIB_000:def 33;
C = G1.reachableFrom(v1) by A1, A3;
hence C in G1.componentSet() by GLIB_002:def 8;
end;
hence thesis by TARSKI:2;
end;
:: into GLIB_002 ?
theorem Th38:
for G1 being _Graph, G2 being spanning Subgraph of G1
st (for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2))
holds G1.numComponents() = G2.numComponents()
proof
let G1 be _Graph, G2 be spanning Subgraph of G1;
assume A1: for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2);
thus G1.numComponents() = card G1.componentSet() by GLIB_002:def 9
.= card G2.componentSet() by A1, Th37
.= G2.numComponents() by GLIB_002:def 9;
end;
:: into CHORD ?
theorem
for G being _Graph holds G is loopless iff
for v being Vertex of G holds not v,v are_adjacent
proof
let G be _Graph;
hereby
assume A1: G is loopless;
let v be Vertex of G;
assume v,v are_adjacent;
then ex e being object st e Joins v,v,G by CHORD:def 3;
hence contradiction by A1, GLIB_000:18;
end;
assume A2: for v being Vertex of G holds not v,v are_adjacent;
now
let v be object;
given e being object such that
A3: e Joins v,v,G;
reconsider v0 = v as Vertex of G by A3, GLIB_000:13;
v0,v0 are_adjacent by A3, CHORD:def 3;
hence contradiction by A2;
end;
hence thesis by GLIB_000:18;
end;
registration
let G be non complete _Graph;
cluster spanning -> non complete for Subgraph of G;
coherence
proof
let G2 be Subgraph of G;
assume A1: G2 is spanning;
assume A2: G2 is complete;
now
let v1,w1 be Vertex of G;
assume A3: v1 <> w1;
reconsider v2 = v1, w2 = w1 as Vertex of G2 by A1, GLIB_000:def 33;
consider e being object such that
A4: e Joins v2,w2,G2 by A2, A3, CHORD:def 6, CHORD:def 3;
thus v1,w1 are_adjacent by A4, GLIB_000:72, CHORD:def 3;
end;
hence contradiction by CHORD:def 6;
end;
end;
:: into GLIB_006 ?
theorem Th40:
for G2, G3 being _Graph, G1 being Supergraph of G3
st G1 == G2 holds G2 is Supergraph of G3
proof
let G2, G3 be _Graph, G1 be Supergraph of G3;
assume G1 == G2;
then A1: the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 &
the_Source_of G1 = the_Source_of G2 &
the_Target_of G1 = the_Target_of G2 by GLIB_000:def 34;
the_Vertices_of G3 c= the_Vertices_of G1 &
the_Edges_of G3 c= the_Edges_of G1 &
for e being set st e in the_Edges_of G3 holds
(the_Source_of G3).e = (the_Source_of G1).e &
(the_Target_of G3).e = (the_Target_of G1).e by GLIB_006:def 9;
hence thesis by A1, GLIB_006:def 9;
end;
theorem Th41:
for G2 being _Graph, V being set, G1 being addVertices of G2, V
for x,y being set, e being object holds
(e Joins x,y,G1 iff e Joins x,y,G2) &
(e DJoins x,y,G1 iff e DJoins x,y,G2) &
(e SJoins x,y,G1 iff e SJoins x,y,G2) &
(e DSJoins x,y,G1 iff e DSJoins x,y,G2)
proof
let G2 be _Graph, V be set, G1 be addVertices of G2, V;
let x,y be set, e be object;
set v1 = (the_Source_of G1).e, w1 = (the_Target_of G1).e;
set v2 = (the_Source_of G2).e, w2 = (the_Target_of G2).e;
hereby
assume e Joins x,y,G1;
then e in the_Edges_of G1 & (v1 = x & w1 = y or v1 = y & w1 = x)
by GLIB_000:def 13;
then A1: e in the_Edges_of G2 & (v1 = x & w1 = y or v1 = y & w1 = x)
by GLIB_006:def 10;
then v1 = v2 & w1 = w2 by GLIB_006:def 9;
hence e Joins x,y,G2 by A1, GLIB_000:def 13;
end;
thus e Joins x,y,G2 implies e Joins x,y,G1 by GLIB_006:70;
hereby
assume e DJoins x,y,G1;
then e in the_Edges_of G1 & v1 = x & w1 = y by GLIB_000:def 14;
then A2: e in the_Edges_of G2 & v1 = x & w1 = y by GLIB_006:def 10;
then v1 = v2 & w1 = w2 by GLIB_006:def 9;
hence e DJoins x,y,G2 by A2, GLIB_000:def 14;
end;
thus e DJoins x,y,G2 implies e DJoins x,y,G1 by GLIB_006:70;
hereby
assume e SJoins x,y,G1;
then e in the_Edges_of G1 & (v1 in x & w1 in y or v1 in y & w1 in x)
by GLIB_000:def 15;
then A3: e in the_Edges_of G2 & (v1 in x & w1 in y or v1 in y & w1 in x)
by GLIB_006:def 10;
then v1 = v2 & w1 = w2 by GLIB_006:def 9;
hence e SJoins x,y,G2 by A3, GLIB_000:def 15;
end;
thus e SJoins x,y,G2 implies e SJoins x,y,G1 by GLIB_006:70;
hereby
assume e DSJoins x,y,G1;
then e in the_Edges_of G1 & v1 in x & w1 in y by GLIB_000:def 16;
then A4: e in the_Edges_of G2 & v1 in x & w1 in y by GLIB_006:def 10;
then v1 = v2 & w1 = w2 by GLIB_006:def 9;
hence e DSJoins x,y,G2 by A4, GLIB_000:def 16;
end;
thus e DSJoins x,y,G2 implies e DSJoins x,y,G1 by GLIB_006:70;
end;
:: into GLIB_007 ?
theorem Th42:
for G1, G2 being _Graph st G1 == G2
holds G2 is reverseEdgeDirections of G1, {}
proof
let G1, G2 be _Graph;
assume A1: G1 == G2;
A2: {} c= the_Edges_of G1 by XBOOLE_1:2;
A3: the_Source_of G2 = the_Source_of G1 by A1, GLIB_000:def 34
.= the_Source_of G1 +* ((the_Target_of G1) | {}) by FUNCT_4:21;
A4: the_Target_of G2 = the_Target_of G1 by A1, GLIB_000:def 34
.= the_Target_of G1 +* ((the_Source_of G1) | {}) by FUNCT_4:21;
the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2
by A1, GLIB_000:def 34;
hence thesis by A2, A3, A4, GLIB_007:def 1;
end;
:: into GLIB_007 ?
theorem
for G being _Graph holds G is reverseEdgeDirections of G, {} by Th42;
begin :: Plain Graphs
definition
let G be _Graph;
attr G is plain means
:Def1:
dom G = _GraphSelectors;
end;
registration
let G be _Graph;
cluster G|(_GraphSelectors) -> plain;
coherence
proof
_GraphSelectors c= dom G by GLIB_000:2;
hence thesis by RELAT_1:62;
end;
end;
registration
let V be non empty set, E be set, S, T be Function of E, V;
cluster createGraph(V,E,S,T) -> plain;
coherence
proof
thus dom createGraph(V,E,S,T) = dom <* V, E, S, T *> by GLIB_000:def 11
.= Seg len <* V, E, S, T *> by FINSEQ_1:def 3
.= _GraphSelectors by GLIB_000:1, def 5, FINSEQ_3:2, FINSEQ_4:76;
end;
end;
registration
let G be _Graph, X be set;
cluster G.set(WeightSelector, X) -> non plain;
coherence
proof
A1: dom G.set(WeightSelector,X) = dom G \/ {WeightSelector} by GLIB_000:7;
WeightSelector in {WeightSelector} by TARSKI:def 1;
then WeightSelector in dom G.set(WeightSelector,X)
by A1, XBOOLE_0:def 3;
hence thesis by GLIB_000:def 5, GLIB_000:1, GLIB_003:def 1, ENUMSET1:def 2;
end;
cluster G.set(ELabelSelector, X) -> non plain;
coherence
proof
A2: dom G.set(ELabelSelector,X) = dom G \/ {ELabelSelector} by GLIB_000:7;
ELabelSelector in {ELabelSelector} by TARSKI:def 1;
then ELabelSelector in dom G.set(ELabelSelector,X)
by A2, XBOOLE_0:def 3;
hence thesis by GLIB_000:def 5, GLIB_000:1, GLIB_003:def 2, ENUMSET1:def 2;
end;
cluster G.set(VLabelSelector, X) -> non plain;
coherence
proof
A3: dom G.set(VLabelSelector,X) = dom G \/ {VLabelSelector} by GLIB_000:7;
VLabelSelector in {VLabelSelector} by TARSKI:def 1;
then VLabelSelector in dom G.set(VLabelSelector,X)
by A3, XBOOLE_0:def 3;
hence thesis by GLIB_000:def 5, GLIB_000:1, GLIB_003:def 3, ENUMSET1:def 2;
end;
end;
registration
cluster plain for _Graph;
existence
proof
set G = (the _Graph)|(_GraphSelectors);
take G;
thus thesis;
end;
end;
theorem
for G1, G2 being plain _Graph st G1 == G2 holds G1 = G2
proof
let G1, G2 be plain _Graph;
dom G1 = _GraphSelectors by Def1;
then A1: dom G1 = dom G2 by Def1;
assume A2: G1 == G2;
for x being object st x in dom G1 holds G1.x = G2.x
proof
let x be object;
assume x in dom G1;
then x in _GraphSelectors by Def1;
then per cases by ENUMSET1:def 2, GLIB_000:def 5;
suppose A3: x = VertexSelector;
hence G1.x = the_Vertices_of G1 by GLIB_000:def 6
.= the_Vertices_of G2 by A2, GLIB_000:def 34
.= G2.x by A3, GLIB_000:def 6;
end;
suppose A4: x = EdgeSelector;
hence G1.x = the_Edges_of G1 by GLIB_000:def 7
.= the_Edges_of G2 by A2, GLIB_000:def 34
.= G2.x by A4, GLIB_000:def 7;
end;
suppose A5: x = SourceSelector;
thus G1.x = the_Source_of G1 by A5, GLIB_000:def 8
.= the_Source_of G2 by A2, GLIB_000:def 34
.= G2.x by A5, GLIB_000:def 8;
end;
suppose A6: x = TargetSelector;
hence G1.x = the_Target_of G1 by GLIB_000:def 9
.= the_Target_of G2 by A2, GLIB_000:def 34
.= G2.x by A6, GLIB_000:def 9;
end;
end;
hence thesis by A1, FUNCT_1:2;
end;
:: existence clusters for plain graph modes
registration
let G be _Graph;
cluster plain for Subgraph of G;
existence
proof
set G2 = the Subgraph of G;
set G3 = G2 | _GraphSelectors;
reconsider G3 as Subgraph of G by GLIB_000:128, GLIB_000:92;
take G3;
thus thesis;
end;
let V be set;
cluster plain for removeVertices of G, V;
existence
proof
set G2 = the removeVertices of G, V;
set G3 = G2 | _GraphSelectors;
take G3;
thus thesis by GLIB_000:128, GLIB_000:101;
end;
let E be set;
cluster plain for inducedSubgraph of G, V, E;
existence
proof
set G2 = the inducedSubgraph of G, V, E;
set G3 = G2 | _GraphSelectors;
take G3;
thus thesis by GLIB_000:128, GLIB_000:101;
end;
end;
registration
let G be _Graph, E be set;
cluster plain for removeEdges of G, E;
existence
proof
set G2 = the removeEdges of G, E;
set G3 = G2 | _GraphSelectors;
take G3;
thus thesis by GLIB_000:128, GLIB_000:101;
end;
cluster plain for reverseEdgeDirections of G, E;
existence
proof
set G2 = the reverseEdgeDirections of G, E;
set G3 = G2 | _GraphSelectors;
take G3;
thus thesis by GLIB_000:128, GLIB_007:2;
end;
end;
registration
let G be _Graph, v be set;
cluster plain for removeVertex of G, v;
existence
proof
set G2 = the removeVertex of G, v;
set G3 = G2 | _GraphSelectors;
take G3;
thus thesis by GLIB_000:128, GLIB_000:101;
end;
end;
registration
let G be _Graph, e be set;
cluster plain for removeEdge of G, e;
existence
proof
set G2 = the removeEdge of G, e;
set G3 = G2 | _GraphSelectors;
take G3;
thus thesis by GLIB_000:128, GLIB_000:101;
end;
end;
registration
let G be _Graph;
cluster plain for Supergraph of G;
existence
proof
set G2 = the Supergraph of G;
set G3 = G2 | _GraphSelectors;
take G3;
thus thesis by Th40, GLIB_000:128;
end;
let V be set;
cluster plain for addVertices of G, V;
existence
proof
set G2 = the addVertices of G, V;
set G3 = G2 | _GraphSelectors;
take G3;
thus thesis by GLIB_000:128, GLIB_006:80;
end;
end;
registration
let G be _Graph, v, e, w be object;
cluster plain for addEdge of G, v, e, w;
existence
proof
set G2 = the addEdge of G,v,e,w;
set G3 = G2 | _GraphSelectors;
take G3;
thus thesis by GLIB_000:128, GLIB_006:101;
end;
cluster plain for addAdjVertex of G, v, e, w;
existence
proof
set G2 = the addAdjVertex of G,v,e,w;
set G3 = G2 | _GraphSelectors;
take G3;
thus thesis by GLIB_000:128, GLIB_006:124;
end;
end;
registration
let G be _Graph, v be object, V be set;
cluster plain for addAdjVertexFromAll of G, v, V;
existence
proof
set G2 = the addAdjVertexFromAll of G,v,V;
set G3 = G2 | _GraphSelectors;
reconsider G3 as addAdjVertexFromAll of G,v,V by GLIB_000:128, GLIB_007:31;
take G3;
thus thesis;
end;
cluster plain for addAdjVertexToAll of G, v, V;
existence
proof
set G2 = the addAdjVertexToAll of G,v,V;
set G3 = G2 | _GraphSelectors;
reconsider G3 as addAdjVertexToAll of G,v,V by GLIB_000:128, GLIB_007:30;
take G3;
thus thesis;
end;
cluster plain for addAdjVertexAll of G, v, V;
existence
proof
set G2 = the addAdjVertexAll of G,v,V;
set G3 = G2 | _GraphSelectors;
take G3;
thus thesis by GLIB_000:128, GLIB_007:48;
end;
end;
begin :: Graphs with Loops removed
definition
let G be _Graph;
func G.loops() -> Subset of the_Edges_of G means
:Def2:
for e being object holds e in it iff ex v being object st e Joins v,v,G;
existence
proof
defpred P[object] means ex v being object st $1 Joins v,v,G;
consider L being Subset of the_Edges_of G such that
A1: for e being set holds e in L iff e in the_Edges_of G & P[e]
from SUBSET_1:sch 1;
take L;
let e be object;
thus e in L implies ex v being object st e Joins v,v,G by A1;
given v being object such that
A2: e Joins v,v,G;
e in the_Edges_of G by A2, GLIB_000:def 13;
hence thesis by A1, A2;
end;
uniqueness
proof
let L1, L2 be Subset of the_Edges_of G;
assume that
A3: for e being object holds
e in L1 iff ex v being object st e Joins v,v,G and
A4: for e being object holds
e in L2 iff ex v being object st e Joins v,v,G;
for e being object holds e in L1 iff e in L2
proof
let e be object;
hereby
assume e in L1;
then ex v being object st e Joins v,v,G by A3;
hence e in L2 by A4;
end;
assume e in L2;
then ex v being object st e Joins v,v,G by A4;
hence e in L1 by A3;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th45:
for G being _Graph, e being object
holds e in G.loops() iff ex v being object st e DJoins v,v,G
proof
let G be _Graph, e be object;
hereby
assume e in G.loops();
then consider v being object such that
A1: e Joins v,v,G by Def2;
take v;
thus e DJoins v,v,G by A1, GLIB_000:16;
end;
given v being object such that
A2: e DJoins v,v,G;
e Joins v,v,G by A2, GLIB_000:16;
hence thesis by Def2;
end;
theorem Th46:
for G being _Graph, e,v,w being object st e Joins v,w,G & v <> w
holds not e in G.loops()
proof
let G be _Graph, e,v,w be object;
assume A1: e Joins v,w,G & v <> w;
assume e in G.loops();
then consider u being object such that
A2: e Joins u,u,G by Def2;
u = v & u = w by A1, A2, GLIB_000:15;
hence contradiction by A1;
end;
theorem Th47:
for G being _Graph holds G is loopless iff G.loops() = {}
proof
let G be _Graph;
now
assume G.loops() <> {};
then consider e being object such that
A1: e in G.loops() by XBOOLE_0:def 1;
consider v being object such that
A2: e Joins v,v,G by A1, Def2;
thus G is non loopless by A2, GLIB_000:18;
end;
hence G is loopless implies G.loops() = {};
now
assume G is non loopless;
then consider v being object such that
A3: ex e being object st e Joins v,v,G by GLIB_000:18;
consider e being object such that
A4: e Joins v,v,G by A3;
thus G.loops() <> {} by A4, Def2;
end;
hence thesis;
end;
registration
let G be loopless _Graph;
cluster G.loops() -> empty;
coherence by Th47;
end;
registration
let G be non loopless _Graph;
cluster G.loops() -> non empty;
coherence by Th47;
end;
theorem Th48:
for G1 being _Graph, G2 being Subgraph of G1 holds G2.loops() c= G1.loops()
proof
let G1 be _Graph, G2 be Subgraph of G1;
now
let e be object;
assume e in G2.loops();
then consider v being object such that
A1: e DJoins v,v,G2 by Th45;
e is set & v is set by TARSKI:1;
hence e in G1.loops() by A1, Th45, GLIB_000:72;
end;
hence thesis by TARSKI:def 3;
end;
theorem Th49:
for G2 being _Graph, G1 being Supergraph of G2 holds G2.loops() c= G1.loops()
proof
let G2 be _Graph, G1 be Supergraph of G2;
G2 is Subgraph of G1 by GLIB_006:57;
hence thesis by Th48;
end;
theorem Th50:
for G1, G2 being _Graph st G1 == G2 holds G1.loops() = G2.loops()
proof
let G1, G2 be _Graph;
assume G1 == G2;
then G1 is Subgraph of G2 & G2 is Subgraph of G1 by GLIB_000:87;
then G1.loops() c= G2.loops() & G2.loops() c= G1.loops() by Th48;
hence thesis by XBOOLE_0:def 10;
end;
theorem
for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
holds G1.loops() = G2.loops()
proof
let G1 be _Graph, E be set, G2 be reverseEdgeDirections of G1, E;
now
let e be object;
hereby
assume e in G1.loops();
then consider v being object such that
A1: e Joins v,v,G1 by Def2;
e Joins v,v,G2 by A1, GLIB_007:9;
hence e in G2.loops() by Def2;
end;
assume e in G2.loops();
then consider v being object such that
A2: e Joins v,v,G2 by Def2;
e Joins v,v,G1 by A2, GLIB_007:9;
hence e in G1.loops() by Def2;
end;
hence thesis by TARSKI:2;
end;
theorem
for G2 being _Graph, V being set, G1 being addVertices of G2, V
holds G1.loops() = G2.loops()
proof
let G2 be _Graph, V be set, G1 be addVertices of G2, V;
now
let e be object;
assume e in G1.loops();
then consider v being object such that
A1: e Joins v,v,G1 by Def2;
v is set by TARSKI:1;
then e Joins v,v,G2 by A1, Th41;
hence e in G2.loops() by Def2;
end;
then A2: G1.loops() c= G2.loops() by TARSKI:def 3;
G2.loops() c= G1.loops() by Th49;
hence thesis by A2, XBOOLE_0:def 10;
end;
theorem
for G2 being _Graph, v1,e,v2 being object, G1 being addEdge of G2,v1,e,v2
st v1 <> v2 holds G1.loops() = G2.loops()
proof
let G2 be _Graph, v1,e,v2 be object, G1 be addEdge of G2,v1,e,v2;
assume A1: v1 <> v2;
per cases;
suppose not v1 in the_Vertices_of G2 or not v2 in the_Vertices_of G2 or
e in the_Edges_of G2;
then G1 == G2 by GLIB_006:def 11;
hence thesis by Th50;
end;
suppose A2: v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 &
not e in the_Edges_of G2;
A3: G2.loops() c= G1.loops() by Th49;
now
let e0 be object;
assume e0 in G1.loops();
then consider w being object such that
A4: e0 Joins w,w,G1 by Def2;
e0 in the_Edges_of G2
proof
assume not e0 in the_Edges_of G2;
then v1 = w & v2 = w by A2, A4, GLIB_006:107;
hence contradiction by A1;
end;
then e0 Joins w,w,G2 by A4, GLIB_006:72;
hence e0 in G2.loops() by Def2;
end;
then G1.loops() c= G2.loops() by TARSKI:def 3;
hence thesis by A3, XBOOLE_0:def 10;
end;
end;
theorem
for G2 being _Graph, v being Vertex of G2, e being object
for G1 being addEdge of G2,v,e,v st not e in the_Edges_of G2
holds G1.loops() = G2.loops() \/ {e}
proof
let G2 be _Graph, v be Vertex of G2, e be object;
let G1 be addEdge of G2,v,e,v;
assume A1: not e in the_Edges_of G2;
then e in G1.loops() by Th45, GLIB_006:105;
then A2: {e} c= G1.loops() by ZFMISC_1:31;
G2.loops() c= G1.loops() by Th49;
then A3: G2.loops() \/ {e} c= G1.loops() by A2, XBOOLE_1:8;
now
let e0 be object;
assume e0 in G1.loops();
then consider w being object such that
A4: e0 Joins w,w,G1 by Def2;
per cases;
suppose e0 in the_Edges_of G2;
then e0 Joins w,w,G2 by A4, GLIB_006:72;
then e0 in G2.loops() by Def2;
hence e0 in G2.loops() \/ {e} by XBOOLE_0:def 3;
end;
suppose not e0 in the_Edges_of G2;
then e = e0 by A1, A4, GLIB_006:106;
then e0 in {e} by TARSKI:def 1;
hence e0 in G2.loops() \/ {e} by XBOOLE_0:def 3;
end;
end;
then G1.loops() c= G2.loops() \/ {e} by TARSKI:def 3;
hence thesis by A3, XBOOLE_0:def 10;
end;
theorem
for G2 being _Graph, v1,e,v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 holds G1.loops() = G2.loops()
proof
let G2 be _Graph, v1,e,v2 be object;
let G1 be addAdjVertex of G2,v1,e,v2;
A1: G2.loops() c= G1.loops() by Th49;
per cases;
suppose A2: v1 in the_Vertices_of G2 & not v2 in the_Vertices_of G2 &
not e in the_Edges_of G2;
now
let e0 be object;
assume e0 in G1.loops();
then consider w being object such that
A3: e0 Joins w,w,G1 by Def2;
e0 in the_Edges_of G2
proof
assume A4: not e0 in the_Edges_of G2;
A5: e0 in the_Edges_of G1 by A3, GLIB_000:def 13;
the_Edges_of G1 = the_Edges_of G2 \/ {e} by A2, GLIB_006:def 12;
then e0 in {e} by A4, A5, XBOOLE_0:def 3;
then e = e0 by TARSKI:def 1;
then e0 Joins v1,v2,G1 by A2, GLIB_006:131;
then v1 = w & v2 = w by A3, GLIB_000:15;
hence contradiction by A2;
end;
then e0 Joins w,w,G2 by A3, GLIB_006:72;
hence e0 in G2.loops() by Def2;
end;
then G1.loops() c= G2.loops() by TARSKI:def 3;
hence thesis by A1, XBOOLE_0:def 10;
end;
suppose A6: not v1 in the_Vertices_of G2 & v2 in the_Vertices_of G2 &
not e in the_Edges_of G2;
now
let e0 be object;
assume e0 in G1.loops();
then consider w being object such that
A7: e0 Joins w,w,G1 by Def2;
e0 in the_Edges_of G2
proof
assume A8: not e0 in the_Edges_of G2;
A9: e0 in the_Edges_of G1 by A7, GLIB_000:def 13;
the_Edges_of G1 = the_Edges_of G2 \/ {e} by A6, GLIB_006:def 12;
then e0 in {e} by A8, A9, XBOOLE_0:def 3;
then e = e0 by TARSKI:def 1;
then e0 Joins v1,v2,G1 by A6, GLIB_006:132;
then v1 = w & v2 = w by A7, GLIB_000:15;
hence contradiction by A6;
end;
then e0 Joins w,w,G2 by A7, GLIB_006:72;
hence e0 in G2.loops() by Def2;
end;
then G1.loops() c= G2.loops() by TARSKI:def 3;
hence thesis by A1, XBOOLE_0:def 10;
end;
suppose not (v1 in the_Vertices_of G2 & not v2 in the_Vertices_of G2 &
not e in the_Edges_of G2) & not (not v1 in the_Vertices_of G2 &
v2 in the_Vertices_of G2 & not e in the_Edges_of G2);
then G1 == G2 by GLIB_006:def 12;
hence thesis by Th50;
end;
end;
theorem
for G2 being _Graph, v being object, V being set
for G1 being addAdjVertexAll of G2,v,V holds G1.loops() = G2.loops()
proof
let G2 be _Graph, v be object, V be set;
let G1 be addAdjVertexAll of G2,v,V;
per cases;
suppose A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
A2: G2.loops() c= G1.loops() by Th49;
now
let e be object;
assume e in G1.loops();
then consider w being object such that
A3: e Joins w,w,G1 by Def2;
v <> w by A1, A3, GLIB_007:def 4;
then e Joins w,w,G2 by A1, A3, GLIB_007:49;
hence e in G2.loops() by Def2;
end;
then G1.loops() c= G2.loops() by TARSKI:def 3;
hence thesis by A2, XBOOLE_0:def 10;
end;
suppose not (V c= the_Vertices_of G2 & not v in the_Vertices_of G2);
then G1 == G2 by GLIB_007:def 4;
hence thesis by Th50;
end;
end;
theorem Th57:
for G being _Graph, P being Path of G holds P.edges() misses G.loops() or
ex v,e being object st e Joins v,v,G & P = G.walkOf(v,e,v)
proof
let G be _Graph, P be Path of G;
assume P.edges() meets G.loops();
then P.edges() /\ G.loops() <> {} by XBOOLE_0:def 7;
then consider e being object such that
A1: e in P.edges() /\ G.loops() by XBOOLE_0:def 1;
A2: e in P.edges() & e in G.loops() by A1, XBOOLE_0:def 4;
then consider v being object such that
A3: e Joins v,v,G by Def2;
consider v1,v2 being Vertex of G, n being odd Element of NAT such that
A4: n+2 <= len P & v1 = P.n & e = P.(n+1) & v2 = P.(n+2) and
A5: e Joins v1,v2,G by A2, GLIB_001:103;
A6: v = v1 & v = v2 by A3, A5, GLIB_000:15;
then A7: P.n = P.(n+2) by A4;
n+0 < n+2 by XREAL_1:8;
then A8: n = 1 & n+2 = len P by A4, A7, GLIB_001:def 28;
then A9: P.1 = v & P.len P = v by A4, A6;
take v,e;
thus e Joins v,v,G by A3;
then G.walkOf(v,e,v) = <* v,e,v *> by GLIB_001:def 5;
hence thesis by A4, A8, A9, FINSEQ_1:45;
end;
definition
let G be _Graph;
mode removeLoops of G is removeEdges of G, G.loops();
end;
theorem Th58:
for G1 being loopless _Graph, G2 being _Graph
holds G1 == G2 iff G2 is removeLoops of G1
proof
let G1 be loopless _Graph, G2 be _Graph;
hereby
assume A1: G1 == G2;
G1 is inducedSubgraph of G1, the_Vertices_of G1 by GLIB_000:100;
then G1 is inducedSubgraph of G1, the_Vertices_of G1, the_Edges_of G1
by GLIB_000:34;
hence G2 is removeLoops of G1 by A1, GLIB_000:101;
end;
assume G2 is removeLoops of G1;
then G2 is inducedSubgraph of G1, the_Vertices_of G1 by GLIB_000:34;
hence G1 == G2 by GLIB_000:94;
end;
theorem Th59:
for G1, G2 being _Graph, G3 being removeLoops of G1
holds G2 == G3 iff G2 is removeLoops of G1 by GLIB_000:101, GLIB_000:93;
theorem Th60:
for G1, G2 being _Graph, G3 being removeLoops of G1
st G1 == G2 holds G3 is removeLoops of G2
proof
let G1, G2 be _Graph, G3 be removeLoops of G1;
assume A1: G1 == G2;
then the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 & G1.loops() = G2.loops()
by Th50, GLIB_000:def 34;
hence thesis by A1, GLIB_000:95;
end;
registration
let G be _Graph;
cluster -> loopless for removeLoops of G;
coherence
proof
let G2 be removeLoops of G;
assume G2 is non loopless;
then consider v being object such that
A1: ex e being object st e Joins v,v,G2 by GLIB_000:18;
consider e being object such that
A2: e Joins v,v,G2 by A1;
v is set by TARSKI:1;
then e Joins v,v,G by A2, GLIB_000:72;
then e in G.loops() by Def2;
then not e in the_Edges_of G \ G.loops() by XBOOLE_0:def 5;
then not e in the_Edges_of G2 by GLIB_000:53;
hence contradiction by A2, GLIB_000:def 13;
end;
cluster plain for removeLoops of G;
existence
proof
take the plain removeEdges of G, G.loops();
thus thesis;
end;
end;
registration
let G be non-multi _Graph;
cluster -> simple for removeLoops of G;
coherence;
end;
registration
let G be non-Dmulti _Graph;
cluster -> Dsimple for removeLoops of G;
coherence;
end;
registration
let G be complete _Graph;
cluster -> complete for removeLoops of G;
coherence
proof
let G2 be removeLoops of G;
A1: the_Vertices_of G2 = the_Vertices_of G &
the_Edges_of G2 = the_Edges_of G \ G.loops() by GLIB_000:53;
now
let v2,w2 be Vertex of G2;
assume A2: v2 <> w2;
reconsider v1 = v2, w1 = w2 as Vertex of G by GLIB_000:53;
consider e being object such that
A3: e Joins v1,w1,G by A2, CHORD:def 6, CHORD:def 3;
A4: not e in G.loops() by A2, A3, Th46;
e in the_Edges_of G by A3, GLIB_000:def 13;
then e in the_Edges_of G2 by A1, A4, XBOOLE_0:def 5;
then e Joins v2,w2,G2 by A3, GLIB_000:73;
hence v2,w2 are_adjacent by CHORD:def 3;
end;
hence thesis by CHORD:def 6;
end;
end;
theorem Th61:
for G1 being _Graph, G2 being removeLoops of G1, W1 being Walk of G1
ex W2 being Walk of G2 st W2 is_Walk_from W1.first(),W1.last()
proof
let G1 be _Graph, G2 be removeLoops of G1;
let W1 be Walk of G1;
A1: W1 is_Walk_from W1.first(), W1.last() by GLIB_001:def 23;
set P = the Path of W1, v = W1.first(), w = W1.last();
A2: P is_Walk_from v,w by A1, GLIB_001:160;
per cases;
suppose P.edges() /\ G1.loops() = {};
then P.edges() c= the_Edges_of G1 \ G1.loops()
by XBOOLE_0:def 7, XBOOLE_1:86;
then A3: P.edges() c= the_Edges_of G2 by GLIB_000:53;
the_Vertices_of G1 = the_Vertices_of G2 by GLIB_000:53;
then P.vertices() c= the_Vertices_of G2;
then reconsider W2 = P as Walk of G2 by A3, GLIB_001:170;
take W2;
thus thesis by A2, GLIB_001:19;
end;
suppose P.edges() /\ G1.loops() <> {};
then consider v0,e being object such that
A4: e Joins v0,v0,G1 & P = G1.walkOf(v0,e,v0) by Th57, XBOOLE_0:def 7;
P.first() = v0 & P.last() = v0 by A4, GLIB_001:15;
then A5: v0 = v & v0 = w by A2, GLIB_001:def 23;
v0 in the_Vertices_of G1 by A4, GLIB_000:13;
then reconsider v0 as Vertex of G2 by GLIB_000:53;
take G2.walkOf(v0);
thus G2.walkOf(v0) is_Walk_from v,w by A5, GLIB_001:13;
end;
end;
theorem Th62:
for G1 being _Graph, G2 being removeLoops of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2)
proof
let G1 be _Graph, G2 be removeLoops of G1;
for W1 being Walk of G1 ex W2 being Walk of G2
st W2 is_Walk_from W1.first(),W1.last() by Th61;
hence for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2) by Th35;
end;
registration
let G be connected _Graph;
cluster -> connected for removeLoops of G;
coherence
proof
let G2 be removeLoops of G;
for W1 being Walk of G ex W2 being Walk of G2
st W2 is_Walk_from W1.first(),W1.last() by Th61;
hence thesis by Th36;
end;
end;
registration
let G be non connected _Graph;
cluster -> non connected for removeLoops of G;
coherence;
end;
theorem
for G1 being _Graph, G2 being removeLoops of G1
holds G1.componentSet() = G2.componentSet()
proof
let G1 be _Graph, G2 be removeLoops of G1;
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2) by Th62;
hence thesis by Th37;
end;
theorem Th64:
for G1 being _Graph, G2 being removeLoops of G1
holds G1.numComponents() = G2.numComponents()
proof
let G1 be _Graph, G2 be removeLoops of G1;
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2) by Th62;
hence thesis by Th38;
end;
theorem Th65:
for G1 being _Graph, G2 being removeLoops of G1
holds G1 is chordal iff G2 is chordal
proof
let G1 be _Graph, G2 be removeLoops of G1;
hereby
assume A1: G1 is chordal;
now
let P2 be Walk of G2;
assume A2: P2.length() > 3 & P2 is Cycle-like;
now
reconsider P1 = P2 as Walk of G1 by GLIB_001:167;
P1.length() > 3 & P1 is Cycle-like by A2, GLIB_001:114, GLIB_006:24;
then consider m, n being odd Nat such that
A3: m+2 < n & n <= len P1 & P1.m <> P1.n and
A4: ex e being object st e Joins P1.m,P1.n,G1 and
A5: for f being object st f in P1.edges()
holds not f Joins P1.m,P1.n,G1 by A1, CHORD:def 11, CHORD:def 10;
take m, n;
thus m+2 < n & n <= len P2 & P2.m <> P2.n by A3;
hereby
consider e being object such that
A6: e Joins P1.m,P1.n,G1 by A4;
take e;
A7: e in the_Edges_of G1 by A6, GLIB_000:def 13;
not e in G1.loops() by A3, A6, Th46;
then e in the_Edges_of G1 \ G1.loops() by A7, XBOOLE_0:def 5;
then e in the_Edges_of G2 by GLIB_000:53;
hence e Joins P2.m,P2.n,G2 by A6, GLIB_000:73;
end;
let f be object;
assume f in P2.edges();
then f in P1.edges() by GLIB_001:110;
hence not f Joins P2.m,P2.n,G2 by A5, GLIB_000:72;
end;
hence P2 is chordal by CHORD:def 10;
end;
hence G2 is chordal by CHORD:def 11;
end;
assume A8: G2 is chordal;
now
let P1 be Walk of G1;
assume A9: P1.length() > 3 & P1 is Cycle-like;
now
P1.edges() misses G1.loops()
proof
assume P1.edges() meets G1.loops();
then consider v,e being object such that
A10: e Joins v,v,G1 & P1 = G1.walkOf(v,e,v) by A9, Th57;
2*P1.length()+1 = len P1 by GLIB_001:112
.= 2*1+1 by A10, GLIB_001:14;
hence contradiction by A9;
end;
then P1.edges() c= the_Edges_of G1 \ G1.loops() by XBOOLE_1:86;
then A11: P1.edges() c= the_Edges_of G2 by GLIB_000:53;
the_Vertices_of G1 = the_Vertices_of G2 by GLIB_000:53;
then P1.vertices() c= the_Vertices_of G2;
then reconsider P2 = P1 as Walk of G2 by A11, GLIB_001:170;
P2.length() > 3 & P2 is Cycle-like by A9, GLIB_001:114, GLIB_006:24;
then consider m, n being odd Nat such that
A12: m+2 < n & n <= len P2 & P2.m <> P2.n and
A13: ex e being object st e Joins P2.m,P2.n,G2 and
A14: for f being object st f in P2.edges()
holds not f Joins P2.m,P2.n,G2 by A8, CHORD:def 11, CHORD:def 10;
take m, n;
thus m+2 < n & n <= len P1 & P1.m <> P1.n by A12;
thus ex e being object st e Joins P1.m,P1.n,G1 by A13, GLIB_000:72;
let f be object;
assume f in P1.edges();
then A15: f in P2.edges() by GLIB_001:110;
then not f Joins P2.m,P2.n,G2 by A14;
hence not f Joins P1.m,P1.n,G1 by A15, GLIB_000:73;
end;
hence P1 is chordal by CHORD:def 10;
end;
hence G1 is chordal by CHORD:def 11;
end;
:: non chordal cluster after non chordal has been clustered with cycles
registration
let G be chordal _Graph;
cluster -> chordal for removeLoops of G;
coherence by Th65;
end;
:: More theorems of this kind can be produced with other
:: subgraph modes. This particular example was needed
:: to show that the cut-vertex property prevails in graphs
:: with removed loops
theorem Th66:
for G1 being _Graph, v being set, G2 being removeLoops of G1
for G3 being removeVertex of G1, v, G4 being removeVertex of G2, v
holds G4 is removeLoops of G3
proof
let G1 be _Graph, v be set, G2 be removeLoops of G1;
let G3 be removeVertex of G1, v, G4 be removeVertex of G2, v;
A1: the_Vertices_of G2 = the_Vertices_of G1 &
the_Edges_of G2 = the_Edges_of G1 \ G1.loops() by GLIB_000:53;
per cases;
suppose A2: G1 is non _trivial & v in the_Vertices_of G1;
then reconsider v1 = v as Vertex of G1;
reconsider v2 = v1 as Vertex of G2 by GLIB_000:53;
A3: the_Vertices_of G3 = the_Vertices_of G1 \ {v1} & the_Edges_of G3
= G1.edgesBetween(the_Vertices_of G1 \ {v1}) by A2, GLIB_000:47;
A4: the_Vertices_of G4 = the_Vertices_of G2 \ {v2} & the_Edges_of G4
= G2.edgesBetween(the_Vertices_of G2 \ {v2}) by A2, GLIB_000:47;
then A5: the_Vertices_of G4 = the_Vertices_of G3 by A3, GLIB_000:53;
A6: the_Edges_of G1 \ v1.edgesInOut()
= G1.edgesBetween(the_Vertices_of G1) \ v1.edgesInOut() by GLIB_000:34
.= the_Edges_of G3 by A3, GLIB_000:107;
A7: the_Edges_of G4 = G2.edgesBetween(the_Vertices_of G2)
\ v2.edgesInOut() by A4, GLIB_000:107
.= the_Edges_of G2 \ v2.edgesInOut() by GLIB_000:34
.= (the_Edges_of G1 \ G1.loops()) \ v2.edgesInOut() by GLIB_000:53
.= (the_Edges_of G1 \ G1.loops())
\ (v1.edgesInOut() /\ the_Edges_of G2) by GLIB_000:79
.= the_Edges_of G1 \ (G1.loops()
\/ (v1.edgesInOut() /\ the_Edges_of G2)) by XBOOLE_1:41
.= (the_Edges_of G1 \ (v1.edgesInOut() /\ the_Edges_of G2))
\ G1.loops() by XBOOLE_1:41
.= ((the_Edges_of G1 \ v1.edgesInOut()) \/ (the_Edges_of G1
\ the_Edges_of G2)) \ G1.loops() by XBOOLE_1:54
.= (the_Edges_of G3 \/ G1.loops()) \ G1.loops() by A1, A6, Th1
.= the_Edges_of G3 \ G1.loops() by XBOOLE_1:40;
now
let e be object;
hereby
assume e in the_Edges_of G3 \ G3.loops();
then A8: e in the_Edges_of G3 & not e in G3.loops() by XBOOLE_0:def 5;
not e in G1.loops()
proof
assume e in G1.loops();
then consider v being object such that
A9: e Joins v,v,G1 by Def2;
e is set & v is set by TARSKI:1;
then e Joins v,v,G3 by A8, A9, GLIB_000:73;
hence contradiction by A8, Def2;
end;
hence e in the_Edges_of G3 \ G1.loops() by A8, XBOOLE_0:def 5;
end;
assume A10: e in the_Edges_of G3 \ G1.loops();
G3.loops() c= G1.loops() by Th48;
hence e in the_Edges_of G3 \ G3.loops() by A10
, XBOOLE_1:34, TARSKI:def 3;
end;
then A11: the_Edges_of G4 = the_Edges_of G3 \ G3.loops() by A7, TARSKI:2;
G4 is Subgraph of G1 by GLIB_000:43;
then A12: G4 is Subgraph of G3 by A5, A11, XBOOLE_1:36, GLIB_000:44;
the_Edges_of G3 \ G3.loops() c= the_Edges_of G3 by XBOOLE_1:36;
then A13: the_Edges_of G3\G3.loops() c= G3.edgesBetween(the_Vertices_of G3)
by GLIB_000:34;
the_Vertices_of G3 c= the_Vertices_of G3;
hence thesis by A5, A11, A12, A13, GLIB_000:def 37;
end;
suppose A14: G1 is _trivial or not v in the_Vertices_of G1;
then A15: G1 == G3 by GLIB_000:114;
G2 == G4 by A1, A14, GLIB_000:114;
then G4 is removeLoops of G1 by Th59;
hence thesis by A15, Th60;
end;
end;
theorem Th67:
for G1 being _Graph, G2 being removeLoops of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds v1 is cut-vertex iff v2 is cut-vertex
proof
let G1 be _Graph, G2 be removeLoops of G1;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2;
hereby
assume A2: v1 is cut-vertex;
now
let G4 be removeVertex of G2, v2;
set G3 = the removeVertex of G1, v1;
G4 is removeLoops of G3 by A1, Th66;
then A3: G3.numComponents() = G4.numComponents() by Th64;
G1.numComponents() in G3.numComponents() by A2, GLIB_002:def 10;
hence G2.numComponents() in G4.numComponents() by A3, Th64;
end;
hence v2 is cut-vertex by GLIB_002:def 10;
end;
assume A4: v2 is cut-vertex;
now
let G3 be removeVertex of G1, v1;
set G4 = the removeVertex of G2, v2;
G4 is removeLoops of G3 by A1, Th66;
then A5: G3.numComponents() = G4.numComponents() by Th64;
G2.numComponents() in G4.numComponents() by A4, GLIB_002:def 10;
hence G1.numComponents() in G3.numComponents() by A5, Th64;
end;
hence v1 is cut-vertex by GLIB_002:def 10;
end;
theorem Th68:
for G1 being _Graph, G2 being removeLoops of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & v1 is endvertex holds v2 is endvertex
proof
let G1 be _Graph, G2 be removeLoops of G1;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2 & v1 is endvertex;
then consider e being object such that
A2: v1.edgesInOut() = {e} & not e Joins v1,v1,G1 by GLIB_000:def 51;
reconsider e as set by TARSKI:1;
e in {e} by TARSKI:def 1;
then consider w1 being Vertex of G1 such that
A3: e Joins v1,w1,G1 by A2, GLIB_000:64;
A4: not e in G1.loops() by A2, A3, Th46;
A5: the_Vertices_of G2 = the_Vertices_of G1 &
the_Edges_of G2 = the_Edges_of G1 \ G1.loops() by GLIB_000:53;
then reconsider w2 = w1 as Vertex of G2;
e in the_Edges_of G1 by A3, GLIB_000:def 13;
then e in the_Edges_of G2 by A4, A5, XBOOLE_0:def 5;
then e Joins v2,w2,G2 by A1, A3, GLIB_000:73;
then e in v2.edgesInOut() by GLIB_000:64;
hence thesis by A1, GLIB_000:def 49, GLIB_000:84;
end;
begin :: Graphs with parallel Edges removed
definition
let G be _Graph;
func EdgeAdjEqRel(G) -> Equivalence_Relation of the_Edges_of G means
:Def3:
for e1, e2 being object holds [e1,e2] in it iff
ex v1, v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G;
existence
proof
defpred P[object,object] means ex v1, v2 being object
st $1 Joins v1,v2,G & $2 Joins v1,v2,G;
A1: for e being object st e in the_Edges_of G holds P[e,e]
proof
let e be object;
assume A2: e in the_Edges_of G;
take (the_Source_of G).e, (the_Target_of G).e;
thus thesis by A2, GLIB_000:def 13;
end;
A3: for e1,e2 being object st P[e1,e2] holds P[e2,e1];
A4: for e1,e2,e3 being object st P[e1,e2] & P[e2,e3] holds P[e1,e3]
proof
let e1,e2,e3 be object;
assume A5: P[e1,e2] & P[e2,e3];
then consider v1,v2 being object such that
A6: e1 Joins v1,v2,G & e2 Joins v1,v2,G;
consider v3,v4 being object such that
A7: e2 Joins v3,v4,G & e3 Joins v3,v4,G by A5;
take v1,v2;
thus e1 Joins v1,v2,G by A6;
per cases by A6, A7, GLIB_000:15;
suppose v1 = v3 & v2 = v4;
hence e3 Joins v1,v2,G by A7;
end;
suppose v1 = v4 & v2 = v3;
hence e3 Joins v1,v2,G by A7, GLIB_000:14;
end;
end;
consider EqR being Equivalence_Relation of the_Edges_of G such that
A8: for e1,e2 being object holds [e1,e2] in EqR iff
e1 in the_Edges_of G & e2 in the_Edges_of G & P[e1,e2]
from EQREL_1:sch 1(A1,A3,A4);
take EqR;
let e1,e2 be object;
thus [e1,e2] in EqR implies ex v1,v2 being object
st e1 Joins v1,v2,G & e2 Joins v1,v2,G by A8;
given v1,v2 being object such that
A9: e1 Joins v1,v2,G & e2 Joins v1,v2,G;
e1 in the_Edges_of G & e2 in the_Edges_of G by A9, GLIB_000:def 13;
hence thesis by A8, A9;
end;
uniqueness
proof
let EqR1, EqR2 be Equivalence_Relation of the_Edges_of G;
assume that
A10: for e1, e2 being object holds [e1,e2] in EqR1 iff
ex v1, v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G and
A11: for e1, e2 being object holds [e1,e2] in EqR2 iff
ex v1, v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G;
now
let e1,e2 be object;
[e1,e2] in EqR1 iff
ex v1, v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G by A10;
hence [e1,e2] in EqR1 iff [e1,e2] in EqR2 by A11;
end;
hence EqR1 = EqR2 by RELAT_1:def 2;
end;
func DEdgeAdjEqRel(G) -> Equivalence_Relation of the_Edges_of G means
:Def4:
for e1, e2 being object holds [e1,e2] in it iff
ex v1, v2 being object st e1 DJoins v1,v2,G & e2 DJoins v1,v2,G;
existence
proof
defpred P[object,object] means ex v1, v2 being object
st $1 DJoins v1,v2,G & $2 DJoins v1,v2,G;
A12: for e being object st e in the_Edges_of G holds P[e,e]
proof
let e be object;
assume A13: e in the_Edges_of G;
take (the_Source_of G).e, (the_Target_of G).e;
thus thesis by A13, GLIB_000:def 14;
end;
A14: for e1,e2 being object st P[e1,e2] holds P[e2,e1];
A15: for e1,e2,e3 being object st P[e1,e2] & P[e2,e3] holds P[e1,e3]
proof
let e1,e2,e3 be object;
assume A16: P[e1,e2] & P[e2,e3];
then consider v1,v2 being object such that
A17: e1 DJoins v1,v2,G & e2 DJoins v1,v2,G;
consider v3,v4 being object such that
A18: e2 DJoins v3,v4,G & e3 DJoins v3,v4,G by A16;
take v1,v2;
v1 = v3 & v2 = v4 by A17, A18, GLIB_000:125;
hence e1 DJoins v1,v2,G & e3 DJoins v1,v2,G by A17, A18;
end;
consider EqR being Equivalence_Relation of the_Edges_of G such that
A19: for e1,e2 being object holds [e1,e2] in EqR iff
e1 in the_Edges_of G & e2 in the_Edges_of G & P[e1,e2]
from EQREL_1:sch 1(A12,A14,A15);
take EqR;
let e1,e2 be object;
thus [e1,e2] in EqR implies ex v1,v2 being object
st e1 DJoins v1,v2,G & e2 DJoins v1,v2,G by A19;
given v1,v2 being object such that
A20: e1 DJoins v1,v2,G & e2 DJoins v1,v2,G;
e1 in the_Edges_of G & e2 in the_Edges_of G by A20, GLIB_000:def 14;
hence thesis by A19, A20;
end;
uniqueness
proof
let EqR1, EqR2 be Equivalence_Relation of the_Edges_of G;
assume that
A21: for e1, e2 being object holds [e1,e2] in EqR1 iff
ex v1, v2 being object st e1 DJoins v1,v2,G & e2 DJoins v1,v2,G and
A22: for e1, e2 being object holds [e1,e2] in EqR2 iff
ex v1, v2 being object st e1 DJoins v1,v2,G & e2 DJoins v1,v2,G;
now
let e1,e2 be object;
[e1,e2] in EqR1 iff
ex v1, v2 being object st e1 DJoins v1,v2,G & e2 DJoins v1,v2,G by A21;
hence [e1,e2] in EqR1 iff [e1,e2] in EqR2 by A22;
end;
hence EqR1 = EqR2 by RELAT_1:def 2;
end;
end;
theorem
for G being _Graph holds DEdgeAdjEqRel(G) c= EdgeAdjEqRel(G)
proof
let G be _Graph;
now
let e1,e2 be object;
assume [e1,e2] in DEdgeAdjEqRel(G);
then consider v1,v2 being object such that
A1: e1 DJoins v1,v2,G & e2 DJoins v1,v2,G by Def4;
e1 Joins v1,v2,G & e2 Joins v1,v2,G by A1, GLIB_000:16;
hence [e1,e2] in EdgeAdjEqRel(G) by Def3;
end;
hence thesis by RELAT_1:def 3;
end;
theorem
for G being _Graph
holds G is non-multi iff EdgeAdjEqRel(G) = id the_Edges_of G
proof
let G be _Graph;
hereby
assume A1: G is non-multi;
now
let e1,e2 be object;
hereby
assume [e1,e2] in EdgeAdjEqRel(G);
then consider v1,v2 being object such that
A2: e1 Joins v1,v2,G & e2 Joins v1,v2,G by Def3;
A3: e1 = e2 by A1, A2, GLIB_000:def 20;
e1 in the_Edges_of G & e2 in the_Edges_of G by A2, GLIB_000:def 13;
hence [e1,e2] in id the_Edges_of G by A3, RELAT_1:def 10;
end;
assume [e1,e2] in id the_Edges_of G;
then A4: e1 in the_Edges_of G & e1 = e2 by RELAT_1:def 10;
now
reconsider v1 = (the_Source_of G).e1, v2 = (the_Target_of G).e1
as object;
take v1,v2;
thus e1 Joins v1,v2,G & e2 Joins v1,v2,G by A4, GLIB_000:def 13;
end;
hence [e1,e2] in EdgeAdjEqRel(G) by Def3;
end;
hence EdgeAdjEqRel(G) = id the_Edges_of G by RELAT_1:def 2;
end;
assume A5: EdgeAdjEqRel(G) = id the_Edges_of G;
now
let e1,e2,v1,v2 be object;
assume e1 Joins v1,v2,G & e2 Joins v1,v2,G;
then [e1,e2] in EdgeAdjEqRel(G) by Def3;
hence e1 = e2 by A5, RELAT_1:def 10;
end;
hence thesis by GLIB_000:def 20;
end;
theorem
for G being _Graph
holds G is non-Dmulti iff DEdgeAdjEqRel(G) = id the_Edges_of G
proof
let G be _Graph;
hereby
assume A1: G is non-Dmulti;
now
let e1,e2 be object;
hereby
assume [e1,e2] in DEdgeAdjEqRel(G);
then consider v1,v2 being object such that
A2: e1 DJoins v1,v2,G & e2 DJoins v1,v2,G by Def4;
A3: e1 = e2 by A1, A2, GLIB_000:def 21;
e1 in the_Edges_of G & e2 in the_Edges_of G by A2, GLIB_000:def 14;
hence [e1,e2] in id the_Edges_of G by A3, RELAT_1:def 10;
end;
assume [e1,e2] in id the_Edges_of G;
then A4: e1 in the_Edges_of G & e1 = e2 by RELAT_1:def 10;
now
reconsider v1 = (the_Source_of G).e1, v2 = (the_Target_of G).e1
as object;
take v1,v2;
thus e1 DJoins v1,v2,G & e2 DJoins v1,v2,G by A4, GLIB_000:def 14;
end;
hence [e1,e2] in DEdgeAdjEqRel(G) by Def4;
end;
hence DEdgeAdjEqRel(G) = id the_Edges_of G by RELAT_1:def 2;
end;
assume A5: DEdgeAdjEqRel(G) = id the_Edges_of G;
now
let e1,e2,v1,v2 be object;
assume e1 DJoins v1,v2,G & e2 DJoins v1,v2,G;
then [e1,e2] in DEdgeAdjEqRel(G) by Def4;
hence e1 = e2 by A5, RELAT_1:def 10;
end;
hence thesis by GLIB_000:def 21;
end;
registration
let G be edgeless _Graph;
cluster EdgeAdjEqRel(G) -> empty;
coherence;
cluster DEdgeAdjEqRel(G) -> empty;
coherence;
end;
registration
let G be non edgeless _Graph;
cluster EdgeAdjEqRel(G) -> non empty;
coherence;
cluster DEdgeAdjEqRel(G) -> non empty;
coherence;
end;
definition
let G be _Graph; :: Rep is short for Representative
mode RepEdgeSelection of G -> Subset of the_Edges_of G means
:Def5:
for v,w,e0 being object st e0 Joins v,w,G
ex e being object st e Joins v,w,G & e in it &
for e9 being object st e9 Joins v,w,G & e9 in it holds e9 = e;
existence
proof
per cases;
suppose the_Edges_of G = {};
then A1: G is edgeless;
take {}the_Edges_of G;
thus thesis by A1, GLIB_008:50;
end;
suppose A2: the_Edges_of G <> {};
set E = {the Element of Class(EdgeAdjEqRel(G),e)
where e is Element of the_Edges_of G : not contradiction};
for x being object holds x in E implies x in the_Edges_of G
proof
let x be object;
assume x in E;
then consider e being Element of the_Edges_of G such that
A3: x = the Element of Class(EdgeAdjEqRel(G),e);
[e,e] in EdgeAdjEqRel(G) by A2, EQREL_1:5;
then Class(EdgeAdjEqRel(G),e) <> {} by RELAT_1:169;
then [e,x] in EdgeAdjEqRel(G) by A3, EQREL_1:18;
then consider v1,v2 being object such that
A4: e Joins v1,v2,G & x Joins v1,v2,G by Def3;
thus thesis by A4, GLIB_000:def 13;
end;
then reconsider E as Subset of the_Edges_of G by TARSKI:def 3;
take E;
let v,w,e0 be object;
assume A5: e0 Joins v,w,G;
then A6: e0 in the_Edges_of G by GLIB_000:def 13;
then reconsider e0 as Element of the_Edges_of G;
set e = the Element of Class(EdgeAdjEqRel(G),e0);
take e;
[e0,e0] in EdgeAdjEqRel(G) by A6, EQREL_1:5;
then Class(EdgeAdjEqRel(G),e0) <> {} by RELAT_1:169;
then [e0,e] in EdgeAdjEqRel(G) by EQREL_1:18;
then consider v1,v2 being object such that
A7: e0 Joins v1,v2,G & e Joins v1,v2,G by Def3;
thus e Joins v,w,G
proof
per cases by A5, A7, GLIB_000:15;
suppose v = v1 & w = v2;
hence thesis by A7;
end;
suppose v = v2 & w = v1;
hence thesis by A7, GLIB_000:14;
end;
end;
thus e in E;
let e9 be object;
assume A8: e9 Joins v,w,G & e9 in E;
then consider e8 being Element of the_Edges_of G such that
A9: e9 = the Element of Class(EdgeAdjEqRel(G),e8);
[e8,e8] in EdgeAdjEqRel(G) by A6, EQREL_1:5;
then Class(EdgeAdjEqRel(G),e8) <> {} by RELAT_1:169;
then A10: e9 in Class(EdgeAdjEqRel(G),e8) by A9;
[e0,e9] in EdgeAdjEqRel(G) by A5, A8, Def3;
then e9 in Class(EdgeAdjEqRel(G),e0) by EQREL_1:18;
then Class(EdgeAdjEqRel(G),e0) = Class(EdgeAdjEqRel(G),e9) by EQREL_1:23
.= Class(EdgeAdjEqRel(G),e8) by A10, EQREL_1:23;
hence e9 = e by A9;
end;
end;
mode RepDEdgeSelection of G -> Subset of the_Edges_of G means
:Def6:
for v,w,e0 being object st e0 DJoins v,w,G
ex e being object st e DJoins v,w,G & e in it &
for e9 being object st e9 DJoins v,w,G & e9 in it holds e9 = e;
existence
proof
per cases;
suppose the_Edges_of G = {};
then A11: G is edgeless;
take {}the_Edges_of G;
thus thesis by A11, GLIB_008:50;
end;
suppose A12: the_Edges_of G <> {};
set E = {the Element of Class(DEdgeAdjEqRel(G),e)
where e is Element of the_Edges_of G : not contradiction};
for x being object holds x in E implies x in the_Edges_of G
proof
let x be object;
assume x in E;
then consider e being Element of the_Edges_of G such that
A13: x = the Element of Class(DEdgeAdjEqRel(G),e);
[e,e] in DEdgeAdjEqRel(G) by A12, EQREL_1:5;
then Class(DEdgeAdjEqRel(G),e) <> {} by RELAT_1:169;
then [e,x] in DEdgeAdjEqRel(G) by A13, EQREL_1:18;
then consider v1,v2 being object such that
A14: e DJoins v1,v2,G & x DJoins v1,v2,G by Def4;
thus thesis by A14, GLIB_000:def 14;
end;
then reconsider E as Subset of the_Edges_of G by TARSKI:def 3;
take E;
let v,w,e0 be object;
assume A15: e0 DJoins v,w,G;
then A16: e0 in the_Edges_of G by GLIB_000:def 14;
then reconsider e0 as Element of the_Edges_of G;
set e = the Element of Class(DEdgeAdjEqRel(G),e0);
take e;
[e0,e0] in DEdgeAdjEqRel(G) by A15, EQREL_1:5, GLIB_000:def 14;
then Class(DEdgeAdjEqRel(G),e0) <> {} by RELAT_1:169;
then [e0,e] in DEdgeAdjEqRel(G) by EQREL_1:18;
then consider v1,v2 being object such that
A17: e0 DJoins v1,v2,G & e DJoins v1,v2,G by Def4;
v = v1 & w = v2 by A15, A17, GLIB_000:125;
hence e DJoins v,w,G by A17;
thus e in E;
let e9 be object;
assume A18: e9 DJoins v,w,G & e9 in E;
then consider e8 being Element of the_Edges_of G such that
A19: e9 = the Element of Class(DEdgeAdjEqRel(G),e8);
[e8,e8] in DEdgeAdjEqRel(G) by A16, EQREL_1:5;
then Class(DEdgeAdjEqRel(G),e8) <> {} by RELAT_1:169;
then A20: e9 in Class(DEdgeAdjEqRel(G),e8) by A19;
[e0,e9] in DEdgeAdjEqRel(G) by A15, A18, Def4;
then e9 in Class(DEdgeAdjEqRel(G),e0) by EQREL_1:18;
then Class(DEdgeAdjEqRel(G),e0) = Class(DEdgeAdjEqRel(G),e9)
by EQREL_1:23
.= Class(DEdgeAdjEqRel(G),e8) by A20, EQREL_1:23;
hence e9 = e by A19;
end;
end;
end;
registration
let G be edgeless _Graph;
cluster -> empty for RepEdgeSelection of G;
coherence
proof
let E be RepEdgeSelection of G;
the_Edges_of G = {};
hence thesis by XBOOLE_1:3;
end;
cluster -> empty for RepDEdgeSelection of G;
coherence
proof
let E be RepDEdgeSelection of G;
the_Edges_of G = {};
hence thesis by XBOOLE_1:3;
end;
end;
registration
let G be non edgeless _Graph;
cluster -> non empty for RepEdgeSelection of G;
coherence
proof
let E be RepEdgeSelection of G;
consider e0 being object such that
A1: e0 in the_Edges_of G by XBOOLE_0:def 1;
set v = (the_Source_of G).e0, w = (the_Target_of G).e0;
e0 Joins v,w,G by A1, GLIB_000:def 13;
then consider e being object such that
A2: e Joins v,w,G & e in E and
for e9 being object st e9 Joins v,w,G & e9 in E holds e9 = e by Def5;
thus thesis by A2;
end;
cluster -> non empty for RepDEdgeSelection of G;
coherence
proof
let E be RepDEdgeSelection of G;
consider e0 being object such that
A3: e0 in the_Edges_of G by XBOOLE_0:def 1;
set v = (the_Source_of G).e0, w = (the_Target_of G).e0;
consider e being object such that
A4: e DJoins v,w,G & e in E and
for e9 being object st e9 DJoins v,w,G & e9 in E holds e9 = e
by A3, Def6, GLIB_000:def 14;
thus thesis by A4;
end;
end;
theorem Th72:
for G being _Graph, E1 being RepDEdgeSelection of G
ex E2 being RepEdgeSelection of G st E2 c= E1
proof
let G be _Graph, E1 be RepDEdgeSelection of G;
set A = {{e where e is Element of the_Edges_of G : e Joins v1,v2,G & e in E1}
where v1,v2 is Vertex of G : ex e0 being object st e0 Joins v1,v2,G};
defpred P[object,object] means ex S being non empty set
st $1 = S & $2 = the Element of S;
A1: for x,y1,y2 being object st x in A & P[x,y1] & P[x,y2] holds y1 = y2;
A2: for x being object st x in A ex y being object st P[x,y]
proof
let x be object;
assume x in A;
then consider v1,v2 being Vertex of G such that
A3: x = {e where e is Element of the_Edges_of G :
e Joins v1,v2,G & e in E1} and
A4: ex e0 being object st e0 Joins v1,v2,G;
reconsider B = x as set by A3;
consider e0 being object such that
A5: e0 Joins v1,v2,G by A4;
per cases by A5, GLIB_000:16;
suppose e0 DJoins v1,v2,G;
then consider e being object such that
A6: e DJoins v1,v2,G & e in E1 and
for e9 being object st e9 DJoins v1,v2,G & e9 in E1 holds e9 = e
by Def6;
e in the_Edges_of G & e Joins v1,v2,G by A6, GLIB_000:16;
then e in B by A3, A6;
then reconsider B as non empty set;
take the Element of B, B;
thus thesis;
end;
suppose e0 DJoins v2,v1,G;
then consider e being object such that
A7: e DJoins v2,v1,G & e in E1 and
for e9 being object st e9 DJoins v2,v1,G & e9 in E1 holds e9 = e
by Def6;
e in the_Edges_of G & e Joins v1,v2,G by A7, GLIB_000:16;
then e in B by A3, A7;
then reconsider B as non empty set;
take the Element of B, B;
thus thesis;
end;
end;
consider f being Function such that
A8: dom f = A & for x being object st x in A holds P[x,f.x]
from FUNCT_1:sch 2(A1,A2);
for e being object holds e in rng f implies e in E1
proof
let e be object;
assume e in rng f;
then consider C being object such that
A9: C in dom f & f.C = e by FUNCT_1:def 3;
consider C0 being non empty set such that
A10: C = C0 & f.C = the Element of C0 by A8, A9;
consider v1,v2 being Vertex of G such that
A11: C = {e2 where e2 is Element of the_Edges_of G :
e2 Joins v1,v2,G & e2 in E1} and
ex e8 being object st e8 Joins v1,v2,G by A8, A9;
e in C0 by A9, A10;
then consider e2 being Element of the_Edges_of G such that
A12: e = e2 & e2 Joins v1,v2,G & e2 in E1 by A10, A11;
thus e in E1 by A12;
end;
then A13: rng f c= E1 by TARSKI:def 3;
then reconsider E2 = rng f as Subset of the_Edges_of G by XBOOLE_1:1;
for v,w,e0 being object st e0 Joins v,w,G
ex e being object st e Joins v,w,G & e in E2 &
for e9 being object st e9 Joins v,w,G & e9 in E2 holds e9 = e
proof
let v,w,e0 be object;
assume A14: e0 Joins v,w,G;
set B = {e where e is Element of the_Edges_of G :
e Joins v,w,G & e in E1};
v in the_Vertices_of G & w in the_Vertices_of G by A14, GLIB_000:13;
then A15: B in A by A14;
then consider B0 being non empty set such that
A16: B = B0 & f.B = the Element of B0 by A8;
f.B in B by A16;
then consider e being Element of the_Edges_of G such that
A17: f.B = e & e Joins v,w,G & e in E1;
take e;
thus e Joins v,w,G by A17;
thus e in E2 by A8, A15, A17, FUNCT_1:3;
let e9 be object;
assume A18: e9 Joins v,w,G & e9 in E2;
then consider C being object such that
A19: C in dom f & f.C = e9 by FUNCT_1:def 3;
consider v1,v2 being Vertex of G such that
A20: C = {e2 where e2 is Element of the_Edges_of G :
e2 Joins v1,v2,G & e2 in E1} and
ex e8 being object st e8 Joins v1,v2,G by A8, A19;
consider C0 being non empty set such that
A21: C = C0 & f.C = the Element of C0 by A8, A19;
e9 in C0 by A19, A21;
then consider e2 being Element of the_Edges_of G such that
A22: e9 = e2 & e2 Joins v1,v2,G & e2 in E1 by A20, A21;
per cases by A18, A22, GLIB_000:15;
suppose v = v1 & w = v2;
hence e9 = e by A17, A19, A20;
end;
suppose A23: v = v2 & w = v1;
for x being object holds x in C0 iff x in B
proof
let x be object;
hereby
assume x in C0;
then consider e2 being Element of the_Edges_of G such that
A24: x = e2 & e2 Joins v1,v2,G & e2 in E1 by A20, A21;
e2 Joins v,w,G by A23, A24, GLIB_000:14;
hence x in B by A24;
end;
assume x in B;
then consider e1 being Element of the_Edges_of G such that
A25: x = e1 & e1 Joins v,w,G & e1 in E1;
e1 Joins v1,v2,G by A23, A25, GLIB_000:14;
hence x in C0 by A20, A21, A25;
end;
hence e9 = e by A17, A19, A21, TARSKI:2;
end;
end;
then reconsider E2 as RepEdgeSelection of G by Def5;
take E2;
thus thesis by A13;
end;
theorem Th73:
for G being _Graph, E2 being RepEdgeSelection of G
ex E1 being RepDEdgeSelection of G st E2 c= E1
proof
let G be _Graph, E2 be RepEdgeSelection of G;
set A = {{e where e is Element of the_Edges_of G : e DJoins v1,v2,G}
where v1,v2 is Vertex of G : (ex e0 being object st e0 DJoins v1,v2,G) &
(for e0 being object st e0 DJoins v1,v2,G holds not e0 in E2)};
defpred P[object,object] means ex S being non empty set
st $1 = S & $2 = the Element of S;
A1: for x,y1,y2 being object st x in A & P[x,y1] & P[x,y2] holds y1 = y2;
A2: for x being object st x in A ex y being object st P[x,y]
proof
let x be object;
assume x in A;
then consider v1,v2 being Vertex of G such that
A3: x = {e where e is Element of the_Edges_of G : e DJoins v1,v2,G} and
A4: ex e0 being object st e0 DJoins v1,v2,G and
for e0 being object st e0 DJoins v1,v2,G holds not e0 in E2;
reconsider B = x as set by A3;
consider e0 being object such that
A5: e0 DJoins v1,v2,G by A4;
reconsider e0 as Element of the_Edges_of G by A5, GLIB_000:def 14;
e0 in B by A3, A5;
then reconsider B as non empty set;
take the Element of B, B;
thus thesis;
end;
consider f being Function such that
A6: dom f = A & for x being object st x in A holds P[x,f.x]
from FUNCT_1:sch 2(A1,A2);
for e being object holds e in rng f implies e in the_Edges_of G
proof
let e be object;
assume e in rng f;
then consider C being object such that
A7: C in dom f & f.C = e by FUNCT_1:def 3;
consider C0 being non empty set such that
A8: C = C0 & f.C = the Element of C0 by A6, A7;
consider v1,v2 being Vertex of G such that
A9: C = {e where e is Element of the_Edges_of G : e DJoins v1,v2,G} and
ex e0 being object st e0 DJoins v1,v2,G and
for e0 being object st e0 DJoins v1,v2,G holds not e0 in E2 by A6, A7;
e in C0 by A7, A8;
then consider e2 being Element of the_Edges_of G such that
A10: e = e2 & e2 DJoins v1,v2,G by A8, A9;
thus e in the_Edges_of G by A10, GLIB_000:def 14;
end;
then rng f c= the_Edges_of G by TARSKI:def 3;
then reconsider E1 = E2 \/ rng f as Subset of the_Edges_of G by XBOOLE_1:8;
for v,w,e0 being object st e0 DJoins v,w,G
ex e being object st e DJoins v,w,G & e in E1 &
for e9 being object st e9 DJoins v,w,G & e9 in E1 holds e9 = e
proof
let v,w,e0 be object;
assume A11: e0 DJoins v,w,G;
then e0 Joins v,w,G by GLIB_000:16;
then consider e2 being object such that
A12: e2 Joins v,w,G & e2 in E2 and
A13: for e8 being object st e8 Joins v,w,G & e8 in E2 holds e8 = e2
by Def5;
per cases by A12, GLIB_000:16;
suppose A14: e2 DJoins v,w,G;
take e2;
thus e2 DJoins v,w,G & e2 in E1 by A12, A14, TARSKI:def 3, XBOOLE_1:7;
let e9 be object;
assume A15: e9 DJoins v,w,G & e9 in E1;
not e9 in rng f
proof
assume e9 in rng f;
then consider C being object such that
A16: C in dom f & f.C = e9 by FUNCT_1:def 3;
consider C0 being non empty set such that
A17: C = C0 & f.C = the Element of C0 by A6, A16;
consider v1,v2 being Vertex of G such that
A18: C = {e where e is Element of the_Edges_of G : e DJoins v1,v2,G}
and ex e0 being object st e0 DJoins v1,v2,G and
A19: for e0 being object st e0 DJoins v1,v2,G holds not e0 in E2
by A6, A16;
e9 in C0 by A16, A17;
then consider e being Element of the_Edges_of G such that
A20: e9 = e & e DJoins v1,v2,G by A17, A18;
v = v1 & w = v2 by A15, A20, GLIB_000:125;
hence contradiction by A12, A14, A19;
end;
then A21: e9 in E2 by A15, XBOOLE_0:def 3;
e9 Joins v,w,G by A15, GLIB_000:16;
hence e9 = e2 by A13, A21;
end;
suppose A22: e2 DJoins w,v,G & not e2 DJoins v,w,G;
set B = {e where e is Element of the_Edges_of G : e DJoins v,w,G};
A23: for e9 being object st e9 DJoins v,w,G holds not e9 in E2
proof
given e9 being object such that
A24: e9 DJoins v,w,G & e9 in E2;
e9 Joins v,w,G by A24, GLIB_000:16;
hence contradiction by A13, A22, A24;
end;
v in the_Vertices_of G & w in the_Vertices_of G by A12, GLIB_000:13;
then A25: B in A by A11, A23;
then consider B0 being non empty set such that
A26: B = B0 & f.B = the Element of B0 by A6;
f.B in B0 by A26;
then consider e being Element of the_Edges_of G such that
A27: f.B = e & e DJoins v,w,G by A26;
take e;
thus e DJoins v,w,G by A27;
e in rng f by A6, A25, A27, FUNCT_1:3;
hence e in E1 by XBOOLE_1:7, TARSKI:def 3;
let e9 be object;
assume A28: e9 DJoins v,w,G & e9 in E1;
not e9 in E2
proof
assume A29: e9 in E2;
e9 Joins v,w,G by A28, GLIB_000:16;
hence contradiction by A13, A22, A28, A29;
end;
then e9 in rng f by A28, XBOOLE_0:def 3;
then consider C being object such that
A30: C in dom f & f.C = e9 by FUNCT_1:def 3;
consider C0 being non empty set such that
A31: C = C0 & f.C = the Element of C0 by A6, A30;
consider v1,v2 being Vertex of G such that
A32: C = {e1 where e1 is Element of the_Edges_of G : e1 DJoins v1,v2,G}
and ex e7 being object st e7 DJoins v1,v2,G and
for e7 being object st e7 DJoins v1,v2,G holds not e7 in E2
by A6, A30;
e9 in C0 by A30, A31;
then consider e1 being Element of the_Edges_of G such that
A33: e9 = e1 & e1 DJoins v1,v2,G by A31, A32;
v = v1 & w = v2 by A28, A33, GLIB_000:125;
hence e9 = e by A27, A30, A32;
end;
end;
then reconsider E1 as RepDEdgeSelection of G by Def6;
take E1;
thus thesis by XBOOLE_1:7;
end;
theorem Th74:
for G being non-multi _Graph, E being RepEdgeSelection of G
holds E = the_Edges_of G
proof
let G be non-multi _Graph, E be RepEdgeSelection of G;
for e being object holds e in the_Edges_of G implies e in E
proof
let e be object;
set v = (the_Source_of G).e, w = (the_Target_of G).e;
assume e in the_Edges_of G;
then A1: e Joins v,w,G by GLIB_000:def 13;
then consider e2 being object such that
A2: e2 Joins v,w,G & e2 in E and
for e9 being object st e9 Joins v,w,G & e9 in E holds e9 = e2
by Def5;
thus thesis by A1, A2, GLIB_000:def 20;
end;
then the_Edges_of G c= E by TARSKI:def 3;
hence E = the_Edges_of G by XBOOLE_0:def 10;
end;
theorem Th75:
for G being _Graph st ex E being RepEdgeSelection of G st E = the_Edges_of G
holds G is non-multi
proof
let G be _Graph;
given E being RepEdgeSelection of G such that
A1: E = the_Edges_of G;
now
let e1,e2,v1,v2 be object;
assume A2: e1 Joins v1,v2,G & e2 Joins v1,v2,G;
then consider e3 being object such that
e3 Joins v1,v2,G & e3 in E and
A3: for e being object st e Joins v1,v2,G & e in E holds e = e3
by Def5;
e1 in the_Edges_of G & e2 in the_Edges_of G &
E = the_Edges_of G by A1, A2, GLIB_000:def 13;
then e1 = e3 & e2 = e3 by A2, A3;
hence e1 = e2;
end;
hence thesis by GLIB_000:def 20;
end;
theorem Th76:
for G being non-Dmulti _Graph, E being RepDEdgeSelection of G
holds E = the_Edges_of G
proof
let G be non-Dmulti _Graph, E be RepDEdgeSelection of G;
for e being object holds e in the_Edges_of G implies e in E
proof
let e be object;
set v = (the_Source_of G).e, w = (the_Target_of G).e;
assume e in the_Edges_of G;
then A1: e DJoins v,w,G by GLIB_000:def 14;
then consider e2 being object such that
A2: e2 DJoins v,w,G & e2 in E and
for e9 being object st e9 DJoins v,w,G & e9 in E holds e9 = e2
by Def6;
thus thesis by A1, A2, GLIB_000:def 21;
end;
then the_Edges_of G c= E by TARSKI:def 3;
hence E = the_Edges_of G by XBOOLE_0:def 10;
end;
theorem Th77:
for G being _Graph st ex E being RepDEdgeSelection of G st E = the_Edges_of G
holds G is non-Dmulti
proof
let G be _Graph;
given E being RepDEdgeSelection of G such that
A1: E = the_Edges_of G;
now
let e1,e2,v1,v2 be object;
assume A2: e1 DJoins v1,v2,G & e2 DJoins v1,v2,G;
then consider e3 being object such that
e3 DJoins v1,v2,G & e3 in E and
A3: for e being object st e DJoins v1,v2,G & e in E holds e = e3
by Def6;
e1 = e3 & e2 = e3 by A1, A2, A3, GLIB_000:def 14;
hence e1 = e2;
end;
hence thesis by GLIB_000:def 21;
end;
theorem Th78:
for G1 being _Graph, G2 being Subgraph of G1, E being RepEdgeSelection of G1
st E c= the_Edges_of G2 holds E is RepEdgeSelection of G2
proof
let G1 be _Graph, G2 be Subgraph of G1, E be RepEdgeSelection of G1;
assume A1: E c= the_Edges_of G2;
now
let v,w,e0 be object;
A2: v is set & w is set by TARSKI:1;
assume e0 Joins v,w,G2;
then consider e being object such that
A3: e Joins v,w,G1 & e in E and
A4: for e9 being object st e9 Joins v,w,G1 & e9 in E holds e9 = e
by A2, Def5, GLIB_000:72;
take e;
thus e Joins v,w,G2 & e in E by A1, A2, A3, GLIB_000:73;
let e9 be object;
assume e9 Joins v,w,G2 & e9 in E;
hence e9 = e by A2, A4, GLIB_000:72;
end;
hence thesis by A1, Def5;
end;
theorem Th79:
for G1 being _Graph, G2 being Subgraph of G1, E being RepDEdgeSelection of G1
st E c= the_Edges_of G2 holds E is RepDEdgeSelection of G2
proof
let G1 be _Graph, G2 be Subgraph of G1, E be RepDEdgeSelection of G1;
assume A1: E c= the_Edges_of G2;
now
let v,w,e0 be object;
A2: v is set & w is set by TARSKI:1;
assume e0 DJoins v,w,G2;
then consider e being object such that
A3: e DJoins v,w,G1 & e in E and
A4: for e9 being object st e9 DJoins v,w,G1 & e9 in E holds e9 = e
by A2, Def6, GLIB_000:72;
take e;
thus e DJoins v,w,G2 & e in E by A1, A2, A3, GLIB_000:73;
let e9 be object;
assume e9 DJoins v,w,G2 & e9 in E;
hence e9 = e by A2, A4, GLIB_000:72;
end;
hence thesis by A1, Def6;
end;
theorem Th80:
for G1 being _Graph, G2 being Subgraph of G1,E2 being RepEdgeSelection of G2
ex E1 being RepEdgeSelection of G1 st E2 = E1 /\ the_Edges_of G2
proof
let G1 be _Graph, G2 be Subgraph of G1, E2 be RepEdgeSelection of G2;
set A = {{e where e is Element of the_Edges_of G1 : e Joins v1,v2,G1}
where v1,v2 is Vertex of G1 : (ex e0 being object st e0 Joins v1,v2,G1) &
(for e0 being object st e0 Joins v1,v2,G1 holds not e0 in E2)};
defpred P[object,object] means ex S being non empty set
st $1 = S & $2 = the Element of S;
A1: for x,y1,y2 being object st x in A & P[x,y1] & P[x,y2] holds y1 = y2;
A2: for x being object st x in A ex y being object st P[x,y]
proof
let x be object;
assume x in A;
then consider v1,v2 being Vertex of G1 such that
A3: x = {e where e is Element of the_Edges_of G1 : e Joins v1,v2,G1} and
A4: ex e0 being object st e0 Joins v1,v2,G1 and
for e0 being object st e0 Joins v1,v2,G1 holds not e0 in E2;
reconsider B = x as set by A3;
consider e0 being object such that
A5: e0 Joins v1,v2,G1 by A4;
reconsider e0 as Element of the_Edges_of G1 by A5, GLIB_000:def 13;
e0 in B by A3, A5;
then reconsider B as non empty set;
take the Element of B, B;
thus thesis;
end;
consider f being Function such that
A6: dom f = A & for x being object st x in A holds P[x,f.x]
from FUNCT_1:sch 2(A1,A2);
for e being object holds e in rng f implies e in the_Edges_of G1
proof
let e be object;
assume e in rng f;
then consider C being object such that
A7: C in dom f & f.C = e by FUNCT_1:def 3;
consider C0 being non empty set such that
A8: C = C0 & f.C = the Element of C0 by A6, A7;
consider v1,v2 being Vertex of G1 such that
A9: C = {e where e is Element of the_Edges_of G1 : e Joins v1,v2,G1} and
ex e0 being object st e0 Joins v1,v2,G1 and
for e0 being object st e0 Joins v1,v2,G1 holds not e0 in E2 by A6, A7;
e in C0 by A7, A8;
then consider e2 being Element of the_Edges_of G1 such that
A10: e = e2 & e2 Joins v1,v2,G1 by A8, A9;
thus e in the_Edges_of G1 by A10, GLIB_000:def 13;
end;
then A11: rng f c= the_Edges_of G1 by TARSKI:def 3;
the_Edges_of G2 c= the_Edges_of G1;
then E2 c= the_Edges_of G1 by XBOOLE_1:1;
then reconsider E1 = E2 \/ rng f as Subset of the_Edges_of G1
by A11, XBOOLE_1:8;
for v,w,e0 being object st e0 Joins v,w,G1
ex e being object st e Joins v,w,G1 & e in E1 &
for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds e9 = e
proof
let v,w,e0 be object;
A12: v is set & w is set by TARSKI:1;
assume A13: e0 Joins v,w,G1;
per cases;
suppose ex e1 being object st e1 Joins v,w,G1 & e1 in E2;
then consider e1 being object such that
A14: e1 Joins v,w,G1 & e1 in E2;
e1 Joins v,w,G2 by A12, A14, GLIB_000:73;
then consider e being object such that
A15: e Joins v,w,G2 & e in E2 and
A16: for e8 being object st e8 Joins v,w,G2 & e8 in E2 holds e8 = e
by Def5;
take e;
thus A17: e Joins v,w,G1 by A12, A15, GLIB_000:72;
thus e in E1 by A15, XBOOLE_0:def 3;
let e9 be object;
assume A18: e9 Joins v,w,G1 & e9 in E1;
not e9 in rng f
proof
assume e9 in rng f;
then consider C being object such that
A19: C in dom f & f.C = e9 by FUNCT_1:def 3;
consider v1,v2 being Vertex of G1 such that
A20: C = {k where k is Element of the_Edges_of G1 : k Joins v1,v2,G1}
and ex k0 being object st k0 Joins v1,v2,G1 and
A21: for k0 being object st k0 Joins v1,v2,G1 holds not k0 in E2
by A6, A19;
consider C0 being non empty set such that
A22: C = C0 & f.C = the Element of C0 by A6, A19;
e9 in C0 by A19, A22;
then consider k being Element of the_Edges_of G1 such that
A23: e9 = k & k Joins v1,v2,G1 by A20, A22;
v1 = v & v2 = w or v1 = w & v2 = v by A18, A23, GLIB_000:15;
hence contradiction by A15, A17, A21, GLIB_000:14;
end;
then A24: e9 in E2 by A18, XBOOLE_0:def 3;
then e9 Joins v,w,G2 by A12, A18, GLIB_000:73;
hence e9 = e by A16, A24;
end;
suppose A25: for e1 being object st e1 Joins v,w,G1 holds not e1 in E2;
A26: v is Vertex of G1 & w is Vertex of G1 by A13, GLIB_000:13;
set B = {e where e is Element of the_Edges_of G1 : e Joins v,w,G1};
A27: B in A by A13, A25, A26;
then consider B0 being non empty set such that
A28: B = B0 & f.B = the Element of B0 by A6;
f.B in B by A28;
then consider e being Element of the_Edges_of G1 such that
A29: f.B = e & e Joins v,w,G1;
take e;
thus e Joins v,w,G1 by A29;
e in rng f by A6, A27, A29, FUNCT_1:3;
hence e in E1 by XBOOLE_0:def 3;
let e9 be object;
assume A30: e9 Joins v,w,G1 & e9 in E1;
then not e9 in E2 by A25;
then e9 in rng f by A30, XBOOLE_0:def 3;
then consider C being object such that
A31: C in dom f & f.C = e9 by FUNCT_1:def 3;
consider v1,v2 being Vertex of G1 such that
A32: C = {k where k is Element of the_Edges_of G1 : k Joins v1,v2,G1}
and ex k0 being object st k0 Joins v1,v2,G1 and
for k0 being object st k0 Joins v1,v2,G1 holds not k0 in E2
by A6, A31;
consider C0 being non empty set such that
A33: C = C0 & f.C = the Element of C0 by A6, A31;
f.C in C0 by A33;
then consider k being Element of the_Edges_of G1 such that
A34: f.C = k & k Joins v1,v2,G1 by A32, A33;
for x being object holds x in B iff x in C0
proof
let x be object;
A35: v1 = v & v2 = w or v1 = w & v2 = v by A30, A31, A34, GLIB_000:15;
hereby
assume x in B;
then consider k being Element of the_Edges_of G1 such that
A36: x = k & k Joins v,w,G1;
k Joins v1,v2,G1 by A35, A36, GLIB_000:14;
hence x in C0 by A32, A33, A36;
end;
assume x in C0;
then consider k being Element of the_Edges_of G1 such that
A37: x = k & k Joins v1,v2,G1 by A32, A33;
k Joins v,w,G1 by A35, A37, GLIB_000:14;
hence x in B by A37;
end;
hence e9 = e by A29, A31, A33, TARSKI:2;
end;
end;
then reconsider E1 as RepEdgeSelection of G1 by Def5;
take E1;
for x being object holds x in E2 iff x in E1 & x in the_Edges_of G2
proof
let x be object;
thus x in E2 implies x in E1 & x in the_Edges_of G2
by TARSKI:def 3, XBOOLE_1:7;
assume A38: x in E1 & x in the_Edges_of G2;
not x in rng f
proof
assume x in rng f;
then consider C being object such that
A39: C in dom f & f.C = x by FUNCT_1:def 3;
consider v1,v2 being Vertex of G1 such that
A40: C = {e where e is Element of the_Edges_of G1 : e Joins v1,v2,G1}
and ex e0 being object st e0 Joins v1,v2,G1 and
A41: for e0 being object st e0 Joins v1,v2,G1 holds not e0 in E2
by A6, A39;
consider C0 being non empty set such that
A42: C = C0 & f.C = the Element of C0 by A6, A39;
f.C in C0 by A42;
then consider e being Element of the_Edges_of G1 such that
A43: f.C = e & e Joins v1,v2,G1 by A40, A42;
x Joins v1,v2,G2 by A38, A39, A43, GLIB_000:73;
then consider e1 being object such that
A44: e1 Joins v1,v2,G2 & e1 in E2 and
for e9 being object st e9 Joins v1,v2,G2 & e9 in E2 holds e9 = e1
by Def5;
thus contradiction by A41, A44, GLIB_000:72;
end;
hence thesis by A38, XBOOLE_0:def 3;
end;
hence thesis by XBOOLE_0:def 4;
end;
theorem Th81:
for G1 being _Graph, G2 being Subgraph of G1,E2 being RepDEdgeSelection of G2
ex E1 being RepDEdgeSelection of G1 st E2 = E1 /\ the_Edges_of G2
proof
let G1 be _Graph, G2 be Subgraph of G1, E2 be RepDEdgeSelection of G2;
set A = {{e where e is Element of the_Edges_of G1 : e DJoins v1,v2,G1}
where v1,v2 is Vertex of G1 : (ex e0 being object st e0 DJoins v1,v2,G1) &
(for e0 being object st e0 DJoins v1,v2,G1 holds not e0 in E2)};
defpred P[object,object] means ex S being non empty set
st $1 = S & $2 = the Element of S;
A1: for x,y1,y2 being object st x in A & P[x,y1] & P[x,y2] holds y1 = y2;
A2: for x being object st x in A ex y being object st P[x,y]
proof
let x be object;
assume x in A;
then consider v1,v2 being Vertex of G1 such that
A3: x = {e where e is Element of the_Edges_of G1 : e DJoins v1,v2,G1} and
A4: ex e0 being object st e0 DJoins v1,v2,G1 and
for e0 being object st e0 DJoins v1,v2,G1 holds not e0 in E2;
reconsider B = x as set by A3;
consider e0 being object such that
A5: e0 DJoins v1,v2,G1 by A4;
reconsider e0 as Element of the_Edges_of G1 by A5, GLIB_000:def 14;
e0 in B by A3, A5;
then reconsider B as non empty set;
take the Element of B, B;
thus thesis;
end;
consider f being Function such that
A6: dom f = A & for x being object st x in A holds P[x,f.x]
from FUNCT_1:sch 2(A1,A2);
for e being object holds e in rng f implies e in the_Edges_of G1
proof
let e be object;
assume e in rng f;
then consider C being object such that
A7: C in dom f & f.C = e by FUNCT_1:def 3;
consider C0 being non empty set such that
A8: C = C0 & f.C = the Element of C0 by A6, A7;
consider v1,v2 being Vertex of G1 such that
A9: C={e where e is Element of the_Edges_of G1 : e DJoins v1,v2,G1} and
ex e0 being object st e0 DJoins v1,v2,G1 and
for e0 being object st e0 DJoins v1,v2,G1 holds not e0 in E2 by A6, A7;
e in C0 by A7, A8;
then consider e2 being Element of the_Edges_of G1 such that
A10: e = e2 & e2 DJoins v1,v2,G1 by A8, A9;
thus e in the_Edges_of G1 by A10, GLIB_000:def 14;
end;
then A11: rng f c= the_Edges_of G1 by TARSKI:def 3;
the_Edges_of G2 c= the_Edges_of G1;
then E2 c= the_Edges_of G1 by XBOOLE_1:1;
then reconsider E1 = E2 \/ rng f as Subset of the_Edges_of G1
by A11, XBOOLE_1:8;
for v,w,e0 being object st e0 DJoins v,w,G1
ex e being object st e DJoins v,w,G1 & e in E1 &
for e9 being object st e9 DJoins v,w,G1 & e9 in E1 holds e9 = e
proof
let v,w,e0 be object;
A12: v is set & w is set by TARSKI:1;
assume A13: e0 DJoins v,w,G1;
per cases;
suppose ex e1 being object st e1 DJoins v,w,G1 & e1 in E2;
then consider e1 being object such that
A14: e1 DJoins v,w,G1 & e1 in E2;
e1 DJoins v,w,G2 by A12, A14, GLIB_000:73;
then consider e being object such that
A15: e DJoins v,w,G2 & e in E2 and
A16: for e8 being object st e8 DJoins v,w,G2 & e8 in E2 holds e8 = e
by Def6;
take e;
thus A17: e DJoins v,w,G1 by A12, A15, GLIB_000:72;
thus e in E1 by A15, XBOOLE_0:def 3;
let e9 be object;
assume A18: e9 DJoins v,w,G1 & e9 in E1;
not e9 in rng f
proof
assume e9 in rng f;
then consider C being object such that
A19: C in dom f & f.C = e9 by FUNCT_1:def 3;
consider v1,v2 being Vertex of G1 such that
A20: C ={k where k is Element of the_Edges_of G1 : k DJoins v1,v2,G1}
and ex k0 being object st k0 DJoins v1,v2,G1 and
A21: for k0 being object st k0 DJoins v1,v2,G1 holds not k0 in E2
by A6, A19;
consider C0 being non empty set such that
A22: C = C0 & f.C = the Element of C0 by A6, A19;
e9 in C0 by A19, A22;
then consider k being Element of the_Edges_of G1 such that
A23: e9 = k & k DJoins v1,v2,G1 by A20, A22;
v1 = v & v2 = w by A18, A23, GLIB_000:125;
hence contradiction by A15, A17, A21;
end;
then A24: e9 in E2 by A18, XBOOLE_0:def 3;
then e9 DJoins v,w,G2 by A12, A18, GLIB_000:73;
hence e9 = e by A16, A24;
end;
suppose A25: for e1 being object st e1 DJoins v,w,G1 holds not e1 in E2;
e0 Joins v,w,G1 by A13, GLIB_000:16;
then A26: v is Vertex of G1 & w is Vertex of G1 by GLIB_000:13;
set B = {e where e is Element of the_Edges_of G1 : e DJoins v,w,G1};
A27: B in A by A13, A25, A26;
then consider B0 being non empty set such that
A28: B = B0 & f.B = the Element of B0 by A6;
f.B in B by A28;
then consider e being Element of the_Edges_of G1 such that
A29: f.B = e & e DJoins v,w,G1;
take e;
thus e DJoins v,w,G1 by A29;
e in rng f by A6, A27, A29, FUNCT_1:3;
hence e in E1 by XBOOLE_0:def 3;
let e9 be object;
assume A30: e9 DJoins v,w,G1 & e9 in E1;
then not e9 in E2 by A25;
then e9 in rng f by A30, XBOOLE_0:def 3;
then consider C being object such that
A31: C in dom f & f.C = e9 by FUNCT_1:def 3;
consider v1,v2 being Vertex of G1 such that
A32: C = {k where k is Element of the_Edges_of G1 : k DJoins v1,v2,G1}
and ex k0 being object st k0 DJoins v1,v2,G1 and
for k0 being object st k0 DJoins v1,v2,G1 holds not k0 in E2
by A6, A31;
consider C0 being non empty set such that
A33: C = C0 & f.C = the Element of C0 by A6, A31;
f.C in C0 by A33;
then consider k being Element of the_Edges_of G1 such that
A34: f.C = k & k DJoins v1,v2,G1 by A32, A33;
for x being object holds x in B iff x in C0
proof
let x be object;
A35: v1 = v & v2 = w by A30, A31, A34, GLIB_000:125;
thus x in B implies x in C0 by A32, A33, A35;
assume x in C0;
then consider k being Element of the_Edges_of G1 such that
A36: x = k & k DJoins v1,v2,G1 by A32, A33;
thus x in B by A35, A36;
end;
hence e9 = e by A29, A31, A33, TARSKI:2;
end;
end;
then reconsider E1 as RepDEdgeSelection of G1 by Def6;
take E1;
for x being object holds x in E2 iff x in E1 & x in the_Edges_of G2
proof
let x be object;
thus x in E2 implies x in E1 & x in the_Edges_of G2
by TARSKI:def 3, XBOOLE_1:7;
assume A37: x in E1 & x in the_Edges_of G2;
not x in rng f
proof
assume x in rng f;
then consider C being object such that
A38: C in dom f & f.C = x by FUNCT_1:def 3;
consider v1,v2 being Vertex of G1 such that
A39: C = {e where e is Element of the_Edges_of G1 : e DJoins v1,v2,G1}
and ex e0 being object st e0 DJoins v1,v2,G1 and
A40: for e0 being object st e0 DJoins v1,v2,G1 holds not e0 in E2
by A6, A38;
consider C0 being non empty set such that
A41: C = C0 & f.C = the Element of C0 by A6, A38;
f.C in C0 by A41;
then consider e being Element of the_Edges_of G1 such that
A42: f.C = e & e DJoins v1,v2,G1 by A39, A41;
x DJoins v1,v2,G2 by A37, A38, A42, GLIB_000:73;
then consider e1 being object such that
A43: e1 DJoins v1,v2,G2 & e1 in E2 and
for e9 being object st e9 DJoins v1,v2,G2 & e9 in E2 holds e9 = e1
by Def6;
thus contradiction by A40, A43, GLIB_000:72;
end;
hence thesis by A37, XBOOLE_0:def 3;
end;
hence thesis by XBOOLE_0:def 4;
end;
theorem Th82:
for G1 being _Graph, E1 being RepEdgeSelection of G1
for G2 being inducedSubgraph of G1, the_Vertices_of G1, E1
for E2 being RepEdgeSelection of G2 holds E1 = E2
proof
let G1 be _Graph, E1 be RepEdgeSelection of G1;
let G2 be inducedSubgraph of G1, the_Vertices_of G1, E1;
let E2 be RepEdgeSelection of G2;
the_Edges_of G1 = G1.edgesBetween(the_Vertices_of G1) &
the_Vertices_of G1 c= the_Vertices_of G1 by GLIB_000:34;
then A1: the_Edges_of G2 = E1 by GLIB_000:def 37;
for e being object holds e in E1 implies e in E2
proof
let e be object;
assume A2: e in E1;
set v = (the_Source_of G2).e, w = (the_Target_of G2).e;
A3: e Joins v,w,G2 by A1, A2, GLIB_000:def 13;
then consider e2 being object such that
A4: e2 Joins v,w,G2 & e2 in E2 and
for e9 being object st e9 Joins v,w,G2 & e9 in E2 holds e9 = e2
by Def5;
A5: e Joins v,w,G1 by A3, GLIB_000:72;
then consider e1 being object such that
e1 Joins v,w,G1 & e1 in E1 and
A6: for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds e9 = e1
by Def5;
e = e1 by A2, A5, A6;
hence e in E2 by A1, A4, A6, GLIB_000:72;
end;
then E1 c= E2 by TARSKI:def 3;
hence thesis by A1, XBOOLE_0:def 10;
end;
theorem Th83:
for G1 being _Graph, E1 being RepDEdgeSelection of G1
for G2 being inducedSubgraph of G1, the_Vertices_of G1, E1
for E2 being RepDEdgeSelection of G2 holds E1 = E2
proof
let G1 be _Graph, E1 be RepDEdgeSelection of G1;
let G2 be inducedSubgraph of G1, the_Vertices_of G1, E1;
let E2 be RepDEdgeSelection of G2;
the_Edges_of G1 = G1.edgesBetween(the_Vertices_of G1) &
the_Vertices_of G1 c= the_Vertices_of G1 by GLIB_000:34;
then A1: the_Edges_of G2 = E1 by GLIB_000:def 37;
for e being object holds e in E1 implies e in E2
proof
let e be object;
assume A2: e in E1;
set v = (the_Source_of G2).e, w = (the_Target_of G2).e;
A3: e DJoins v,w,G2 by A1, A2, GLIB_000:def 14;
then consider e2 being object such that
A4: e2 DJoins v,w,G2 & e2 in E2 and
for e9 being object st e9 DJoins v,w,G2 & e9 in E2 holds e9 = e2
by Def6;
A5: e DJoins v,w,G1 by A3, GLIB_000:72;
then consider e1 being object such that
e1 DJoins v,w,G1 & e1 in E1 and
A6: for e9 being object st e9 DJoins v,w,G1 & e9 in E1 holds e9 = e1
by Def6;
e = e1 by A2, A5, A6;
hence e in E2 by A1, A4, A6, GLIB_000:72;
end;
then E1 c= E2 by TARSKI:def 3;
hence thesis by A1, XBOOLE_0:def 10;
end;
theorem Th84:
for G1 being _Graph, E1 being RepDEdgeSelection of G1
for G2 being inducedSubgraph of G1, the_Vertices_of G1, E1
for E2 being RepEdgeSelection of G2
holds E2 c= E1 & E2 is RepEdgeSelection of G1
proof
let G1 be _Graph, E1 be RepDEdgeSelection of G1;
let G2 be inducedSubgraph of G1, the_Vertices_of G1, E1;
let E2 be RepEdgeSelection of G2;
the_Vertices_of G1 c= the_Vertices_of G1 &
the_Edges_of G1 = G1.edgesBetween(the_Vertices_of G1) by GLIB_000:34;
then A1: the_Vertices_of G2 = the_Vertices_of G1 &
the_Edges_of G2 = E1 by GLIB_000:def 37;
hence E2 c= E1;
then A2: E2 c= the_Edges_of G1 by XBOOLE_1:1;
now
let v,w,e0 be object;
A3: v is set & w is set by TARSKI:1;
assume A4: e0 Joins v,w,G1;
ex e1 being object st e1 Joins v,w,G2
proof
per cases by A4, GLIB_000:16;
suppose e0 DJoins v,w,G1;
then consider e1 being object such that
A5: e1 DJoins v,w,G1 & e1 in E1 and
for e9 being object st e9 DJoins v,w,G1 & e9 in E1 holds e9 = e1
by Def6;
take e1;
e1 DJoins v,w,G2 by A1, A3, A5, GLIB_000:73;
hence e1 Joins v,w,G2 by GLIB_000:16;
end;
suppose e0 DJoins w,v,G1;
then consider e1 being object such that
A6: e1 DJoins w,v,G1 & e1 in E1 and
for e9 being object st e9 DJoins w,v,G1 & e9 in E1 holds e9 = e1
by Def6;
take e1;
e1 DJoins w,v,G2 by A3, A1, A6, GLIB_000:73;
hence e1 Joins v,w,G2 by GLIB_000:16;
end;
end;
then consider e1 being object such that
A7: e1 Joins v,w,G2;
consider e2 being object such that
A8: e2 Joins v,w,G2 & e2 in E2 and
A9: for e9 being object st e9 Joins v,w,G2 & e9 in E2 holds e9 = e2
by A7, Def5;
take e2;
thus e2 Joins v,w,G1 & e2 in E2 by A3, A8, GLIB_000:72;
let e9 be object;
assume A10: e9 Joins v,w,G1 & e9 in E2;
e9 Joins v,w,G2 by A3, A10, GLIB_000:73;
hence e9 = e2 by A9, A10;
end;
hence thesis by A2, Def5;
end;
theorem Th85:
for G being _Graph, E1, E2 being RepEdgeSelection of G
ex f being one-to-one Function st dom f = E1 & rng f = E2 &
for e,v,w being object st e in E1 holds e Joins v,w,G iff f.e Joins v,w,G
proof
let G be _Graph, E1, E2 be RepEdgeSelection of G;
defpred P[object,object] means $2 in E2 & ex v,w being object
st $1 Joins v,w,G & $2 Joins v,w,G;
A1: for x,y1,y2 being object st x in E1 & P[x,y1] & P[x,y2] holds y1 = y2
proof
let x,y1,y2 be object;
assume A2: x in E1 & P[x,y1] & P[x,y2];
then consider v1,w1 being object such that
A3: x Joins v1,w1,G & y1 Joins v1,w1,G;
consider v2,w2 being object such that
A4: x Joins v2,w2,G & y2 Joins v2,w2,G by A2;
consider e2 being object such that
e2 Joins v1,w1,G & e2 in E2 and
A5: for e9 being object st e9 Joins v1,w1,G & e9 in E2 holds e9 = e2
by A3, Def5;
A6: y1 = e2 by A2, A3, A5;
v1 = v2 & w1 = w2 or v1 = w2 & w1 = v2 by A3, A4, GLIB_000:15;
hence y1 = y2 by A2, A4, A5, A6, GLIB_000:14;
end;
A7: for x being object st x in E1 ex y being object st P[x,y]
proof
let x be object;
set v = (the_Source_of G).x, w = (the_Target_of G).x;
assume x in E1;
then A8: x Joins v,w,G by GLIB_000:def 13;
then consider e2 being object such that
A9: e2 Joins v,w,G & e2 in E2 and
for e9 being object st e9 Joins v,w,G & e9 in E2 holds e9 = e2 by Def5;
take e2;
thus e2 in E2 by A9;
take v,w;
thus thesis by A8, A9;
end;
consider f being Function such that
A10: dom f = E1 & for x being object st x in E1 holds P[x,f.x]
from FUNCT_1:sch 2(A1,A7);
now
let x1,x2 be object;
assume A11: x1 in dom f & x2 in dom f & f.x1 = f.x2;
then consider v1,w1 being object such that
A12: x1 Joins v1,w1,G & f.x1 Joins v1,w1,G by A10;
consider v2,w2 being object such that
A13: x2 Joins v2,w2,G & f.x2 Joins v2,w2,G by A10, A11;
consider e1 being object such that
e1 Joins v1,w1,G & e1 in E1 and
A14: for e9 being object st e9 Joins v1,w1,G & e9 in E1 holds e9 = e1
by A12, Def5;
A15: x1 = e1 by A10, A11, A12, A14;
v1 = v2 & w1 = w2 or v1 = w2 & w1 = v2 by A11, A12, A13, GLIB_000:15;
hence x1 = x2 by A10, A11, A13, A14, A15, GLIB_000:14;
end;
then reconsider f as one-to-one Function by FUNCT_1:def 4;
take f;
thus dom f = E1 by A10;
now
let y be object;
hereby
assume y in rng f;
then consider x being object such that
A16: x in dom f & f.x = y by FUNCT_1:def 3;
thus y in E2 by A10, A16;
end;
assume A17: y in E2;
set v = (the_Source_of G).y, w = (the_Target_of G).y;
A18: y Joins v,w,G by A17, GLIB_000:def 13;
then consider e1 being object such that
A19: e1 Joins v,w,G & e1 in E1 and
for e9 being object st e9 Joins v,w,G & e9 in E1 holds e9 = e1
by Def5;
consider e2 being object such that
e2 Joins v,w,G & e2 in E2 and
A20: for e9 being object st e9 Joins v,w,G & e9 in E2 holds e9 = e2
by A18, Def5;
consider v0,w0 being object such that
A21: e1 Joins v0,w0,G & f.e1 Joins v0,w0,G by A10, A19;
v0 = v & w0 = w or v0 = w & w0 = v by A19, A21, GLIB_000:15;
then f.e1 Joins v,w,G by A21, GLIB_000:14;
then A22: f.e1 = e2 by A10, A19, A20;
y = e2 by A17, A18, A20;
hence y in rng f by A10, A19, A22, FUNCT_1:3;
end;
hence rng f = E2 by TARSKI:2;
let e,v,w be object;
assume e in E1;
then consider v0,w0 being object such that
A23: e Joins v0,w0,G & f.e Joins v0,w0,G by A10;
hereby
assume e Joins v,w,G;
then v0 = v & w0 = w or v0 = w & w0 = v by A23, GLIB_000:15;
hence f.e Joins v,w,G by A23, GLIB_000:14;
end;
assume f.e Joins v,w,G;
then v0 = v & w0 = w or v0 = w & w0 = v by A23, GLIB_000:15;
hence e Joins v,w,G by A23, GLIB_000:14;
end;
theorem
for G being _Graph, E1, E2 being RepEdgeSelection of G
holds card E1 = card E2
proof
let G be _Graph, E1, E2 be RepEdgeSelection of G;
consider f being one-to-one Function such that
A1: dom f = E1 & rng f = E2 and
for e,v,w being object st e in E1 holds e Joins v,w,G iff f.e Joins v,w,G
by Th85;
thus thesis by A1, WELLORD2:def 4, CARD_1:5;
end;
theorem Th87:
for G being _Graph, E1, E2 being RepDEdgeSelection of G
ex f being one-to-one Function st dom f = E1 & rng f = E2 &
for e,v,w being object st e in E1 holds e DJoins v,w,G iff f.e DJoins v,w,G
proof
let G be _Graph, E1, E2 be RepDEdgeSelection of G;
defpred P[object,object] means $2 in E2 & ex v,w being object
st $1 DJoins v,w,G & $2 DJoins v,w,G;
A1: for x,y1,y2 being object st x in E1 & P[x,y1] & P[x,y2] holds y1 = y2
proof
let x,y1,y2 be object;
assume A2: x in E1 & P[x,y1] & P[x,y2];
then consider v1,w1 being object such that
A3: x DJoins v1,w1,G & y1 DJoins v1,w1,G;
consider v2,w2 being object such that
A4: x DJoins v2,w2,G & y2 DJoins v2,w2,G by A2;
consider e2 being object such that
e2 DJoins v1,w1,G & e2 in E2 and
A5: for e9 being object st e9 DJoins v1,w1,G & e9 in E2 holds e9 = e2
by A3, Def6;
A6: y1 = e2 by A2, A3, A5;
v1 = v2 & w1 = w2 by A3, A4, GLIB_000:125;
hence y1 = y2 by A2, A4, A5, A6;
end;
A7: for x being object st x in E1 ex y being object st P[x,y]
proof
let x be object;
set v = (the_Source_of G).x, w = (the_Target_of G).x;
assume A8: x in E1;
then consider e2 being object such that
A9: e2 DJoins v,w,G & e2 in E2 and
for e9 being object st e9 DJoins v,w,G & e9 in E2 holds e9 = e2
by Def6, GLIB_000:def 14;
take e2;
thus e2 in E2 by A9;
take v,w;
thus thesis by A8, A9, GLIB_000:def 14;
end;
consider f being Function such that
A10: dom f = E1 & for x being object st x in E1 holds P[x,f.x]
from FUNCT_1:sch 2(A1,A7);
now
let x1,x2 be object;
assume A11: x1 in dom f & x2 in dom f & f.x1 = f.x2;
then consider v1,w1 being object such that
A12: x1 DJoins v1,w1,G & f.x1 DJoins v1,w1,G by A10;
consider v2,w2 being object such that
A13: x2 DJoins v2,w2,G & f.x2 DJoins v2,w2,G by A10, A11;
consider e1 being object such that
e1 DJoins v1,w1,G & e1 in E1 and
A14: for e9 being object st e9 DJoins v1,w1,G & e9 in E1 holds e9 = e1
by A12, Def6;
A15: x1 = e1 by A10, A11, A12, A14;
v1 = v2 & w1 = w2 by A11, A12, A13, GLIB_000:125;
hence x1 = x2 by A10, A11, A13, A14, A15;
end;
then reconsider f as one-to-one Function by FUNCT_1:def 4;
take f;
thus dom f = E1 by A10;
now
let y be object;
hereby
assume y in rng f;
then consider x being object such that
A16: x in dom f & f.x = y by FUNCT_1:def 3;
thus y in E2 by A10, A16;
end;
assume A17: y in E2;
set v = (the_Source_of G).y, w = (the_Target_of G).y;
consider e1 being object such that
A18: e1 DJoins v,w,G & e1 in E1 and
for e9 being object st e9 DJoins v,w,G & e9 in E1 holds e9 = e1
by A17, Def6, GLIB_000:def 14;
consider e2 being object such that
e2 DJoins v,w,G & e2 in E2 and
A19: for e9 being object st e9 DJoins v,w,G & e9 in E2 holds e9 = e2
by A17, Def6, GLIB_000:def 14;
consider v0,w0 being object such that
A20: e1 DJoins v0,w0,G & f.e1 DJoins v0,w0,G by A10, A18;
v0 = v & w0 = w by A18, A20, GLIB_000:125;
then A21: f.e1 = e2 by A10, A18, A19, A20;
y DJoins v,w,G by A17, GLIB_000:def 14;
then y = e2 by A17, A19;
hence y in rng f by A10, A18, A21, FUNCT_1:3;
end;
hence rng f = E2 by TARSKI:2;
let e,v,w be object;
assume e in E1;
then consider v0,w0 being object such that
A22: e DJoins v0,w0,G & f.e DJoins v0,w0,G by A10;
hereby
assume e DJoins v,w,G;
then v0 = v & w0 = w by A22, GLIB_000:125;
hence f.e DJoins v,w,G by A22;
end;
assume f.e DJoins v,w,G;
then v0 = v & w0 = w by A22, GLIB_000:125;
hence e DJoins v,w,G by A22;
end;
theorem
for G being _Graph, E1, E2 being RepDEdgeSelection of G
holds card E1 = card E2
proof
let G be _Graph, E1, E2 be RepDEdgeSelection of G;
consider f being one-to-one Function such that
A1: dom f = E1 & rng f = E2 and
for e,v,w being object st e in E1 holds e DJoins v,w,G iff f.e DJoins v,w,G
by Th87;
thus thesis by A1, WELLORD2:def 4, CARD_1:5;
end;
definition
let G be _Graph;
mode removeParallelEdges of G -> Subgraph of G means
:Def7:
ex E being RepEdgeSelection of G
st it is inducedSubgraph of G, the_Vertices_of G, E;
existence
proof
set E = the RepEdgeSelection of G;
set G2 = the inducedSubgraph of G, the_Vertices_of G, E;
take G2, E;
thus thesis;
end;
mode removeDParallelEdges of G -> Subgraph of G means
:Def8:
ex E being RepDEdgeSelection of G
st it is inducedSubgraph of G, the_Vertices_of G, E;
existence
proof
set E = the RepDEdgeSelection of G;
set G2 = the inducedSubgraph of G, the_Vertices_of G, E;
take G2, E;
thus thesis;
end;
end;
registration
let G be _Graph;
cluster -> spanning non-multi for removeParallelEdges of G;
coherence
proof
let G2 be removeParallelEdges of G;
consider E being RepEdgeSelection of G such that
A1: G2 is inducedSubgraph of G, the_Vertices_of G, E by Def7;
set E2 = the RepEdgeSelection of G2;
E c= the_Edges_of G;
then A2: E c= G.edgesBetween(the_Vertices_of G) by GLIB_000:34;
the_Vertices_of G c= the_Vertices_of G;
then the_Edges_of G2 = E by A1, A2, GLIB_000:def 37;
then the_Edges_of G2 = E2 by A1, Th82;
hence thesis by A1, Th75;
end;
cluster -> spanning non-Dmulti for removeDParallelEdges of G;
coherence
proof
let G2 be removeDParallelEdges of G;
consider E being RepDEdgeSelection of G such that
A3: G2 is inducedSubgraph of G, the_Vertices_of G, E by Def8;
set E2 = the RepDEdgeSelection of G2;
E c= the_Edges_of G;
then A4: E c= G.edgesBetween(the_Vertices_of G) by GLIB_000:34;
the_Vertices_of G c= the_Vertices_of G;
then the_Edges_of G2 = E by A3, A4, GLIB_000:def 37;
then the_Edges_of G2 = E2 by A3, Th83;
hence thesis by A3, Th77;
end;
cluster plain for removeParallelEdges of G;
existence
proof
set E = the RepEdgeSelection of G;
reconsider G2 = the plain inducedSubgraph of G, the_Vertices_of G, E
as removeParallelEdges of G by Def7;
take G2;
thus thesis;
end;
cluster plain for removeDParallelEdges of G;
existence
proof
set E = the RepDEdgeSelection of G;
reconsider G2 = the plain inducedSubgraph of G, the_Vertices_of G, E
as removeDParallelEdges of G by Def8;
take G2;
thus thesis;
end;
end;
registration
let G be loopless _Graph;
cluster -> simple for removeParallelEdges of G;
coherence;
cluster -> Dsimple for removeDParallelEdges of G;
coherence;
end;
theorem
for G1 being non-multi _Graph, G2 being _Graph
holds G1 == G2 iff G2 is removeParallelEdges of G1
proof
let G1 be non-multi _Graph, G2 be _Graph;
hereby
assume A1: G1 == G2;
set E = the RepEdgeSelection of G1;
G1 is inducedSubgraph of G1, the_Vertices_of G1 by GLIB_000:100;
then G1 is inducedSubgraph of G1, the_Vertices_of G1, the_Edges_of G1
by GLIB_000:34;
then G2 is inducedSubgraph of G1, the_Vertices_of G1, the_Edges_of G1
by A1, GLIB_000:101;
then G2 is inducedSubgraph of G1, the_Vertices_of G1, E by Th74;
hence G2 is removeParallelEdges of G1 by Def7;
end;
assume G2 is removeParallelEdges of G1;
then consider E being RepEdgeSelection of G1 such that
A2: G2 is inducedSubgraph of G1, the_Vertices_of G1, E by Def7;
G2 is inducedSubgraph of G1, the_Vertices_of G1, the_Edges_of G1
by A2, Th74;
then A3: G2 is inducedSubgraph of G1, the_Vertices_of G1 by GLIB_000:34;
G1 is inducedSubgraph of G1, the_Vertices_of G1 by GLIB_000:100;
hence G1 == G2 by A3, GLIB_000:93;
end;
theorem
for G1 being non-Dmulti _Graph, G2 being _Graph
holds G1 == G2 iff G2 is removeDParallelEdges of G1
proof
let G1 be non-Dmulti _Graph, G2 be _Graph;
hereby
assume A1: G1 == G2;
set E = the RepDEdgeSelection of G1;
G1 is inducedSubgraph of G1, the_Vertices_of G1 by GLIB_000:100;
then G1 is inducedSubgraph of G1, the_Vertices_of G1, the_Edges_of G1
by GLIB_000:34;
then G2 is inducedSubgraph of G1, the_Vertices_of G1, the_Edges_of G1
by A1, GLIB_000:101;
then G2 is inducedSubgraph of G1, the_Vertices_of G1, E by Th76;
hence G2 is removeDParallelEdges of G1 by Def8;
end;
assume G2 is removeDParallelEdges of G1;
then consider E being RepDEdgeSelection of G1 such that
A2: G2 is inducedSubgraph of G1, the_Vertices_of G1, E by Def8;
G2 is inducedSubgraph of G1, the_Vertices_of G1, the_Edges_of G1
by A2, Th76;
then A3: G2 is inducedSubgraph of G1, the_Vertices_of G1 by GLIB_000:34;
G1 is inducedSubgraph of G1, the_Vertices_of G1 by GLIB_000:100;
hence G1 == G2 by A3, GLIB_000:93;
end;
theorem Th91:
for G1, G2 being _Graph, G3 being removeParallelEdges of G1
st G1 == G2 holds G3 is removeParallelEdges of G2
proof
let G1, G2 be _Graph, G3 be removeParallelEdges of G1;
consider E being RepEdgeSelection of G1 such that
A1: G3 is inducedSubgraph of G1, the_Vertices_of G1, E by Def7;
assume A2: G1 == G2;
then A3: the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 by GLIB_000:def 34;
then A4: G3 is inducedSubgraph of G2, the_Vertices_of G2, E
by A1, A2, GLIB_000:95;
G2 is Subgraph of G1 by A2, GLIB_000:87;
then E is RepEdgeSelection of G2 by A3, Th78;
hence thesis by A4, Def7;
end;
theorem
for G1, G2 being _Graph, G3 being removeDParallelEdges of G1
st G1 == G2 holds G3 is removeDParallelEdges of G2
proof
let G1, G2 be _Graph, G3 be removeDParallelEdges of G1;
consider E being RepDEdgeSelection of G1 such that
A1: G3 is inducedSubgraph of G1, the_Vertices_of G1, E by Def8;
assume A2: G1 == G2;
then A3: the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 by GLIB_000:def 34;
then A4: G3 is inducedSubgraph of G2, the_Vertices_of G2, E
by A1, A2, GLIB_000:95;
G2 is Subgraph of G1 by A2, GLIB_000:87;
then E is RepDEdgeSelection of G2 by A3, Th79;
hence thesis by A4, Def8;
end;
theorem Th93:
for G1, G2 being _Graph, G3 being removeParallelEdges of G1
st G2 == G3 holds G2 is removeParallelEdges of G1
proof
let G1, G2 be _Graph, G3 be removeParallelEdges of G1;
consider E being RepEdgeSelection of G1 such that
A1: G3 is inducedSubgraph of G1, the_Vertices_of G1, E by Def7;
assume G2 == G3;
then G2 is inducedSubgraph of G1, the_Vertices_of G1, E by A1, GLIB_000:101;
hence thesis by Def7;
end;
theorem
for G1, G2 being _Graph, G3 being removeDParallelEdges of G1
st G2 == G3 holds G2 is removeDParallelEdges of G1
proof
let G1, G2 be _Graph, G3 be removeDParallelEdges of G1;
consider E being RepDEdgeSelection of G1 such that
A1: G3 is inducedSubgraph of G1, the_Vertices_of G1, E by Def8;
assume G2 == G3;
then G2 is inducedSubgraph of G1, the_Vertices_of G1, E by A1, GLIB_000:101;
hence thesis by Def8;
end;
theorem Th95:
for G1 being _Graph, G2 being removeDParallelEdges of G1
for G3 being removeParallelEdges of G2
holds G3 is removeParallelEdges of G1
proof
let G1 be _Graph, G2 be removeDParallelEdges of G1;
let G3 be removeParallelEdges of G2;
A1: G3 is Subgraph of G1 by GLIB_000:43;
consider E1 being RepDEdgeSelection of G1 such that
A2: G2 is inducedSubgraph of G1, the_Vertices_of G1, E1 by Def8;
A3: the_Vertices_of G1 c= the_Vertices_of G1 &
the_Edges_of G1 = G1.edgesBetween(the_Vertices_of G1) by GLIB_000:34;
then A4: the_Vertices_of G2 = the_Vertices_of G1 &
the_Edges_of G2 = E1 by A2, GLIB_000:def 37;
consider E2 being RepEdgeSelection of G2 such that
A5: G3 is inducedSubgraph of G2, the_Vertices_of G2, E2 by Def7;
the_Vertices_of G2 c= the_Vertices_of G2 &
the_Edges_of G2 = G2.edgesBetween(the_Vertices_of G2) by GLIB_000:34;
then A6: the_Vertices_of G3 = the_Vertices_of G2 &
the_Edges_of G3 = E2 by A5, GLIB_000:def 37;
E2 c= the_Edges_of G1 by A1, A6, GLIB_000:def 32;
then A7: G3 is inducedSubgraph of G1, the_Vertices_of G1, E2
by A1, A3, A4, A6, GLIB_000:def 37;
E2 is RepEdgeSelection of G1 by A2, Th84;
hence thesis by A7, Def7;
end;
theorem Th96:
for G1 being _Graph, G2 being removeDParallelEdges of G1
ex G3 being removeParallelEdges of G1
st G3 is removeParallelEdges of G2
proof
let G1 be _Graph, G2 be removeDParallelEdges of G1;
consider E1 being RepDEdgeSelection of G1 such that
A1: G2 is inducedSubgraph of G1, the_Vertices_of G1, E1 by Def8;
consider E2 being RepEdgeSelection of G1 such that
A2: E2 c= E1 by Th72;
set G3 = the inducedSubgraph of G1, the_Vertices_of G1, E2;
reconsider G3 as removeParallelEdges of G1 by Def7;
take G3;
A3: the_Vertices_of G1 c= the_Vertices_of G1 &
the_Edges_of G1 = G1.edgesBetween(the_Vertices_of G1) by GLIB_000:34;
then A4: G3 is Subgraph of G2 by A1, A2, GLIB_000:46;
A5: the_Vertices_of G2 c= the_Vertices_of G2 &
the_Edges_of G2 = G2.edgesBetween(the_Vertices_of G2) by GLIB_000:34;
the_Vertices_of G2 = the_Vertices_of G1 by A1, A3, GLIB_000:def 37;
then A6: the_Vertices_of G3 = the_Vertices_of G2 by A3, GLIB_000:def 37;
A7: E2 c= the_Edges_of G2 by A1, A2, A3, GLIB_000:def 37;
the_Edges_of G3 = E2 by A3, GLIB_000:def 37;
then A8: G3 is inducedSubgraph of G2, the_Vertices_of G2, E2
by A4, A5, A6, A7, GLIB_000:def 37;
E2 is RepEdgeSelection of G2 by A7, Th78;
hence thesis by A8, Def7;
end;
theorem Th97:
for G1 being _Graph, G3 being removeParallelEdges of G1
ex G2 being removeDParallelEdges of G1
st G3 is removeParallelEdges of G2
proof
let G1 be _Graph, G3 be removeParallelEdges of G1;
consider E2 being RepEdgeSelection of G1 such that
A1: G3 is inducedSubgraph of G1, the_Vertices_of G1, E2 by Def7;
consider E1 being RepDEdgeSelection of G1 such that
A2: E2 c= E1 by Th73;
set G2 = the inducedSubgraph of G1, the_Vertices_of G1, E1;
reconsider G2 as removeDParallelEdges of G1 by Def8;
take G2;
A3: the_Vertices_of G1 c= the_Vertices_of G1 &
the_Edges_of G1 = G1.edgesBetween(the_Vertices_of G1) by GLIB_000:34;
then A4: G3 is Subgraph of G2 by A1, A2, GLIB_000:46;
A5: the_Vertices_of G2 c= the_Vertices_of G2 &
the_Edges_of G2 = G2.edgesBetween(the_Vertices_of G2) by GLIB_000:34;
the_Vertices_of G3 = the_Vertices_of G1 by A1, A3, GLIB_000:def 37;
then A6: the_Vertices_of G3 = the_Vertices_of G2 by A3, GLIB_000:def 37;
A7: E2 c= the_Edges_of G2 by A2, A3, GLIB_000:def 37;
the_Edges_of G3 = E2 by A1, A3, GLIB_000:def 37;
then A8: G3 is inducedSubgraph of G2, the_Vertices_of G2, E2
by A4, A5, A6, A7, GLIB_000:def 37;
E2 is RepEdgeSelection of G2 by A7, Th78;
hence thesis by A8, Def7;
end;
registration
let G be complete _Graph;
cluster -> complete for removeParallelEdges of G;
coherence
proof
let G2 be removeParallelEdges of G;
consider E being RepEdgeSelection of G such that
A1: G2 is inducedSubgraph of G, the_Vertices_of G, E by Def7;
the_Vertices_of G c= the_Vertices_of G &
the_Edges_of G = G.edgesBetween(the_Vertices_of G) by GLIB_000:34;
then A2: the_Vertices_of G2 = the_Vertices_of G & the_Edges_of G2 = E
by A1, GLIB_000:def 37;
now
let v2,w2 be Vertex of G2;
assume A3: v2 <> w2;
reconsider v1 = v2, w1 = w2 as Vertex of G by A2;
consider e0 being object such that
A4: e0 Joins v1,w1,G by A3, CHORD:def 6, CHORD:def 3;
consider e being object such that
A5: e Joins v1,w1,G & e in E and
for e9 being object st e9 Joins v1,w1,G & e9 in E holds e9 = e
by A4, Def5;
e Joins v2,w2,G2 by A2, A5, GLIB_000:73;
hence v2,w2 are_adjacent by CHORD:def 3;
end;
hence thesis by CHORD:def 6;
end;
cluster -> complete for removeDParallelEdges of G;
coherence
proof
let G2 be removeDParallelEdges of G;
consider E being RepDEdgeSelection of G such that
A6: G2 is inducedSubgraph of G, the_Vertices_of G, E by Def8;
the_Vertices_of G c= the_Vertices_of G &
the_Edges_of G = G.edgesBetween(the_Vertices_of G) by GLIB_000:34;
then A7: the_Vertices_of G2 = the_Vertices_of G & the_Edges_of G2 = E
by A6, GLIB_000:def 37;
now
let v2,w2 be Vertex of G2;
assume A8: v2 <> w2;
reconsider v1 = v2, w1 = w2 as Vertex of G by A7;
consider e0 being object such that
A9: e0 Joins v1,w1,G by A8, CHORD:def 6, CHORD:def 3;
per cases by A9, GLIB_000:16;
suppose e0 DJoins v1,w1,G;
then consider e being object such that
A10: e DJoins v1,w1,G & e in E and
for e9 being object st e9 DJoins v1,w1,G & e9 in E holds e9 = e
by Def6;
e DJoins v2,w2,G2 by A7, A10, GLIB_000:73;
then e Joins v2,w2,G2 by GLIB_000:16;
hence v2,w2 are_adjacent by CHORD:def 3;
end;
suppose e0 DJoins w1,v1,G;
then consider e being object such that
A11: e DJoins w1,v1,G & e in E and
for e9 being object st e9 DJoins w1,v1,G & e9 in E holds e9 = e
by Def6;
e DJoins w2,v2,G2 by A7, A11, GLIB_000:73;
then e Joins v2,w2,G2 by GLIB_000:16;
hence v2,w2 are_adjacent by CHORD:def 3;
end;
end;
hence thesis by CHORD:def 6;
end;
end;
theorem Th98:
for G1 being _Graph, G2 being removeParallelEdges of G1, W1 being Walk of G1
ex W2 being Walk of G2 st W1.vertexSeq() = W2.vertexSeq()
proof
let G1 be _Graph, G2 be removeParallelEdges of G1;
defpred P[Walk of G1] means ex W2 being Walk of G2
st $1.vertexSeq() = W2.vertexSeq();
A1: for W being trivial Walk of G1 holds P[W]
proof
let W be trivial Walk of G1;
consider v1 being Vertex of G1 such that
A2: W = G1.walkOf(v1) by GLIB_001:128;
reconsider v2 = v1 as Vertex of G2 by GLIB_000:def 33;
set W2 = G2.walkOf(v2);
take W2;
thus W.vertexSeq() = <* v1 *> by A2, GLIB_001:69
.= W2.vertexSeq() by GLIB_001:69;
end;
A3: for W being Walk of G1, e being object st e in W.last().edgesInOut() &
P[W] holds P[W.addEdge(e)]
proof
let W1 be Walk of G1, e0 be object;
assume A4: e0 in W1.last().edgesInOut() & P[W1];
then consider W2 being Walk of G2 such that
A5: W1.vertexSeq() = W2.vertexSeq();
A6: W2.first() = W1.first() & W2.last() = W1.last() by A5, Th30;
consider E being RepEdgeSelection of G1 such that
A7: G2 is inducedSubgraph of G1, the_Vertices_of G1, E by Def7;
the_Vertices_of G1 c= the_Vertices_of G1 &
the_Edges_of G1 = G1.edgesBetween(the_Vertices_of G1) by GLIB_000:34;
then A8: the_Edges_of G2 = E by A7, GLIB_000:def 37;
per cases by A4, GLIB_000:61;
suppose A9: (the_Source_of G1).e0 = W1.last();
set v = W1.last(), w = (the_Target_of G1).e0;
A10: e0 Joins v,w,G1 by A4, A9, GLIB_000:def 13;
then consider e being object such that
A11: e Joins v,w,G1 & e in E and
for e9 being object st e9 Joins v,w,G1 & e9 in E holds e9 = e
by Def5;
set W3 = W1.addEdge(e0), W4 = W2.addEdge(e);
take W4;
A12: e Joins W2.last(),w,G2 by A8, A6, A11, GLIB_000:73;
A13: e is set & e0 is set by TARSKI:1;
thus W3.vertexSeq() = W1.vertexSeq() ^ <* w *> by A10, A13, GLIB_001:75
.= W4.vertexSeq() by A5, A12, A13, GLIB_001:75;
end;
suppose A14: (the_Target_of G1).e0 = W1.last();
set v = W1.last(), w = (the_Source_of G1).e0;
A15: e0 Joins v,w,G1 by A4, A14, GLIB_000:def 13;
then consider e being object such that
A16: e Joins v,w,G1 & e in E and
for e9 being object st e9 Joins v,w,G1 & e9 in E holds e9 = e
by Def5;
set W3 = W1.addEdge(e0), W4 = W2.addEdge(e);
take W4;
A17: e Joins W2.last(),w,G2 by A8, A6, A16, GLIB_000:73;
A18: e is set & e0 is set by TARSKI:1;
thus W3.vertexSeq() = W1.vertexSeq() ^ <* w *> by A15, A18, GLIB_001:75
.= W4.vertexSeq() by A5, A17, A18, GLIB_001:75;
end;
end;
for W1 being Walk of G1 holds P[W1] from IndWalk(A1,A3);
hence thesis;
end;
Lm4:
for G1 being _Graph, G2 being removeParallelEdges of G1, W1 being Walk of G1
ex W2 being Walk of G2 st W2 is_Walk_from W1.first(),W1.last()
proof
let G1 be _Graph, G2 be removeParallelEdges of G1, W1 be Walk of G1;
consider W2 being Walk of G2 such that
A1: W1.vertexSeq() = W2.vertexSeq() by Th98;
take W2;
thus thesis by A1, Th30;
end;
theorem Th99:
for G1 being _Graph, G2 being removeDParallelEdges of G1, W1 being Walk of G1
ex W2 being Walk of G2 st W1.vertexSeq() = W2.vertexSeq()
proof
let G1 be _Graph, G2 be removeDParallelEdges of G1;
let W1 be Walk of G1;
set G3 = the removeParallelEdges of G2;
G3 is removeParallelEdges of G1 by Th95;
then consider W3 being Walk of G3 such that
A1: W1.vertexSeq() = W3.vertexSeq() by Th98;
reconsider W2 = W3 as Walk of G2 by GLIB_001:167;
take W2;
thus thesis by A1, GLIB_001:76;
end;
Lm5:
for G1 being _Graph, G2 being removeDParallelEdges of G1, W1 being Walk of G1
ex W2 being Walk of G2 st W2 is_Walk_from W1.first(),W1.last()
proof
let G1 be _Graph, G2 be removeDParallelEdges of G1, W1 be Walk of G1;
consider W2 being Walk of G2 such that
A1: W1.vertexSeq() = W2.vertexSeq() by Th99;
take W2;
thus thesis by A1, Th30;
end;
theorem Th100:
for G1 being _Graph, G2 being removeParallelEdges of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2)
proof
let G1 be _Graph, G2 be removeParallelEdges of G1;
for W1 being Walk of G1 ex W2 being Walk of G2
st W2 is_Walk_from W1.first(),W1.last() by Lm4;
hence for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2) by Th35;
end;
theorem Th101:
for G1 being _Graph, G2 being removeDParallelEdges of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2)
proof
let G1 be _Graph, G2 be removeDParallelEdges of G1;
for W1 being Walk of G1 ex W2 being Walk of G2
st W2 is_Walk_from W1.first(),W1.last() by Lm5;
hence for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2) by Th35;
end;
registration
let G be connected _Graph;
cluster -> connected for removeParallelEdges of G;
coherence
proof
let G2 be removeParallelEdges of G;
for W1 being Walk of G ex W2 being Walk of G2
st W2 is_Walk_from W1.first(),W1.last() by Lm4;
hence thesis by Th36;
end;
cluster -> connected for removeDParallelEdges of G;
coherence
proof
let G2 be removeDParallelEdges of G;
for W1 being Walk of G ex W2 being Walk of G2
st W2 is_Walk_from W1.first(),W1.last() by Lm5;
hence thesis by Th36;
end;
end;
registration
let G be non connected _Graph;
cluster -> non connected for removeParallelEdges of G;
coherence
proof
let G2 be removeParallelEdges of G;
consider E being RepEdgeSelection of G such that
A1: G2 is inducedSubgraph of G, the_Vertices_of G, E by Def7;
thus thesis by A1, Th33;
end;
cluster -> non connected for removeDParallelEdges of G;
coherence
proof
let G2 be removeDParallelEdges of G;
consider E being RepDEdgeSelection of G such that
A2: G2 is inducedSubgraph of G, the_Vertices_of G, E by Def8;
thus thesis by A2, Th33;
end;
end;
theorem
for G1 being _Graph, G2 being removeParallelEdges of G1
holds G1.componentSet() = G2.componentSet()
proof
let G1 be _Graph, G2 be removeParallelEdges of G1;
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2) by Th100;
hence thesis by Th37;
end;
theorem
for G1 being _Graph, G2 being removeDParallelEdges of G1
holds G1.componentSet() = G2.componentSet()
proof
let G1 be _Graph, G2 be removeDParallelEdges of G1;
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2) by Th101;
hence thesis by Th37;
end;
theorem Th104:
for G1 being _Graph, G2 being removeParallelEdges of G1
holds G1.numComponents() = G2.numComponents()
proof
let G1 be _Graph, G2 be removeParallelEdges of G1;
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2) by Th100;
hence thesis by Th38;
end;
theorem
for G1 being _Graph, G2 being removeDParallelEdges of G1
holds G1.numComponents() = G2.numComponents()
proof
let G1 be _Graph, G2 be removeDParallelEdges of G1;
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2) by Th101;
hence thesis by Th38;
end;
theorem Th106:
for G1 being _Graph, G2 being removeParallelEdges of G1
holds G1 is chordal iff G2 is chordal
proof
let G1 be _Graph, G2 be removeParallelEdges of G1;
consider E being RepEdgeSelection of G1 such that
A1: G2 is inducedSubgraph of G1, the_Vertices_of G1, E by Def7;
the_Vertices_of G1 c= the_Vertices_of G1 &
the_Edges_of G1 = G1.edgesBetween(the_Vertices_of G1) by GLIB_000:34;
then A2: the_Edges_of G2 = E by A1, GLIB_000:def 37;
hereby
assume A3: G1 is chordal;
now
let P2 be Walk of G2;
assume A4: P2.length() > 3 & P2 is Cycle-like;
now
reconsider P1 = P2 as Walk of G1 by GLIB_001:167;
P1.length() > 3 & P1 is Cycle-like by A4, GLIB_001:114, GLIB_006:24;
then consider m,n being odd Nat such that
A5: m+2 < n & n <= len P1 & P1.m <> P1.n and
A6: ex e being object st e Joins P1.m,P1.n,G1 and
A7: for f being object st f in P1.edges()
holds not f Joins P1.m,P1.n,G1 by A3, CHORD:def 11, CHORD:def 10;
take m,n;
thus m+2 < n & n <= len P2 & P2.m <> P2.n by A5;
hereby
consider e0 being object such that
A8: e0 Joins P1.m,P1.n,G1 by A6;
consider e being object such that
A9: e Joins P1.m,P1.n,G1 & e in E and
for e9 being object st e9 Joins P1.m,P1.n,G1 & e9 in E holds e9 = e
by A8, Def5;
take e;
thus e Joins P2.m,P2.n,G2 by A2, A9, GLIB_000:73;
end;
let f be object;
assume f in P2.edges();
then f in P1.edges() by GLIB_001:110;
hence not f Joins P2.m,P2.n,G2 by A7, GLIB_000:72;
end;
hence P2 is chordal by CHORD:def 10;
end;
hence G2 is chordal by CHORD:def 11;
end;
assume A10: G2 is chordal;
now
let P1 be Walk of G1;
assume A11: P1.length() > 3 & P1 is Cycle-like;
A12: len P1 <> 5
proof
assume len P1 = 5;
then 2*P1.length()+1 = 2*2+1 by GLIB_001:112;
hence contradiction by A11;
end;
now
consider P2 being Walk of G2 such that
A13: P1.vertexSeq() = P2.vertexSeq() by Th98;
A14: P1.length() = P2.length() & P2 is Cycle-like
by A11, A12, A13, Th30, Th32;
then consider m,n being odd Nat such that
A15: m+2 < n & n <= len P2 & P2.m <> P2.n and
A16: ex e being object st e Joins P2.m,P2.n,G2 and
A17: for f being object st f in P2.edges()
holds not f Joins P2.m,P2.n,G2 by A10, A11, CHORD:def 11, def 10;
take m,n;
A18: len P1 = 2*P1.length()+1 by GLIB_001:112
.= len P2 by A14, GLIB_001:112;
hence m+2 < n & n <= len P1 by A15;
A19: P1.n = P2.n & P1.m = P2.m by A13, Th29;
hence P1.m <> P1.n by A15;
thus ex e being object st e Joins P1.m,P1.n,G1 by A16, A19, GLIB_000:72;
let f be object;
assume f in P1.edges();
then consider k being odd Element of NAT such that
A20: k < len P1 & P1.(k+1) = f by GLIB_001:100;
A21: f Joins P1.k,P1.(k+2),G1 by A20, GLIB_001:def 3;
assume A22: f Joins P1.m,P1.n,G1;
then consider f2 being object such that
A23: f2 Joins P1.m,P1.n,G1 & f2 in E and
A24: for f9 being object st f9 Joins P1.m,P1.n,G1 & f9 in E
holds f9 = f2 by Def5;
A25: f2 Joins P2.m,P2.n,G2 by A2, A19, A23, GLIB_000:73;
A26: k < len P2 by A18, A20;
then A27: P2.(k+1) Joins P2.k,P2.(k+2),G2 by GLIB_001:def 3;
P1.k = P2.k & P1.(k+2) = P2.(k+2) by A13, Th29;
then A28: P2.(k+1) Joins P1.k,P1.(k+2),G1 by A27, GLIB_000:72;
A29: P2.(k+1) in E by A2, A27, GLIB_000:def 13;
P1.m = P1.k & P1.n = P1.(k+2) or P1.m = P1.(k+2) & P1.n = P1.k
by A21, A22, GLIB_000:15;
then P2.(k+1) = f2 by A24, A28, A29, GLIB_000:14;
hence contradiction by A17, A25, A26, GLIB_001:100;
end;
hence P1 is chordal by CHORD:def 10;
end;
hence G1 is chordal by CHORD:def 11;
end;
theorem Th107:
for G1 being _Graph, G2 being removeDParallelEdges of G1
holds G1 is chordal iff G2 is chordal
proof
let G1 be _Graph, G2 be removeDParallelEdges of G1;
set G3 = the removeParallelEdges of G2;
G3 is removeParallelEdges of G1 by Th95;
then G1 is chordal iff G3 is chordal by Th106;
hence thesis by Th106;
end;
:: non chordal cluster after non chordal has been clustered with cycles
registration
let G be chordal _Graph;
cluster -> chordal for removeParallelEdges of G;
coherence by Th106;
cluster -> chordal for removeDParallelEdges of G;
coherence by Th107;
end;
:: for cut-vertex property, same as with removeLoops above
theorem Th108:
for G1 being _Graph, v being set, G2 being removeParallelEdges of G1
for G3 being removeVertex of G1, v, G4 being removeVertex of G2, v
holds G4 is removeParallelEdges of G3
proof
let G1 be _Graph, v be set, G2 be removeParallelEdges of G1;
let G3 be removeVertex of G1, v, G4 be removeVertex of G2, v;
consider E1 being RepEdgeSelection of G1 such that
A1: G2 is inducedSubgraph of G1, the_Vertices_of G1, E1 by Def7;
the_Vertices_of G1 c= the_Vertices_of G1 &
the_Edges_of G1 = G1.edgesBetween(the_Vertices_of G1) by GLIB_000:34;
then A2: the_Vertices_of G2 = the_Vertices_of G1 &
the_Edges_of G2 = E1 by A1, GLIB_000:def 37;
per cases;
suppose A3: G1 is non _trivial & v in the_Vertices_of G1;
then reconsider v1 = v as Vertex of G1;
reconsider v2 = v1 as Vertex of G2 by A2;
A4: the_Vertices_of G3 = the_Vertices_of G1 \ {v1} & the_Edges_of G3
= G1.edgesBetween(the_Vertices_of G1 \ {v1}) by A3, GLIB_000:47;
then A5: the_Edges_of G3
= G1.edgesBetween(the_Vertices_of G1) \ v1.edgesInOut() by GLIB_000:107
.= the_Edges_of G1 \ v1.edgesInOut() by GLIB_000:34;
A6: the_Vertices_of G4 = the_Vertices_of G2 \ {v2} & the_Edges_of G4
= G2.edgesBetween(the_Vertices_of G2 \ {v2}) by A3, GLIB_000:47;
then A7: the_Edges_of G4
= G2.edgesBetween(the_Vertices_of G2) \ v2.edgesInOut() by GLIB_000:107
.= the_Edges_of G2 \ v2.edgesInOut() by GLIB_000:34;
set E2 = E1 /\ the_Edges_of G3;
A8: E2 c= the_Edges_of G3 by XBOOLE_1:17;
now
let v,w,e0 be object;
assume A9: e0 Joins v,w,G3;
A10: v is set & w is set by TARSKI:1;
then e0 Joins v,w,G1 by A9, GLIB_000:72;
then consider e being object such that
A11: e Joins v,w,G1 & e in E1 and
A12: for e9 being object st e9 Joins v,w,G1 & e9 in E1 holds e9 = e
by Def5;
take e;
A13: e in the_Edges_of G3
proof
not e in v1.edgesInOut()
proof
assume e in v1.edgesInOut();
then (the_Source_of G1).e = v1 or (the_Target_of G1).e = v1
by GLIB_000:61;
then v = v1 or w = v1 by A11, GLIB_000:def 13;
then A14: v1 in the_Vertices_of G3 by A9, GLIB_000:13;
v1 in {v1} by TARSKI:def 1;
hence contradiction by A4, A14, XBOOLE_0:def 5;
end;
hence thesis by A5, A11, XBOOLE_0:def 5;
end;
hence e Joins v,w,G3 by A10, A11, GLIB_000:73;
thus e in E2 by A11, A13, XBOOLE_0:def 4;
let e9 be object;
assume A15: e9 Joins v,w,G3 & e9 in E2;
then e9 in E1 & e9 in the_Edges_of G3 by XBOOLE_0:def 4;
hence e9 = e by A10, A12, A15, GLIB_000:72;
end;
then reconsider E2 as RepEdgeSelection of G3 by A8, Def5;
A16: the_Vertices_of G4 = the_Vertices_of G3 by A2, A4, A6;
A17: G4 is Subgraph of G1 by GLIB_000:43;
for e being object holds e in the_Edges_of G4 iff e in E2
proof
let e be object;
hereby
assume A18: e in the_Edges_of G4;
then A19: e in E1 by A2;
the_Edges_of G4 c= the_Edges_of G1 by A17, GLIB_000:def 32;
then A20: e in the_Edges_of G1 by A18;
not e in v1.edgesInOut()
proof
assume e in v1.edgesInOut();
then ((the_Source_of G1).e = v1 or (the_Target_of G1).e = v1)
by GLIB_000:61;
then e Joins v1,(the_Target_of G1).e,G1 or
e Joins (the_Source_of G1).e,v1,G1 by A20, GLIB_000:def 13;
then e Joins v1,(the_Target_of G1).e,G4 or
e Joins (the_Source_of G1).e,v1,G4
by A18, A17, GLIB_000:73;
then A21: v1 in the_Vertices_of G4 by GLIB_000:13;
v1 in {v2} by TARSKI:def 1;
hence contradiction by A6, A21, XBOOLE_0:def 5;
end;
then e in the_Edges_of G3 by A5, A20, XBOOLE_0:def 5;
hence e in E2 by A19, XBOOLE_0:def 4;
end;
assume e in E2;
then A22: e in the_Edges_of G3 & e in E1 by XBOOLE_0:def 4;
not e in v2.edgesInOut()
proof
assume e in v2.edgesInOut();
then ((the_Source_of G2).e = v2 or (the_Target_of G2).e = v2)
by GLIB_000:61;
then e Joins v2,(the_Target_of G2).e,G2 or
e Joins (the_Source_of G2).e,v2,G2 by A2, A22, GLIB_000:def 13;
then e Joins v2,(the_Target_of G2).e,G1 or
e Joins (the_Source_of G2).e,v2,G1 by GLIB_000:72;
then e Joins v2,(the_Target_of G2).e,G3 or
e Joins (the_Source_of G2).e,v2,G3 by A22, GLIB_000:73;
then A23: v2 in the_Vertices_of G3 by GLIB_000:13;
v2 in {v1} by TARSKI:def 1;
hence contradiction by A4, A23, XBOOLE_0:def 5;
end;
hence e in the_Edges_of G4 by A2, A7, A22, XBOOLE_0:def 5;
end;
then A24: the_Edges_of G4 = E2 by TARSKI:2;
then A25: G4 is Subgraph of G3 by A16, A17, GLIB_000:44;
the_Vertices_of G3 c= the_Vertices_of G3 &
the_Edges_of G3 = G3.edgesBetween(the_Vertices_of G3) by GLIB_000:34;
then G4 is inducedSubgraph of G3, the_Vertices_of G3, E2
by A16, A24, A25, GLIB_000:def 37;
hence thesis by Def7;
end;
suppose A26: G1 is _trivial or not v in the_Vertices_of G1;
then A27: G1 == G3 by GLIB_000:114;
G2 is _trivial or not v in the_Vertices_of G2 by A26;
then G2 == G4 by GLIB_000:114;
then G4 is removeParallelEdges of G1 by Th93;
hence thesis by A27, Th91;
end;
end;
theorem Th109:
for G1 being _Graph, G2 being removeParallelEdges of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds v1 is cut-vertex iff v2 is cut-vertex
proof
let G1 be _Graph, G2 be removeParallelEdges of G1;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2;
hereby
assume A2: v1 is cut-vertex;
now
let G4 be removeVertex of G2, v2;
set G3 = the removeVertex of G1, v1;
G4 is removeParallelEdges of G3 by A1, Th108;
then G3.numComponents() = G4.numComponents() by Th104;
then G1.numComponents() in G4.numComponents() by A2, GLIB_002:def 10;
hence G2.numComponents() in G4.numComponents() by Th104;
end;
hence v2 is cut-vertex by GLIB_002:def 10;
end;
assume A3: v2 is cut-vertex;
now
let G3 be removeVertex of G1, v1;
set G4 = the removeVertex of G2, v2;
G4 is removeParallelEdges of G3 by A1, Th108;
then G3.numComponents() = G4.numComponents() by Th104;
then G2.numComponents() in G3.numComponents() by A3, GLIB_002:def 10;
hence G1.numComponents() in G3.numComponents() by Th104;
end;
hence v1 is cut-vertex by GLIB_002:def 10;
end;
theorem Th110:
for G1 being _Graph, G2 being removeDParallelEdges of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds v1 is cut-vertex iff v2 is cut-vertex
proof
let G1 be _Graph, G2 be removeDParallelEdges of G1;
set G3 = the removeParallelEdges of G2;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2;
reconsider v3 = v2 as Vertex of G3 by GLIB_000:def 33;
G3 is removeParallelEdges of G1 by Th95;
then v1 is cut-vertex iff v3 is cut-vertex by A1, Th109;
hence thesis by Th109;
end;
theorem Th111:
for G1 being _Graph, G2 being removeParallelEdges of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds v1 is isolated iff v2 is isolated
proof
let G1 be _Graph, G2 be removeParallelEdges of G1;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2;
hence v1 is isolated implies v2 is isolated by GLIB_000:83;
assume v2 is isolated;
then A2: v2.edgesInOut() = {} by GLIB_000:def 49;
v1.edgesInOut() = {}
proof
assume v1.edgesInOut() <> {};
then consider e0 being object such that
A3: e0 in v1.edgesInOut() by XBOOLE_0:def 1;
consider w being Vertex of G1 such that
A4: e0 Joins v1,w,G1 by A3, GLIB_000:64;
consider E1 being RepEdgeSelection of G1 such that
A5: G2 is inducedSubgraph of G1, the_Vertices_of G1, E1 by Def7;
consider e1 being object such that
A6: e1 Joins v1,w,G1 & e1 in E1 and
for e9 being object st e9 Joins v1,w,G1 & e9 in E1 holds e9 = e1
by A4, Def5;
the_Vertices_of G1 c= the_Vertices_of G1 &
the_Edges_of G1 = G1.edgesBetween(the_Vertices_of G1) by GLIB_000:34;
then A7: the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G2 = E1 by A5, GLIB_000:def 37;
then reconsider w as Vertex of G2;
A8: e1 Joins v2,w,G2 by A1, A6, A7, GLIB_000:73;
e1 is set by TARSKI:1;
hence thesis by A2, A8, GLIB_000:64;
end;
hence thesis by GLIB_000:def 49;
end;
theorem Th112:
for G1 being _Graph, G2 being removeDParallelEdges of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds v1 is isolated iff v2 is isolated
proof
let G1 be _Graph, G2 be removeDParallelEdges of G1;
set G3 = the removeParallelEdges of G2;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2;
reconsider v3 = v2 as Vertex of G3 by GLIB_000:def 33;
G3 is removeParallelEdges of G1 by Th95;
then v1 is isolated iff v3 is isolated by A1, Th111;
hence thesis by Th111;
end;
theorem Th113:
for G1 being _Graph, G2 being removeParallelEdges of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & v1 is endvertex holds v2 is endvertex
proof
let G1 be _Graph, G2 be removeParallelEdges of G1;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2 & v1 is endvertex;
then A2: v2 is endvertex or v2 is isolated by GLIB_000:84;
v1 is non isolated by A1;
hence v2 is endvertex by A1, A2, Th111;
end;
theorem Th114:
for G1 being _Graph, G2 being removeDParallelEdges of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & v1 is endvertex holds v2 is endvertex
proof
let G1 be _Graph, G2 be removeDParallelEdges of G1;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2 & v1 is endvertex;
then A2: v2 is endvertex or v2 is isolated by GLIB_000:84;
v1 is non isolated by A1;
hence v2 is endvertex by A1, A2, Th112;
end;
:: Graphs with Loops and parallel Edges removed
definition
let G be _Graph;
mode SimpleGraph of G -> Subgraph of G means
:Def9:
ex E being RepEdgeSelection of G st
it is inducedSubgraph of G, the_Vertices_of G, E \ G.loops();
existence
proof
set E = the RepEdgeSelection of G;
set G2 = the inducedSubgraph of G, the_Vertices_of G, E \ G.loops();
take G2, E;
thus thesis;
end;
mode DSimpleGraph of G -> Subgraph of G means
:Def10:
ex E being RepDEdgeSelection of G st
it is inducedSubgraph of G, the_Vertices_of G, E \ G.loops();
existence
proof
set E = the RepDEdgeSelection of G;
set G2 = the inducedSubgraph of G, the_Vertices_of G, E \ G.loops();
take G2, E;
thus thesis;
end;
end;
theorem
for G1 being _Graph, G2 being removeParallelEdges of G1
for G3 being removeLoops of G2 holds G3 is SimpleGraph of G1
proof
let G1 be _Graph, G2 be removeParallelEdges of G1, G3 be removeLoops of G2;
consider E being RepEdgeSelection of G1 such that
A1: G2 is inducedSubgraph of G1, the_Vertices_of G1, E by Def7;
A2: the_Vertices_of G1 c= the_Vertices_of G1 &
the_Edges_of G1 = G1.edgesBetween(the_Vertices_of G1) by GLIB_000:34;
then A3: the_Vertices_of G2 = the_Vertices_of G1 &
the_Edges_of G2 = E by A1, GLIB_000:def 37;
A4: the_Vertices_of G3 = the_Vertices_of G2 &
the_Edges_of G3 = the_Edges_of G2 \ G2.loops() by GLIB_000:53;
A5: the_Edges_of G2 \ G1.loops() c= the_Edges_of G2 \ G2.loops()
by Th48, XBOOLE_1:34;
now
let e be object;
assume e in the_Edges_of G2 \ G2.loops();
then A6: e in the_Edges_of G2 & not e in G2.loops() by XBOOLE_0:def 5;
not e in G1.loops()
proof
assume e in G1.loops();
then consider v being object such that
A7: e Joins v,v,G1 by Def2;
e is set & v is set by TARSKI:1;
then e Joins v,v,G2 by A6, A7, GLIB_000:73;
hence contradiction by A6, Def2;
end;
hence e in the_Edges_of G2 \ G1.loops() by A6, XBOOLE_0:def 5;
end;
then the_Edges_of G2 \ G2.loops() c= the_Edges_of G2 \ G1.loops()
by TARSKI:def 3;
then A8: the_Edges_of G3 = E \ G1.loops() by A3, A4, A5, XBOOLE_0:def 10;
A9: the_Vertices_of G3 = the_Vertices_of G1 by A3, A4;
G3 is Subgraph of G1 by GLIB_000:43;
then G3 is inducedSubgraph of G1, the_Vertices_of G1, E \ G1.loops()
by A2, A8, A9, GLIB_000:def 37;
hence thesis by Def9;
end;
theorem
for G1 being _Graph, G2 being removeDParallelEdges of G1
for G3 being removeLoops of G2 holds G3 is DSimpleGraph of G1
proof
let G1 be _Graph, G2 be removeDParallelEdges of G1, G3 be removeLoops of G2;
consider E being RepDEdgeSelection of G1 such that
A1: G2 is inducedSubgraph of G1, the_Vertices_of G1, E by Def8;
A2: the_Vertices_of G1 c= the_Vertices_of G1 &
the_Edges_of G1 = G1.edgesBetween(the_Vertices_of G1) by GLIB_000:34;
then A3: the_Vertices_of G2 = the_Vertices_of G1 &
the_Edges_of G2 = E by A1, GLIB_000:def 37;
A4: the_Vertices_of G3 = the_Vertices_of G2 &
the_Edges_of G3 = the_Edges_of G2 \ G2.loops() by GLIB_000:53;
A5: the_Edges_of G2 \ G1.loops() c= the_Edges_of G2 \ G2.loops()
by Th48, XBOOLE_1:34;
now
let e be object;
assume e in the_Edges_of G2 \ G2.loops();
then A6: e in the_Edges_of G2 & not e in G2.loops() by XBOOLE_0:def 5;
not e in G1.loops()
proof
assume e in G1.loops();
then consider v being object such that
A7: e Joins v,v,G1 by Def2;
e is set & v is set by TARSKI:1;
then e Joins v,v,G2 by A6, A7, GLIB_000:73;
hence contradiction by A6, Def2;
end;
hence e in the_Edges_of G2 \ G1.loops() by A6, XBOOLE_0:def 5;
end;
then the_Edges_of G2 \ G2.loops() c= the_Edges_of G2 \ G1.loops()
by TARSKI:def 3;
then A8: the_Edges_of G3 = E \ G1.loops() by A3, A4, A5, XBOOLE_0:def 10;
A9: the_Vertices_of G3 = the_Vertices_of G1 by A3, A4;
G3 is Subgraph of G1 by GLIB_000:43;
then G3 is inducedSubgraph of G1, the_Vertices_of G1, E \ G1.loops()
by A2, A8, A9, GLIB_000:def 37;
hence thesis by Def10;
end;
theorem Th117:
for G1 being _Graph, G2 being removeLoops of G1
for G3 being removeParallelEdges of G2 holds G3 is SimpleGraph of G1
proof
let G1 be _Graph, G2 be removeLoops of G1;
let G3 be removeParallelEdges of G2;
consider E being RepEdgeSelection of G2 such that
A1: G3 is inducedSubgraph of G2, the_Vertices_of G2, E by Def7;
the_Vertices_of G2 c= the_Vertices_of G2 &
the_Edges_of G2 = G2.edgesBetween(the_Vertices_of G2) by GLIB_000:34;
then A2: the_Vertices_of G3 = the_Vertices_of G2 &
the_Edges_of G3 = E by A1, GLIB_000:def 37;
A3: the_Vertices_of G2 = the_Vertices_of G1 &
the_Edges_of G2 = the_Edges_of G1 \ G1.loops() by GLIB_000:53;
consider E0 being RepEdgeSelection of G1 such that
A4: E = E0 /\ the_Edges_of G2 by Th80;
A5: the_Vertices_of G3 = the_Vertices_of G1 by A2, A3;
for e being object holds e in the_Edges_of G3 iff e in E0 \ G1.loops()
proof
let e be object;
hereby
assume e in the_Edges_of G3;
then A6: e in E0 & e in the_Edges_of G2 by A2, A4, XBOOLE_0:def 4;
then not e in G1.loops() by A3, XBOOLE_0:def 5;
hence e in E0 \ G1.loops() by A6, XBOOLE_0:def 5;
end;
assume A7: e in E0 \ G1.loops();
then A8: e in the_Edges_of G2 by A3, TARSKI:def 3, XBOOLE_1:33;
e in E0 by A7, XBOOLE_0:def 5;
hence thesis by A2, A4, A8, XBOOLE_0:def 4;
end;
then A9: the_Edges_of G3 = E0 \ G1.loops() by TARSKI:2;
A10: G3 is Subgraph of G1 by GLIB_000:43;
the_Vertices_of G1 c= the_Vertices_of G1 &
the_Edges_of G1 = G1.edgesBetween(the_Vertices_of G1) by GLIB_000:34;
then G3 is inducedSubgraph of G1, the_Vertices_of G1, E0 \ G1.loops()
by A5, A9, A10, GLIB_000:def 37;
hence thesis by Def9;
end;
theorem Th118:
for G1 being _Graph, G2 being removeLoops of G1
for G3 being removeDParallelEdges of G2 holds G3 is DSimpleGraph of G1
proof
let G1 be _Graph, G2 be removeLoops of G1;
let G3 be removeDParallelEdges of G2;
consider E being RepDEdgeSelection of G2 such that
A1: G3 is inducedSubgraph of G2, the_Vertices_of G2, E by Def8;
the_Vertices_of G2 c= the_Vertices_of G2 &
the_Edges_of G2 = G2.edgesBetween(the_Vertices_of G2) by GLIB_000:34;
then A2: the_Vertices_of G3 = the_Vertices_of G2 &
the_Edges_of G3 = E by A1, GLIB_000:def 37;
A3: the_Vertices_of G2 = the_Vertices_of G1 &
the_Edges_of G2 = the_Edges_of G1 \ G1.loops() by GLIB_000:53;
consider E0 being RepDEdgeSelection of G1 such that
A4: E = E0 /\ the_Edges_of G2 by Th81;
A5: the_Vertices_of G3 = the_Vertices_of G1 by A2, A3;
for e being object holds e in the_Edges_of G3 iff e in E0 \ G1.loops()
proof
let e be object;
hereby
assume e in the_Edges_of G3;
then A6: e in E0 & e in the_Edges_of G2 by A2, A4, XBOOLE_0:def 4;
then not e in G1.loops() by A3, XBOOLE_0:def 5;
hence e in E0 \ G1.loops() by A6, XBOOLE_0:def 5;
end;
assume A7: e in E0 \ G1.loops();
then A8: e in the_Edges_of G2 by A3, TARSKI:def 3, XBOOLE_1:33;
e in E0 by A7, XBOOLE_0:def 5;
hence thesis by A2, A4, A8, XBOOLE_0:def 4;
end;
then A9: the_Edges_of G3 = E0 \ G1.loops() by TARSKI:2;
A10: G3 is Subgraph of G1 by GLIB_000:43;
the_Vertices_of G1 c= the_Vertices_of G1 &
the_Edges_of G1 = G1.edgesBetween(the_Vertices_of G1) by GLIB_000:34;
then G3 is inducedSubgraph of G1, the_Vertices_of G1, E0 \ G1.loops()
by A5, A9, A10, GLIB_000:def 37;
hence thesis by Def10;
end;
theorem Th119:
for G1 being _Graph, G3 being SimpleGraph of G1
ex G2 being removeParallelEdges of G1 st G3 is removeLoops of G2
proof
let G1 be _Graph, G3 be SimpleGraph of G1;
consider E being RepEdgeSelection of G1 such that
A1: G3 is inducedSubgraph of G1,the_Vertices_of G1,E\G1.loops() by Def9;
set G2 = the inducedSubgraph of G1, the_Vertices_of G1, E;
reconsider G2 as removeParallelEdges of G1 by Def7;
take G2;
A2: the_Vertices_of G1 c= the_Vertices_of G1 &
the_Edges_of G1 = G1.edgesBetween(the_Vertices_of G1) by GLIB_000:34;
then A3: the_Vertices_of G3 = the_Vertices_of G1 &
the_Edges_of G3 = E \ G1.loops() by A1, GLIB_000:def 37;
A4: the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = E
by A2, GLIB_000:def 37;
A5: the_Vertices_of G3 = the_Vertices_of G2 by A3, A4;
for e being object holds e in the_Edges_of G3 iff
e in the_Edges_of G2 \ G2.loops()
proof
let e be object;
hereby
assume e in the_Edges_of G3;
then A6: e in the_Edges_of G2 & not e in G1.loops()
by A3, A4, XBOOLE_0:def 5;
not e in G2.loops()
proof
assume e in G2.loops();
then consider v being object such that
A7: e Joins v,v,G2 by Def2;
e is set & v is set by TARSKI:1;
then e Joins v,v,G1 by A7, GLIB_000:72;
hence contradiction by A6, Def2;
end;
hence e in the_Edges_of G2 \ G2.loops() by A6, XBOOLE_0:def 5;
end;
assume e in the_Edges_of G2 \ G2.loops();
then A8: e in the_Edges_of G2 & not e in G2.loops() by XBOOLE_0:def 5;
not e in G1.loops()
proof
assume e in G1.loops();
then consider v being object such that
A9: e Joins v,v,G1 by Def2;
e is set & v is set by TARSKI:1;
then e Joins v,v,G2 by A8, A9, GLIB_000:73;
hence contradiction by A8, Def2;
end;
hence e in the_Edges_of G3 by A3, A4, A8, XBOOLE_0:def 5;
end;
then A10: the_Edges_of G3 = the_Edges_of G2 \ G2.loops() by TARSKI:2;
E \ G1.loops() c= E by XBOOLE_1:36;
then A11: G3 is Subgraph of G2 by A2, A1, GLIB_000:46;
the_Vertices_of G2 c= the_Vertices_of G2 &
the_Edges_of G2 = G2.edgesBetween(the_Vertices_of G2) by GLIB_000:34;
hence thesis by A5, A10, A11, GLIB_000:def 37;
end;
theorem Th120:
for G1 being _Graph, G3 being DSimpleGraph of G1
ex G2 being removeDParallelEdges of G1 st G3 is removeLoops of G2
proof
let G1 be _Graph, G3 be DSimpleGraph of G1;
consider E being RepDEdgeSelection of G1 such that
A1: G3 is inducedSubgraph of G1,the_Vertices_of G1,E\G1.loops() by Def10;
set G2 = the inducedSubgraph of G1, the_Vertices_of G1, E;
reconsider G2 as removeDParallelEdges of G1 by Def8;
take G2;
A2: the_Vertices_of G1 c= the_Vertices_of G1 &
the_Edges_of G1 = G1.edgesBetween(the_Vertices_of G1) by GLIB_000:34;
then A3: the_Vertices_of G3 = the_Vertices_of G1 &
the_Edges_of G3 = E \ G1.loops() by A1, GLIB_000:def 37;
A4: the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = E
by A2, GLIB_000:def 37;
A5: the_Vertices_of G3 = the_Vertices_of G2 by A3, A4;
for e being object holds e in the_Edges_of G3 iff
e in the_Edges_of G2 \ G2.loops()
proof
let e be object;
hereby
assume e in the_Edges_of G3;
then A6: e in the_Edges_of G2 & not e in G1.loops()
by A3, A4, XBOOLE_0:def 5;
not e in G2.loops()
proof
assume e in G2.loops();
then consider v being object such that
A7: e Joins v,v,G2 by Def2;
e is set & v is set by TARSKI:1;
then e Joins v,v,G1 by A7, GLIB_000:72;
hence contradiction by A6, Def2;
end;
hence e in the_Edges_of G2 \ G2.loops() by A6, XBOOLE_0:def 5;
end;
assume e in the_Edges_of G2 \ G2.loops();
then A8: e in the_Edges_of G2 & not e in G2.loops() by XBOOLE_0:def 5;
not e in G1.loops()
proof
assume e in G1.loops();
then consider v being object such that
A9: e Joins v,v,G1 by Def2;
e is set & v is set by TARSKI:1;
then e Joins v,v,G2 by A8, A9, GLIB_000:73;
hence contradiction by A8, Def2;
end;
hence e in the_Edges_of G3 by A3, A4, A8, XBOOLE_0:def 5;
end;
then A10: the_Edges_of G3 = the_Edges_of G2 \ G2.loops() by TARSKI:2;
E \ G1.loops() c= E by XBOOLE_1:36;
then A11: G3 is Subgraph of G2 by A2, A1, GLIB_000:46;
the_Vertices_of G2 c= the_Vertices_of G2 &
the_Edges_of G2 = G2.edgesBetween(the_Vertices_of G2) by GLIB_000:34;
hence thesis by A5, A10, A11, GLIB_000:def 37;
end;
theorem Th121:
for G1 being _Graph, G2 being removeLoops of G1, G3 being SimpleGraph of G1
holds G3 is removeParallelEdges of G2
proof
let G1 be _Graph, G2 being removeLoops of G1, G3 be SimpleGraph of G1;
consider E being RepEdgeSelection of G1 such that
A1: G3 is inducedSubgraph of G1,the_Vertices_of G1,E\G1.loops() by Def9;
A2: the_Vertices_of G1 c= the_Vertices_of G1 &
the_Edges_of G1 = G1.edgesBetween(the_Vertices_of G1) by GLIB_000:34;
then A3: the_Vertices_of G3 = the_Vertices_of G1 &
the_Edges_of G3 = E\G1.loops() by A1, GLIB_000:def 37;
A4: the_Vertices_of G2 = the_Vertices_of G1 &
the_Edges_of G2 = the_Edges_of G1 \ G1.loops() by GLIB_000:53;
set E2 = E \ G1.loops();
A5: E2 c= the_Edges_of G2 by A4, XBOOLE_1:33;
now
let v,w,e0 be object;
A6: v is set & w is set by TARSKI:1;
assume A7: e0 Joins v,w,G2;
then A8: e0 Joins v,w,G1 by A6, GLIB_000:72;
then consider e being object such that
A9: e Joins v,w,G1 & e in E and
A10: for e9 being object st e9 Joins v,w,G1 & e9 in E holds e9 = e
by Def5;
take e;
A11: not e in G1.loops()
proof
assume e in G1.loops();
then consider u being object such that
A12: e Joins u,u,G1 by Def2;
v = u & w = u by A9, A12, GLIB_000:15;
then A13: e0 in G1.loops() by A8, Def2;
e0 in the_Edges_of G2 by A7, GLIB_000:def 13;
hence contradiction by A4, A13, XBOOLE_0:def 5;
end;
e in the_Edges_of G2 by A4, A9, A11, XBOOLE_0:def 5;
hence e Joins v,w,G2 by A6, A9, GLIB_000:73;
thus e in E2 by A9, A11, XBOOLE_0:def 5;
let e9 be object;
assume e9 Joins v,w,G2 & e9 in E2;
then e9 Joins v,w,G1 & e9 in E2 by A6, GLIB_000:72;
then e9 Joins v,w,G1 & e9 in E by XBOOLE_1:36, TARSKI:def 3;
hence e9 = e by A10;
end;
then reconsider E2 as RepEdgeSelection of G2 by A5, Def5;
A14: the_Vertices_of G3 = the_Vertices_of G2 by A3, A4;
E\G1.loops() c= the_Edges_of G1\G1.loops() by XBOOLE_1:33;
then A15: G3 is Subgraph of G2 by A1, A2, GLIB_000:46;
the_Vertices_of G2 c= the_Vertices_of G2 &
the_Edges_of G2 = G2.edgesBetween(the_Vertices_of G2) by GLIB_000:34;
then G3 is inducedSubgraph of G2, the_Vertices_of G2, E2
by A3, A14, A15, GLIB_000:def 37;
hence thesis by Def7;
end;
theorem Th122:
for G1 being _Graph, G2 being removeLoops of G1, G3 being DSimpleGraph of G1
holds G3 is removeDParallelEdges of G2
proof
let G1 be _Graph, G2 being removeLoops of G1, G3 be DSimpleGraph of G1;
consider E being RepDEdgeSelection of G1 such that
A1: G3 is inducedSubgraph of G1,the_Vertices_of G1,E\G1.loops() by Def10;
A2: the_Vertices_of G1 c= the_Vertices_of G1 &
the_Edges_of G1 = G1.edgesBetween(the_Vertices_of G1) by GLIB_000:34;
then A3: the_Vertices_of G3 = the_Vertices_of G1 &
the_Edges_of G3 = E\G1.loops() by A1, GLIB_000:def 37;
A4: the_Vertices_of G2 = the_Vertices_of G1 &
the_Edges_of G2 = the_Edges_of G1 \ G1.loops() by GLIB_000:53;
set E2 = E \ G1.loops();
A5: E2 c= the_Edges_of G2 by A4, XBOOLE_1:33;
now
let v,w,e0 be object;
A6: v is set & w is set by TARSKI:1;
assume A7: e0 DJoins v,w,G2;
then A8: e0 DJoins v,w,G1 by A6, GLIB_000:72;
then consider e being object such that
A9: e DJoins v,w,G1 & e in E and
A10: for e9 being object st e9 DJoins v,w,G1 & e9 in E holds e9 = e
by Def6;
take e;
A11: not e in G1.loops()
proof
assume e in G1.loops();
then consider u being object such that
A12: e DJoins u,u,G1 by Th45;
v = u & w = u by A9, A12, GLIB_000:125;
then A13: e0 in G1.loops() by A8, Th45;
e0 in the_Edges_of G2 by A7, GLIB_000:def 14;
hence contradiction by A4, A13, XBOOLE_0:def 5;
end;
then e in the_Edges_of G2 by A4, A9, XBOOLE_0:def 5;
hence e DJoins v,w,G2 by A6, A9, GLIB_000:73;
thus e in E2 by A9, A11, XBOOLE_0:def 5;
let e9 be object;
assume e9 DJoins v,w,G2 & e9 in E2;
then e9 DJoins v,w,G1 & e9 in E2 by A6, GLIB_000:72;
then e9 DJoins v,w,G1 & e9 in E by XBOOLE_1:36, TARSKI:def 3;
hence e9 = e by A10;
end;
then reconsider E2 as RepDEdgeSelection of G2 by A5, Def6;
A14: the_Vertices_of G3 = the_Vertices_of G2 by A3, A4;
E\G1.loops() c= the_Edges_of G1\G1.loops() by XBOOLE_1:33;
then A15: G3 is Subgraph of G2 by A1, A2, GLIB_000:46;
the_Vertices_of G2 c= the_Vertices_of G2 &
the_Edges_of G2 = G2.edgesBetween(the_Vertices_of G2) by GLIB_000:34;
then G3 is inducedSubgraph of G2, the_Vertices_of G2, E2
by A3, A14, A15, GLIB_000:def 37;
hence thesis by Def8;
end;
theorem Th123:
for G1 being loopless _Graph, G2 being _Graph
holds G2 is SimpleGraph of G1 iff G2 is removeParallelEdges of G1
proof
let G1 be loopless _Graph, G2 be _Graph;
hereby
assume G2 is SimpleGraph of G1;
then consider E being RepEdgeSelection of G1 such that
A1: G2 is inducedSubgraph of G1, the_Vertices_of G1, E \ G1.loops()
by Def9;
thus G2 is removeParallelEdges of G1 by A1, Def7;
end;
assume G2 is removeParallelEdges of G1;
then consider E being RepEdgeSelection of G1 such that
A2: G2 is inducedSubgraph of G1, the_Vertices_of G1, E by Def7;
E = E \ G1.loops();
hence G2 is SimpleGraph of G1 by A2, Def9;
end;
theorem
for G1 being loopless _Graph, G2 being _Graph
holds G2 is DSimpleGraph of G1 iff G2 is removeDParallelEdges of G1
proof
let G1 be loopless _Graph, G2 be _Graph;
hereby
assume G2 is DSimpleGraph of G1;
then consider E being RepDEdgeSelection of G1 such that
A1: G2 is inducedSubgraph of G1, the_Vertices_of G1, E \ G1.loops()
by Def10;
thus G2 is removeDParallelEdges of G1 by A1, Def8;
end;
assume G2 is removeDParallelEdges of G1;
then consider E being RepDEdgeSelection of G1 such that
A2: G2 is inducedSubgraph of G1, the_Vertices_of G1, E by Def8;
E = E \ G1.loops();
hence G2 is DSimpleGraph of G1 by A2, Def10;
end;
theorem
for G1 being non-multi _Graph, G2 being _Graph
holds G2 is SimpleGraph of G1 iff G2 is removeLoops of G1
proof
let G1 be non-multi _Graph, G2 be _Graph;
hereby
assume G2 is SimpleGraph of G1;
then consider E being RepEdgeSelection of G1 such that
A1: G2 is inducedSubgraph of G1, the_Vertices_of G1, E\G1.loops()
by Def9;
thus G2 is removeLoops of G1 by A1, Th74;
end;
assume A2: G2 is removeLoops of G1;
set E = the RepEdgeSelection of G1;
E = the_Edges_of G1 by Th74;
hence thesis by A2, Def9;
end;
theorem
for G1 being non-Dmulti _Graph, G2 being _Graph
holds G2 is DSimpleGraph of G1 iff G2 is removeLoops of G1
proof
let G1 be non-Dmulti _Graph, G2 be _Graph;
hereby
assume G2 is DSimpleGraph of G1;
then consider E being RepDEdgeSelection of G1 such that
A1: G2 is inducedSubgraph of G1, the_Vertices_of G1, E\G1.loops()
by Def10;
thus G2 is removeLoops of G1 by A1, Th76;
end;
assume A2: G2 is removeLoops of G1;
set E = the RepDEdgeSelection of G1;
E = the_Edges_of G1 by Th76;
hence thesis by A2, Def10;
end;
registration
let G be _Graph;
cluster -> spanning loopless non-multi simple for SimpleGraph of G;
coherence
proof
let G3 be SimpleGraph of G;
consider E being RepEdgeSelection of G such that
A1: G3 is inducedSubgraph of G, the_Vertices_of G, E\G.loops() by Def9;
consider G2 being removeParallelEdges of G such that
A2: G3 is removeLoops of G2 by Th119;
thus thesis by A1, A2;
end;
cluster -> spanning loopless non-Dmulti Dsimple for DSimpleGraph of G;
coherence
proof
let G3 be DSimpleGraph of G;
consider E being RepDEdgeSelection of G such that
A3: G3 is inducedSubgraph of G, the_Vertices_of G, E\G.loops() by Def10;
consider G2 being removeDParallelEdges of G such that
A4: G3 is removeLoops of G2 by Th120;
thus thesis by A3, A4;
end;
cluster plain for SimpleGraph of G;
existence
proof
set E = the RepEdgeSelection of G;
reconsider G2 = the plain inducedSubgraph of G, the_Vertices_of G,
E\G.loops() as SimpleGraph of G by Def9;
take G2;
thus thesis;
end;
cluster plain for DSimpleGraph of G;
existence
proof
set E = the RepDEdgeSelection of G;
reconsider G2 = the plain inducedSubgraph of G, the_Vertices_of G,
E\G.loops() as DSimpleGraph of G by Def10;
take G2;
thus thesis;
end;
end;
theorem
for G1 being simple _Graph, G2 being _Graph
holds G1 == G2 iff G2 is SimpleGraph of G1
proof
let G1 be simple _Graph, G2 be _Graph;
hereby
assume A1: G1 == G2;
set E = the RepEdgeSelection of G1;
A2: the_Edges_of G1 = E \ G1.loops() by Th74;
G1 is inducedSubgraph of G1, the_Vertices_of G1 by GLIB_000:100;
then G1 is inducedSubgraph of G1, the_Vertices_of G1, the_Edges_of G1
by GLIB_000:34;
then G2 is inducedSubgraph of G1, the_Vertices_of G1, the_Edges_of G1
by A1, GLIB_000:101;
hence G2 is SimpleGraph of G1 by A2, Def9;
end;
assume G2 is SimpleGraph of G1;
then consider E being RepEdgeSelection of G1 such that
A3: G2 is inducedSubgraph of G1,the_Vertices_of G1,E\G1.loops() by Def9;
the_Edges_of G1 = E \ G1.loops() by Th74;
then G2 is inducedSubgraph of G1, the_Vertices_of G1 by A3, GLIB_000:34;
hence G1 == G2 by GLIB_000:94;
end;
theorem
for G1 being Dsimple _Graph, G2 being _Graph
holds G1 == G2 iff G2 is DSimpleGraph of G1
proof
let G1 be Dsimple _Graph, G2 be _Graph;
hereby
assume A1: G1 == G2;
set E = the RepDEdgeSelection of G1;
A2: the_Edges_of G1 = E \ G1.loops() by Th76;
G1 is inducedSubgraph of G1, the_Vertices_of G1 by GLIB_000:100;
then G1 is inducedSubgraph of G1, the_Vertices_of G1, the_Edges_of G1
by GLIB_000:34;
then G2 is inducedSubgraph of G1, the_Vertices_of G1, the_Edges_of G1
by A1, GLIB_000:101;
hence G2 is DSimpleGraph of G1 by A2, Def10;
end;
assume G2 is DSimpleGraph of G1;
then consider E being RepDEdgeSelection of G1 such that
A3: G2 is inducedSubgraph of G1,the_Vertices_of G1,E\G1.loops() by Def10;
the_Edges_of G1 = E \ G1.loops() by Th76;
then G2 is inducedSubgraph of G1, the_Vertices_of G1 by A3, GLIB_000:34;
hence G1 == G2 by GLIB_000:94;
end;
theorem
for G1, G2 being _Graph, G3 being SimpleGraph of G1
st G1 == G2 holds G3 is SimpleGraph of G2
proof
let G1, G2 be _Graph, G3 be SimpleGraph of G1;
consider E being RepEdgeSelection of G1 such that
A1: G3 is inducedSubgraph of G1,the_Vertices_of G1,E\G1.loops() by Def9;
assume A2: G1 == G2;
then A3: the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 by GLIB_000:def 34;
then A4: G3 is inducedSubgraph of G2, the_Vertices_of G2, E\G1.loops()
by A1, A2, GLIB_000:95;
A5: G1.loops() = G2.loops() by A2, Th50;
G2 is Subgraph of G1 by A2, GLIB_000:87;
then E is RepEdgeSelection of G2 by A3, Th78;
hence thesis by A4, A5, Def9;
end;
theorem
for G1, G2 being _Graph, G3 being DSimpleGraph of G1
st G1 == G2 holds G3 is DSimpleGraph of G2
proof
let G1, G2 be _Graph, G3 be DSimpleGraph of G1;
consider E being RepDEdgeSelection of G1 such that
A1: G3 is inducedSubgraph of G1,the_Vertices_of G1,E\G1.loops() by Def10;
assume A2: G1 == G2;
then A3: the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 by GLIB_000:def 34;
then A4: G3 is inducedSubgraph of G2, the_Vertices_of G2, E\G1.loops()
by A1, A2, GLIB_000:95;
A5: G1.loops() = G2.loops() by A2, Th50;
G2 is Subgraph of G1 by A2, GLIB_000:87;
then E is RepDEdgeSelection of G2 by A3, Th79;
hence thesis by A4, A5, Def10;
end;
theorem
for G1, G2 being _Graph, G3 being SimpleGraph of G1
st G2 == G3 holds G2 is SimpleGraph of G1
proof
let G1, G2 be _Graph, G3 be SimpleGraph of G1;
consider E being RepEdgeSelection of G1 such that
A1: G3 is inducedSubgraph of G1,the_Vertices_of G1,E\G1.loops() by Def9;
assume G2 == G3;
then G2 is inducedSubgraph of G1, the_Vertices_of G1, E\G1.loops()
by A1, GLIB_000:101;
hence thesis by Def9;
end;
theorem
for G1, G2 being _Graph, G3 being DSimpleGraph of G1
st G2 == G3 holds G2 is DSimpleGraph of G1
proof
let G1, G2 be _Graph, G3 be DSimpleGraph of G1;
consider E being RepDEdgeSelection of G1 such that
A1: G3 is inducedSubgraph of G1,the_Vertices_of G1,E\G1.loops() by Def10;
assume G2 == G3;
then G2 is inducedSubgraph of G1, the_Vertices_of G1, E\G1.loops()
by A1, GLIB_000:101;
hence thesis by Def10;
end;
theorem Th133:
for G1 being _Graph, G2 being DSimpleGraph of G1, G3 being SimpleGraph of G2
holds G3 is SimpleGraph of G1
proof
let G1 be _Graph, G2 be DSimpleGraph of G1, G3 be SimpleGraph of G2;
set H = the removeLoops of G1;
G2 is removeDParallelEdges of H & G3 is removeParallelEdges of G2
by Th122, Th123;
then G3 is removeParallelEdges of H by Th95;
hence thesis by Th117;
end;
theorem
for G1 being _Graph, G2 being DSimpleGraph of G1
ex G3 being SimpleGraph of G1 st G3 is SimpleGraph of G2
proof
let G1 be _Graph, G2 be DSimpleGraph of G1;
set H = the removeLoops of G1;
G2 is removeDParallelEdges of H by Th122;
then consider G3 being removeParallelEdges of H such that
A1: G3 is removeParallelEdges of G2 by Th96;
reconsider G3 as SimpleGraph of G1 by Th117;
take G3;
thus thesis by A1, Th123;
end;
theorem
for G1 being _Graph, G3 being SimpleGraph of G1
ex G2 being DSimpleGraph of G1 st G3 is SimpleGraph of G2
proof
let G1 be _Graph, G3 be SimpleGraph of G1;
set H = the removeLoops of G1;
G3 is removeParallelEdges of H by Th121;
then consider G2 being removeDParallelEdges of H such that
A1: G3 is removeParallelEdges of G2 by Th97;
reconsider G2 as DSimpleGraph of G1 by Th118;
take G2;
thus thesis by A1, Th123;
end;
registration
let G be complete _Graph;
cluster -> complete for SimpleGraph of G;
coherence
proof
let G3 be SimpleGraph of G;
consider G2 being removeParallelEdges of G such that
A1: G3 is removeLoops of G2 by Th119;
thus thesis by A1;
end;
cluster -> complete for DSimpleGraph of G;
coherence
proof
let G3 be DSimpleGraph of G;
consider G2 being removeDParallelEdges of G such that
A2: G3 is removeLoops of G2 by Th120;
thus thesis by A2;
end;
end;
theorem Th136:
for G1 being _Graph, G2 being SimpleGraph of G1, W1 being Walk of G1
ex W2 being Walk of G2 st W2 is_Walk_from W1.first(),W1.last()
proof
let G1 be _Graph, G2 be SimpleGraph of G1, W1 be Walk of G1;
consider H being removeParallelEdges of G1 such that
A1: G2 is removeLoops of H by Th119;
consider W2 being Walk of H such that
A2: W2 is_Walk_from W1.first(),W1.last() by Lm4;
consider W3 being Walk of G2 such that
A3: W3 is_Walk_from W2.first(),W2.last() by A1, Th61;
take W3;
W1.first()=W2.first() & W1.last()=W2.last() by A2, GLIB_001:def 23;
hence thesis by A3;
end;
theorem Th137:
for G1 being _Graph, G2 being DSimpleGraph of G1, W1 being Walk of G1
ex W2 being Walk of G2 st W2 is_Walk_from W1.first(),W1.last()
proof
let G1 be _Graph, G2 be DSimpleGraph of G1, W1 be Walk of G1;
set G3 = the SimpleGraph of G2;
G3 is SimpleGraph of G1 by Th133;
then consider W3 being Walk of G3 such that
A1: W3 is_Walk_from W1.first(),W1.last() by Th136;
reconsider W2 = W3 as Walk of G2 by GLIB_001:167;
take W2;
thus thesis by A1, GLIB_001:19;
end;
theorem Th138:
for G1 being _Graph, G2 being SimpleGraph of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2)
proof
let G1 be _Graph, G2 be SimpleGraph of G1;
for W1 being Walk of G1 ex W2 being Walk of G2
st W2 is_Walk_from W1.first(),W1.last() by Th136;
hence for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2) by Th35;
end;
theorem Th139:
for G1 being _Graph, G2 being DSimpleGraph of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2)
proof
let G1 be _Graph, G2 be DSimpleGraph of G1;
for W1 being Walk of G1 ex W2 being Walk of G2
st W2 is_Walk_from W1.first(),W1.last() by Th137;
hence for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2) by Th35;
end;
registration
let G be connected _Graph;
cluster -> connected for SimpleGraph of G;
coherence
proof
let G2 be SimpleGraph of G;
for W1 being Walk of G ex W2 being Walk of G2
st W2 is_Walk_from W1.first(),W1.last() by Th136;
hence thesis by Th36;
end;
cluster -> connected for DSimpleGraph of G;
coherence
proof
let G2 be DSimpleGraph of G;
for W1 being Walk of G ex W2 being Walk of G2
st W2 is_Walk_from W1.first(),W1.last() by Th137;
hence thesis by Th36;
end;
end;
registration
let G be non connected _Graph;
cluster -> non connected for SimpleGraph of G;
coherence
proof
let G2 be SimpleGraph of G;
consider E being RepEdgeSelection of G such that
A1: G2 is inducedSubgraph of G, the_Vertices_of G, E\G.loops() by Def9;
thus thesis by A1, Th33;
end;
cluster -> non connected for DSimpleGraph of G;
coherence
proof
let G2 be DSimpleGraph of G;
consider E being RepDEdgeSelection of G such that
A2: G2 is inducedSubgraph of G, the_Vertices_of G, E\G.loops() by Def10;
thus thesis by A2, Th33;
end;
end;
theorem
for G1 being _Graph, G2 being SimpleGraph of G1
holds G1.componentSet() = G2.componentSet()
proof
let G1 be _Graph, G2 be SimpleGraph of G1;
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2) by Th138;
hence thesis by Th37;
end;
theorem
for G1 being _Graph, G2 being DSimpleGraph of G1
holds G1.componentSet() = G2.componentSet()
proof
let G1 be _Graph, G2 be DSimpleGraph of G1;
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2) by Th139;
hence thesis by Th37;
end;
theorem
for G1 being _Graph, G2 being SimpleGraph of G1
holds G1.numComponents() = G2.numComponents()
proof
let G1 be _Graph, G2 be SimpleGraph of G1;
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2) by Th138;
hence thesis by Th38;
end;
theorem
for G1 being _Graph, G2 being DSimpleGraph of G1
holds G1.numComponents() = G2.numComponents()
proof
let G1 be _Graph, G2 be DSimpleGraph of G1;
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2) by Th139;
hence thesis by Th38;
end;
theorem Th144:
for G1 being _Graph, G2 being SimpleGraph of G1
holds G1 is chordal iff G2 is chordal
proof
let G1 be _Graph, G2 be SimpleGraph of G1;
consider H being removeParallelEdges of G1 such that
A1: G2 is removeLoops of H by Th119;
H is chordal iff G2 is chordal by A1, Th65;
hence thesis by Th106;
end;
theorem Th145:
for G1 being _Graph, G2 being DSimpleGraph of G1
holds G1 is chordal iff G2 is chordal
proof
let G1 be _Graph, G2 be DSimpleGraph of G1;
consider H being removeDParallelEdges of G1 such that
A1: G2 is removeLoops of H by Th120;
H is chordal iff G2 is chordal by A1, Th65;
hence thesis by Th107;
end;
:: non chordal cluster after non chordal has been clustered with cycles
registration
let G be chordal _Graph;
cluster -> chordal for SimpleGraph of G;
coherence by Th144;
cluster -> chordal for DSimpleGraph of G;
coherence by Th145;
end;
theorem
for G1 being _Graph, G2 being SimpleGraph of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds v1 is cut-vertex iff v2 is cut-vertex
proof
let G1 be _Graph, G2 be SimpleGraph of G1;
consider H being removeParallelEdges of G1 such that
A1: G2 is removeLoops of H by Th119;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A2: v1 = v2;
reconsider v3 = v2 as Vertex of H by A1, GLIB_000:def 33;
v3 is cut-vertex iff v2 is cut-vertex by A1, Th67;
hence thesis by A2, Th109;
end;
theorem
for G1 being _Graph, G2 being DSimpleGraph of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds v1 is cut-vertex iff v2 is cut-vertex
proof
let G1 be _Graph, G2 be DSimpleGraph of G1;
consider H being removeDParallelEdges of G1 such that
A1: G2 is removeLoops of H by Th120;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A2: v1 = v2;
reconsider v3 = v2 as Vertex of H by A1, GLIB_000:def 33;
v3 is cut-vertex iff v2 is cut-vertex by A1, Th67;
hence thesis by A2, Th110;
end;
theorem
for G1 being loopless _Graph, G2 being SimpleGraph of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds v1 is isolated iff v2 is isolated
proof
let G1 be loopless _Graph, G2 be SimpleGraph of G1;
consider H being removeParallelEdges of G1 such that
A1: G2 is removeLoops of H by Th119;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A2: v1 = v2;
reconsider v3 = v2 as Vertex of H by A1, GLIB_000:def 33;
G2 == H by A1, Th58;
then v3 is isolated iff v2 is isolated by GLIB_000:97;
hence thesis by A2, Th111;
end;
theorem
for G1 being loopless _Graph, G2 being DSimpleGraph of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds v1 is isolated iff v2 is isolated
proof
let G1 be loopless _Graph, G2 be DSimpleGraph of G1;
consider H being removeDParallelEdges of G1 such that
A1: G2 is removeLoops of H by Th120;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A2: v1 = v2;
reconsider v3 = v2 as Vertex of H by A1, GLIB_000:def 33;
G2 == H by A1, Th58;
then v3 is isolated iff v2 is isolated by GLIB_000:97;
hence thesis by A2, Th112;
end;
theorem
for G1 being _Graph, G2 being SimpleGraph of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & v1 is endvertex holds v2 is endvertex
proof
let G1 be _Graph, G2 be SimpleGraph of G1;
consider H being removeParallelEdges of G1 such that
A1: G2 is removeLoops of H by Th119;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A2: v1 = v2 & v1 is endvertex;
reconsider v3 = v2 as Vertex of H by A1, GLIB_000:def 33;
v3 is endvertex by A2, Th113;
hence v2 is endvertex by A1, Th68;
end;
theorem
for G1 being _Graph, G2 being DSimpleGraph of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & v1 is endvertex holds v2 is endvertex
proof
let G1 be _Graph, G2 be DSimpleGraph of G1;
consider H being removeDParallelEdges of G1 such that
A1: G2 is removeLoops of H by Th120;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A2: v1 = v2 & v1 is endvertex;
reconsider v3 = v2 as Vertex of H by A1, GLIB_000:def 33;
v3 is endvertex by A2, Th114;
hence v2 is endvertex by A1, Th68;
end;