:: Miscellaneous Graph Preliminaries, {I}
:: by Sebastian Koch
::
:: Received March 30, 2021
:: Copyright (c) 2021-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, RELAT_1, FUNCT_1, XBOOLE_0, TARSKI, SUBSET_1, FINSEQ_1,
NAT_1, FUNCT_4, FUNCOP_1, ZFMISC_1, CARD_1, ARYTM_3, CARD_2, ORDINAL2,
XXREAL_0, PBOOLE, GLIB_000, RING_3, GLIB_002, PARTFUN1, FUNCT_2, CHORD,
SCMYCIEL, REWRITE1, ARYTM_1, GLIB_006, GLIB_007, GLIB_009, GLIB_010,
GLIB_012, WAYBEL_0, MOD_4, RELAT_2, GRAPH_1, GLIB_001, ABIAN, SGRAPH1,
TREES_1, MSUALG_6, EQREL_1, GLIB_013, GLIB_014, RCOMP_1, MSAFREE2,
FUNCT_7, HELLY, INT_1, TAXONOM2, CARD_3, AOFA_I00;
notations TARSKI, XBOOLE_0, ENUMSET1, XTUPLE_0, ZFMISC_1, SUBSET_1, SETFAM_1,
RELAT_1, FUNCT_1, RELAT_2, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2,
BINOP_1, DOMAIN_1, FUNCT_3, FUNCOP_1, FUNCT_4, CARD_1, PBOOLE, ORDERS_1,
CARD_3, NUMBERS, XXREAL_0, XREAL_0, XCMPLX_0, NAT_1, INT_1, VALUED_0,
NAT_D, CARD_2, FINSEQ_1, EQREL_1, NEWTON, ABIAN, FINSEQ_6, GLIB_000,
FINSEQ_8, GRAPH_2, TAXONOM2, COMPUT_1, GLIB_001, GLIB_002, CHORD, HELLY,
AOFA_I00, GLIB_006, GLIB_007, GLIB_008, GLIB_009, GLIB_010, GLIB_011,
GLIBPRE0, GLIB_012, GLIB_013, GLIB_014, GLUNIR00;
constructors DOMAIN_1, FUNCT_4, NAT_1, NAT_D, BINOP_2, CARD_2, FINSEQ_4,
PBOOLE, ORDINAL3, WELLORD2, PARTFUN1, RELSET_1, SQUARE_1, GLIB_000,
NEWTON, XTUPLE_0, CHORD, GLIB_002, GLIB_006, GLIB_007, GLIB_008,
GLIB_009, GLIB_010, GLIB_011, GLIB_001, ABIAN, BINOP_1, FINSOP_1,
RVSUM_1, FINSEQ_5, GRAPH_5, FUNCT_2, FIB_NUM2, FINSEQ_8, HELLY, FUNCT_3,
GRAPH_2, FINSEQ_6, FUNCT_7, FINSEQ_1, SUBSET_1, RELAT_1, ENUMSET1,
ORDINAL1, INT_1, XXREAL_0, XREAL_0, XCMPLX_0, GLIB_012, PARTFUN2,
ORDERS_1, TOLER_1, TAXONOM2, SETFAM_1, COMPUT_1, EQREL_1, GLIBPRE0,
GLIB_013, GLIB_014, GLUNIR00, WELLORD1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
FINSET_1, XREAL_0, NAT_1, CARD_1, FINSEQ_1, FINSEQ_4, FUNCT_2, PARTFUN1,
RELSET_1, GLIB_000, CHORD, GLIB_002, GLIB_006, GLIB_007, GLIB_009,
GLIB_008, GLIB_010, GLIB_011, SQUARE_1, NEWTON, XTUPLE_0, ABIAN,
GLIB_001, NUMBERS, MEMBERED, INT_1, CARD_3, RFINSEQ, GRAPH_2, GLIB_012,
SETFAM_1, COMPUT_1, ZFMISC_1, OPOSET_1, RELAT_2, GLIBPRE0, GLIB_013,
GLIB_014, ORDERS_1, ORDINAL5, EQREL_1, MSAFREE5, PRE_POLY;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
equalities SUBSET_1, GLIB_000, GLIB_001, GLIB_010, GLUNIR00;
theorems GLIB_000, CHORD, GLIB_002, GLIB_006, GLIB_007, GLIB_009, GLIB_010,
TARSKI, ZFMISC_1, FUNCT_1, XBOOLE_0, XBOOLE_1, FUNCT_2, XREGULAR,
PARTFUN1, SUBSET_1, FUNCT_4, GLIB_001, RELAT_1, CARD_1, CARD_2, XTUPLE_0,
FUNCOP_1, FINSEQ_1, FINSEQ_3, XXREAL_0, GLIB_008, XREAL_1, NAT_1,
ENUMSET1, ORDINAL1, GLIB_012, COMPUT_1, RELAT_2, POLYFORM, EQREL_1,
FUNCT_3, GLIBPRE0, GLIB_014, ORDERS_1, HELLY, INT_1, ABIAN, NAT_D,
COMBGRAS, FRECHET, PARTIT1, TAXONOM2, SCMYCIEL, GLUNIR00, AOFA_I00,
CARD_3, PARTIT_2, GLIB_013, FUNCT_7;
schemes FUNCT_1, FUNCT_2, NAT_1, GLIB_009;
begin :: Preliminaries not directly related to graphs
:: Proof mostly copied from XREGULAR:10
:: into XREGULAR ?
theorem
for X1, X2, X3, X4, X5, X6, X7 being set
holds not (X1 in X2 & X2 in X3 & X3 in X4 & X4 in X5 & X5 in X6 & X6 in X7 &
X7 in X1)
proof
let X1, X2, X3, X4, X5, X6, X7 be set;
assume that
A1: X1 in X2 and
A2: X2 in X3 and
A3: X3 in X4 and
A4: X4 in X5 and
A5: X5 in X6 and
A6: X6 in X7 and
A7: X7 in X1;
set Z = { X1,X2,X3,X4,X5,X6,X7 };
for Y being set st Y in Z holds Z meets Y
proof
let Y be set such that
A9: Y in Z;
now
per cases by A9,ENUMSET1:def 5;
suppose
A10: Y = X1;
take y = X7;
thus y in Z & y in Y by A7,A10,ENUMSET1:def 5;
end;
suppose
A11: Y = X2;
take y = X1;
thus y in Z & y in Y by A1,A11,ENUMSET1:def 5;
end;
suppose
A12: Y = X3;
take y = X2;
thus y in Z & y in Y by A2,A12,ENUMSET1:def 5;
end;
suppose
A13: Y = X4;
take y = X3;
thus y in Z & y in Y by A3,A13,ENUMSET1:def 5;
end;
suppose
A14: Y = X5;
take y = X4;
thus y in Z & y in Y by A4,A14,ENUMSET1:def 5;
end;
suppose
A15: Y = X6;
take y = X5;
thus y in Z & y in Y by A5,A15,ENUMSET1:def 5;
end;
suppose
A16: Y = X7;
take y = X6;
thus y in Z & y in Y by A6,A16,ENUMSET1:def 5;
end;
end;
hence thesis by XBOOLE_0:3;
end;
hence contradiction by XREGULAR:1;
end;
:: Proof mostly copied from XREGULAR:10
:: into XREGULAR ?
theorem
for X1, X2, X3, X4, X5, X6, X7, X8 being set
holds not (X1 in X2 & X2 in X3 & X3 in X4 & X4 in X5 & X5 in X6 & X6 in X7 &
X7 in X8 & X8 in X1)
proof
let X1, X2, X3, X4, X5, X6, X7, X8 be set;
assume that
A1: X1 in X2 and
A2: X2 in X3 and
A3: X3 in X4 and
A4: X4 in X5 and
A5: X5 in X6 and
A6: X6 in X7 and
A7: X7 in X8 and
A8: X8 in X1;
set Z = { X1,X2,X3,X4,X5,X6,X7,X8 };
for Y being set st Y in Z holds Z meets Y
proof
let Y be set such that
A10: Y in Z;
now
per cases by A10,ENUMSET1:def 6;
suppose
A11: Y = X1;
take y = X8;
thus y in Z & y in Y by A8,A11,ENUMSET1:def 6;
end;
suppose
A12: Y = X2;
take y = X1;
thus y in Z & y in Y by A1,A12,ENUMSET1:def 6;
end;
suppose
A13: Y = X3;
take y = X2;
thus y in Z & y in Y by A2,A13,ENUMSET1:def 6;
end;
suppose
A14: Y = X4;
take y = X3;
thus y in Z & y in Y by A3,A14,ENUMSET1:def 6;
end;
suppose
A15: Y = X5;
take y = X4;
thus y in Z & y in Y by A4,A15,ENUMSET1:def 6;
end;
suppose
A16: Y = X6;
take y = X5;
thus y in Z & y in Y by A5,A16,ENUMSET1:def 6;
end;
suppose
A17: Y = X7;
take y = X6;
thus y in Z & y in Y by A6,A17,ENUMSET1:def 6;
end;
suppose
A18: Y = X8;
take y = X7;
thus y in Z & y in Y by A7,A18,ENUMSET1:def 6;
end;
end;
hence thesis by XBOOLE_0:3;
end;
hence contradiction by XREGULAR:1;
end;
:: into FUNCT_1 ?
registration
cluster one-to-one constant -> trivial for Function;
coherence
proof
let f be Function;
assume A1: f is one-to-one constant;
set x = the Element of dom f;
now
let x9,y9 be object;
assume [x9,y9] in f;
then A2: x9 in dom f & f.x9 = y9 by FUNCT_1:1;
then f.x9 = f.x by A1, FUNCT_1:def 10;
then x = x9 by A1, A2, FUNCT_1:def 4;
hence [x9,y9] in {[x,f.x]} by A2, TARSKI:def 1;
end;
then f c= {[x,f.x]} by RELAT_1:def 3;
hence thesis;
end;
end;
:: into FUNCT_1 ?
theorem
for f being Function
holds f is non empty constant iff ex y being object st rng f = {y}
proof
let f be Function;
hereby
assume A1: f is non empty constant;
set Y = the Element of rng f;
reconsider y = Y as object;
consider x being object such that
A2: x in dom f & f.x = y by A1, FUNCT_1:def 3;
take y;
now
let y2 be object;
assume y2 in rng f;
then consider x2 being object such that
A3: x2 in dom f & f.x2 = y2 by FUNCT_1:def 3;
f.x = f.x2 by A1, A2, A3, FUNCT_1:def 10;
hence y2 in {y} by A2, A3, TARSKI:def 1;
end;
hence rng f = {y} by A1, TARSKI:def 3, ZFMISC_1:33;
end;
given y being object such that
A4: rng f = {y};
thus f is non empty by A4;
now
let x1, x2 be object;
assume x1 in dom f & x2 in dom f;
then f.x1 in rng f & f.x2 in rng f by FUNCT_1:3;
then f.x1 = y & f.x2 = y by A4, TARSKI:def 1;
hence f.x1 = f.x2;
end;
hence f is constant by FUNCT_1:def 10;
end;
:: into PBOOLE ?
registration
let X be set;
cluster one-to-one for ManySortedSet of X;
existence
proof
take id X;
thus thesis;
end;
end;
:: into PBOOLE ?
registration
let X be set;
cluster total one-to-one for X-defined Function;
existence
proof
take id X;
thus thesis;
end;
end;
:: into PBOOLE ?
registration
let X be non empty set;
cluster total one-to-one non empty for X-defined Function;
existence
proof
take id X;
thus thesis;
end;
end;
:: this is a variant of FUNCT_2:sch 4 which can be used a little bit easier
:: into FUNCT_2 ?
scheme
LambdaDf {C, D() -> non empty set, F(Element of C()) -> object} :
ex f being Function of C(),D() st
for x being Element of C() holds f.x=F(x)
provided
A1: for x being Element of C() holds F(x) in D()
proof
defpred P[object,object] means $2 = F(In($1,C()));
A2: for x being Element of C() ex y being Element of D() st P[x,y]
proof
let x be Element of C();
reconsider y = F(x) as Element of D() by A1;
take y;
thus thesis;
end;
consider f being Function of C(),D() such that
A3: for x being Element of C() holds P[x,f.x] from FUNCT_2:sch 3(A2);
take f;
let x be Element of C();
In(x,C()) = x;
hence thesis by A3;
end;
:: into FUNCOP_1 ?
theorem
for f being one-to-one Function, y being object st rng f = {y}
ex x being object st f = x .--> y
proof
let f be one-to-one Function, y be object;
assume A1: rng f = {y};
then y in rng f by TARSKI:def 1;
then consider x being object such that
A2: x in dom f & f.x = y by FUNCT_1:def 3;
take x;
f is constant by A1;
then dom f = {x} by A2, ZFMISC_1:132;
hence thesis by A1, FUNCT_4:112;
end;
:: into FUNCOP_1 ?
registration
let f be one-to-one Function;
cluster f~ -> one-to-one;
coherence
proof
now
let x1,x2 be object;
assume A1: x1 in dom(f~) & x2 in dom(f~) & f~.x1 = f~.x2;
then A2: x1 in dom f & x2 in dom f by FUNCOP_1:def 1;
then per cases by FUNCOP_1:def 1;
suppose A3: f.x1 = f~.x1 & for y1,z1 being object holds f.x1 <> [y1,z1];
f.x2 = f~.x2
proof
assume f.x2 <> f~.x2;
then consider y2,z2 being object such that
A4: f.x2 = [y2,z2] by A2, FUNCOP_1:def 1;
[z2,y2] = f~.x1 by A1, A2, A4, FUNCOP_1:def 1;
then [y2,z2] = f~~.x1 by A1, FUNCOP_1:def 1
.= f.x1;
hence contradiction by A3;
end;
hence x1 = x2 by A1, A2, A3, FUNCT_1:def 4;
end;
suppose ex y1,z1 being object st f.x1 = [y1,z1];
then consider y1,z1 being object such that
A5: f.x1 = [y1,z1];
[z1,y1] = f~.x2 by A1, A2, A5, FUNCOP_1:def 1;
then [y1,z1] = f~~.x2 by A1, FUNCOP_1:def 1
.= f.x2;
hence x1 = x2 by A2, A5, FUNCT_1:def 4;
end;
end;
hence thesis by FUNCT_1:def 4;
end;
end;
:: into FUNCT_3 or FUNCOP_1 ?
registration
let f be Function, g be one-to-one Function;
cluster <: f,g :> -> one-to-one;
coherence
proof
set h = <: f,g :>;
now
let x1,x2 be object;
assume A1: x1 in dom h & x2 in dom h & h.x1 = h.x2;
then x1 in dom f /\ dom g & x2 in dom f /\ dom g by FUNCT_3:def 7;
then A2: x1 in dom g & x2 in dom g by XBOOLE_0:def 4;
[f.x1,g.x1] = h.x1 & [f.x2,g.x2] = h.x2 by A1, FUNCT_3:def 7;
then g.x1 = g.x2 by A1, XTUPLE_0:1;
hence x1 = x2 by A2, FUNCT_1:def 4;
end;
hence thesis by FUNCT_1:def 4;
end;
cluster <: g,f :> -> one-to-one;
coherence
proof
<: g,f :> = <: f,g :>~ by FUNCOP_1:2;
hence thesis;
end;
end;
:: into FUNCT_3 or FUNCOP_1 ?
theorem Th5:
for f being empty Function holds .:f = {} .--> {}
proof
let f be empty Function;
A1: dom(.:f) = bool dom f by FUNCT_3:def 1
.= {{}} by ZFMISC_1:1;
then A2: dom(.:f) = dom {[{},{}]} by RELAT_1:9
.= dom({} .--> {}) by FUNCT_4:82;
now
let x be object;
assume x in dom(.:f);
then A3: x = {} by A1, TARSKI:def 1;
hence (.:f).x = {} by FUNCT_3:8
.= ({} .--> {}).x by A3, FUNCOP_1:72;
end;
hence thesis by A2, FUNCT_1:2;
end;
:: into FUNCT_3 ?
registration
let f be one-to-one Function;
cluster .:f -> one-to-one;
coherence
proof
per cases;
suppose A1: f <> {};
reconsider f0 = f as Function of dom f, rng f by FUNCT_2:1;
now
let x1,x2 be object;
assume A2: x1 in dom .:f & x2 in dom .:f & (.:f).x1 = (.:f).x2;
then reconsider X1 = x1, X2 = x2 as Subset of dom f by FUNCT_3:def 1;
(.:f).x1 = f.:X1 & (.:f).x2 = f.:X2 by A2, FUNCT_3:7;
then f0.:X1 = f0.:X2 by A2;
hence x1 = x2 by A1, COMBGRAS:6;
end;
hence thesis by FUNCT_1:def 4;
end;
suppose f = {};
hence thesis by Th5;
end;
end;
end;
:: into FUNCT_3 ?
theorem Th6:
for f being non empty one-to-one Function
for X being non empty Subset of bool dom f
holds rng((.:f)|X) = the set of all f.:x where x is Element of X
proof
let f be non empty one-to-one Function, X be non empty Subset of bool dom f;
set S = the set of all f.:x where x is Element of X;
now
let y be object;
hereby
assume y in S;
then consider x9 being Element of X such that
A1: y = f.:x9;
reconsider x = x9 as object;
take x;
x in bool dom f;
then A2: x in dom(.:f) by FUNCT_3:def 1;
hence x in dom((.:f)|X) by RELAT_1:57;
thus y = (.:f).x by A1, A2, FUNCT_3:7
.= ((.:f)|X).x by FUNCT_1:49;
end;
given x being object such that
A3: x in dom((.:f)|X) & y = ((.:f)|X).x;
A4: x in dom(.:f) & x in X by A3, RELAT_1:57;
then reconsider x9 = x as Element of X;
y = (.:f).x by A3, FUNCT_1:47
.= f.:x9 by A4, FUNCT_3:7;
hence y in S;
end;
hence thesis by FUNCT_1:def 3;
end;
:: into FUNCT_4 ?
theorem
for f being Function, g, h being one-to-one Function
st h = f +* g holds h"|rng g = g"
proof
let f be Function, g, h be one-to-one Function;
assume A1: h = f +* g;
A2: dom(h"|rng g) = dom(h") /\ rng g by RELAT_1:61
.= rng h /\ rng g by FUNCT_1:33
.= (f.:(dom f\dom g) \/ rng g) /\ rng g by A1, FRECHET:12
.= rng g by XBOOLE_1:21
.= dom(g") by FUNCT_1:33;
now
let y be object;
assume y in dom(g");
then A3: y in rng g by FUNCT_1:33;
then consider x being object such that
A4: x in dom g & g.x = y by FUNCT_1:def 3;
dom h = dom f \/ dom g by A1, FUNCT_4:def 1;
then A5: x in dom h by A4, XBOOLE_0:def 3;
thus g".y = x by A4, FUNCT_1:34
.= h".(h.x) by A5, FUNCT_1:34
.= h".y by A1, A4, FUNCT_4:13
.= (h"|rng g).y by A3, FUNCT_1:49;
end;
hence thesis by A2, FUNCT_1:2;
end;
:: special case of FUNCT_7:10, compare FUNCT_7:9, FUNCT_7:11
:: into FUNCT_4 ?
theorem Th8:
for f, g, h being Function st rng f c= dom h holds (g +* h)*f = h*f
proof
let f, g, h be Function;
assume A1: rng f c= dom h;
then rng f c= dom g \/ dom h by XBOOLE_1:10;
then rng f c= dom(g +* h) by FUNCT_4:def 1;
then A2: dom((g +* h)*f) = dom f by RELAT_1:27
.= dom(h*f) by A1, RELAT_1:27;
now
let x be object;
assume A3: x in dom((g +* h)*f);
then A4: x in dom f by FUNCT_1:11;
then A5: f.x in rng f by FUNCT_1:3;
thus ((g +* h)*f).x = (g +* h).(f.x) by A3, FUNCT_1:12
.= h.(f.x) by A1, A5, FUNCT_4:13
.= (h*f).x by A4, FUNCT_1:13;
end;
hence thesis by A2, FUNCT_1:2;
end;
:: into FUNCT_4 ?
theorem
for f being Function, g being one-to-one Function
holds (f +* g)*(g") = id rng g
proof
let f be Function, g be one-to-one Function;
rng(g") = dom g by FUNCT_1:33;
hence (f +* g)*(g") = g*g" by Th8
.= id rng g by FUNCT_1:39;
end;
:: into RELAT_2 or ORDERS_1 ?
registration
cluster reflexive connected -> strongly_connected for Relation;
coherence
proof
let R be Relation;
assume R is reflexive connected;
then R is_connected_in field R & R is_reflexive_in field R
by RELAT_2:def 9, RELAT_2:def 14;
hence thesis by ORDERS_1:7, RELAT_2:def 15;
end;
end;
:: into RELSET_1 or ORDERS_1 ?
theorem
for X being set, R being Relation of X
holds R is antisymmetric iff R \ id X is asymmetric
proof
let X be set, R be Relation of X;
per cases;
suppose A1: X is non empty;
hereby
assume R is antisymmetric;
then R is_antisymmetric_in X by A1, PARTIT_2:24;
hence R \ id X is asymmetric by A1, RELAT_2:3, PARTIT_2:29;
end;
assume R \ id X is asymmetric;
then R \ id X is_asymmetric_in X by A1, PARTIT_2:28;
hence R is antisymmetric by A1, RELAT_2:3, PARTIT_2:25;
end;
suppose X is empty;
hence thesis;
end;
end;
:: into EQREL_1 or TAXONOM2 ?
theorem Th11:
for X being set st X is mutually-disjoint
holds X \ {{}} is a_partition of union X
proof
let X be set;
assume A1: X is mutually-disjoint;
now
let x be object;
reconsider y = x as set by TARSKI:1;
assume x in X \ {{}};
then y c= union X by ZFMISC_1:74;
hence x in bool union X;
end;
then A2: X \ {{}} is Subset of bool union X by TARSKI:def 3;
now
thus union (X \ {{}}) = union X by PARTIT1:2;
let A be Subset of union X;
assume A3: A in X \ {{}};
then not A in {{}} by XBOOLE_0:def 5;
hence A <> {} by TARSKI:def 1;
let B be Subset of union X;
assume B in X \ {{}} & A <> B;
hence A misses B by A1, A3, TAXONOM2:def 5;
end;
hence thesis by A2, EQREL_1:def 4;
end;
:: into EQREL_1 or TAXONOM2 ?
registration
let X be set;
cluster -> mutually-disjoint for a_partition of X;
coherence
proof
let P be a_partition of X;
for x,y being set st x in P & y in P & x <> y holds x misses y
by EQREL_1:def 4;
hence thesis by TAXONOM2:def 5;
end;
end;
:: compare CARD_2:86, Proof mostly copied from there
:: into CARD_2 ?
theorem Th12:
for M,N being Cardinal, f being Function holds
(M c= card dom f & for x being object st x in dom f
holds N c= card (f.x)) implies M*`N c= Sum Card f
proof
let M,N being Cardinal, f being Function;
assume that
A1: M c= card dom f and
A2: for x being object st x in dom f holds N c= card (f.x);
A3: dom Card f = dom f by CARD_3:def 2;
A4: dom(dom f --> N) = dom f;
now
let x be object;
assume
A5: x in dom Card f;
then
A6: (Card f).x = card (f.x) by A3,CARD_3:def 2;
(dom f --> N).x = N by A3,A5,FUNCOP_1:7;
hence (dom f --> N).x c= (Card f).x by A2,A3,A5,A6;
end;
then
A7: Sum(dom f --> N) c= Sum Card f by A3,A4,CARD_3:30;
A8: [:M,N:] c= [:card dom f,N:] by A1,ZFMISC_1:95;
Sum(dom f --> N) = card Union disjoin (dom f --> N) by CARD_3:def 7
.= card [:N,dom f:] by CARD_3:25
.= card [:N,card dom f:] by CARD_2:7
.= card [:card dom f,N:] by CARD_2:4;
then card [:M,N:] c= Sum(dom f --> N) by A8,CARD_1:11;
then card [:M,N:] c= Sum Card f by A7,XBOOLE_1:1;
hence thesis by CARD_2:def 2;
end;
:: into CARD_3 ?
theorem Th13:
for X, x being set st x in X holds (disjoin Card id X).x = [: card x, {x} :]
proof
let X, x be set;
assume A1: x in X;
then A2: x in dom id X;
then x in dom Card id X by CARD_3:def 2;
hence (disjoin Card id X).x = [: (Card id X).x, {x} :] by CARD_3:def 3
.= [: card ((id X).x), {x} :] by A2, CARD_3:def 2
.= [: card x, {x} :] by A1, FUNCT_1:18;
end;
:: into CARD_3 or TAXONOM2 ?
theorem Th14:
for X being set st X is mutually-disjoint holds Sum Card id X = card union X
proof
let X be set;
set D = disjoin Card id X;
assume A1: X is mutually-disjoint;
per cases;
suppose A2: X <> {} & X <> {{}};
reconsider P = X \ {{}} as a_partition of union X by A1, Th11;
reconsider U = union X as non empty set by A2, SCMYCIEL:18;
reconsider P as non empty a_partition of U;
deffunc e(object) = the Enumeration of ((proj P).$1);
deffunc F(object) = [e($1).$1, (proj P).$1];
consider f being Function such that
A3: dom f = union X & for z being object st z in union X holds f.z = F(z)
from FUNCT_1:sch 3;
A4: dom D = dom Card id X by CARD_3:def 3
.= dom id X by CARD_3:def 2
.= X;
:: show that rng f = Union D
now
let y be object;
hereby
assume y in rng f;
then consider z being object such that
A5: z in dom f & f.z = y by FUNCT_1:def 3;
set x = (proj P).z;
A6: y = [e(z).z,x] by A3, A5;
A7: x in P by A3, A5, FUNCT_2:5;
then A8: D.x = [: card x, {x} :] by Th13;
A9: D.x in rng D by A4, A7, FUNCT_1:3;
y in D.x
proof
z in x by A3, A5, EQREL_1:def 9;
then z in dom e(z) by AOFA_I00:6;
then A10: e(z).z in rng e(z) by FUNCT_1:3;
x in {x} by TARSKI:def 1;
hence thesis by A6, A8, A10, ZFMISC_1:def 2;
end;
then y in union rng D by A9, TARSKI:def 4;
hence y in Union D by CARD_3:def 4;
end;
assume y in Union D;
then y in union rng D by CARD_3:def 4;
then consider Y being set such that
A11: y in Y & Y in rng D by TARSKI:def 4;
consider x being object such that
A12: x in dom D & D.x = Y by A11, FUNCT_1:def 3;
reconsider x as set by TARSKI:1;
y in [: card x, {x} :] by A4, A11, A12, Th13;
then consider a,b being object such that
A13: a in card x & b in {x} & y = [a,b] by ZFMISC_1:def 2;
a in rng the Enumeration of x by A13, AOFA_I00:6;
then consider z being object such that
A14: z in dom the Enumeration of x and
A15: (the Enumeration of x).z = a by FUNCT_1:def 3;
A16: z in x by A14;
then A17: z in U by A4, A12, TARSKI:def 4;
not x in {{}} by A16, TARSKI:def 1;
then x in P by A4, A12, XBOOLE_0:def 5;
then (proj P).z = x by A16, EQREL_1:65;
then a = e(z).z & b = (proj P).z by A13, A15, TARSKI:def 1;
then y = f.z by A3, A13, A17;
hence y in rng f by A3, A17, FUNCT_1:3;
end;
then A18: rng f = Union D by TARSKI:2;
:: show that f is one-to-one
now
let z1,z2 be object;
assume A19: z1 in dom f & z2 in dom f & f.z1 = f.z2;
then f.z1 = [e(z1).z1,(proj P).z1] & f.z2 = [e(z2).z2,(proj P).z2] by A3;
then A20: e(z1).z1 = e(z2).z2 & (proj P).z1 = (proj P).z2
by A19, XTUPLE_0:1;
then z1 in (proj P).z1 & z2 in (proj P).z1 by A3, A19, EQREL_1:def 9;
then z1 in dom e(z1) & z2 in dom e(z1) by AOFA_I00:6;
hence z1 = z2 by A20, FUNCT_1:def 4;
end;
then card Union D = card union X by A3, A18, CARD_1:70, FUNCT_1:def 4;
hence thesis by CARD_3:def 7;
end;
suppose A21: X = {};
set f = the empty Function;
thus Sum Card id X
= card Union disjoin Card id X by CARD_3:def 7
.= card union rng disjoin Card id X by CARD_3:def 4
.= card union rng disjoin f by A21
.= card union X by A21, CARD_3:3;
end;
suppose A22: X = {{}};
thus Sum Card id X
= card Union disjoin Card id X by CARD_3:def 7
.= card union rng disjoin Card id X by CARD_3:def 4
.= card union rng disjoin Card ({} .--> {}) by A22, FUNCT_4:96
.= card union rng disjoin Card (X --> {}) by A22, FUNCOP_1:def 9
.= card union rng disjoin (X --> card {}) by CARD_3:2
.= card union rng disjoin ({} .--> {}) by A22, FUNCOP_1:def 9
.= card union rng ({} .--> [:{},{{}}:]) by CARD_3:4
.= card union X by A22, FUNCOP_1:88;
end;
end;
:: compare CARD_2:87, Proof mostly copied from there
:: into CARD_2 ?
theorem
for X being set, M, N being Cardinal st X is mutually-disjoint &
M c= card X & for Y being set st Y in X holds N c= card Y
holds M*`N c= card union X
proof
let X be set, M,N be Cardinal;
assume that
A1: X is mutually-disjoint and
A2: M c= card X and
A3: for Y being set st Y in X holds N c= card Y;
now
let x be object;
assume x in dom id X;
then (id X).x in X by FUNCT_1:18;
hence N c= card ((id X).x) by A3;
end;
then M*`N c= Sum Card id X by A2,Th12;
hence thesis by A1, Th14;
end;
:: into COMPUT_1 ?
theorem
for F being compatible functional set
st (for f1 being Function st f1 in F holds f1 is one-to-one &
for f2 being Function st f2 in F & f1 <> f2 holds rng f1 misses rng f2)
holds union F is one-to-one
proof
let F be compatible functional set;
assume A1: for f1 being Function st f1 in F holds f1 is one-to-one &
for f2 being Function st f2 in F & f1 <> f2 holds rng f1 misses rng f2;
now
let x1, x2 be object;
assume A2: x1 in dom union F & x2 in dom union F &
(union F).x1 = (union F).x2;
then [x1,(union F).x1] in union F by FUNCT_1:1;
then consider X1 being set such that
A3: [x1,(union F).x1] in X1 & X1 in F by TARSKI:def 4;
reconsider f1 = X1 as Function by A3;
A4: x1 in dom f1 & f1.x1 = (union F).x1 by A3, FUNCT_1:1;
[x2,(union F).x2] in union F by A2, FUNCT_1:1;
then consider X2 being set such that
A5: [x2,(union F).x2] in X2 & X2 in F by TARSKI:def 4;
reconsider f2 = X2 as Function by A5;
A6: x2 in dom f2 & f2.x2 = (union F).x2 by A5, FUNCT_1:1;
then A7: f1.x1 = f2.x2 by A2, A4;
f1.x1 in rng f1 & f2.x2 in rng f2 by A4, A6, FUNCT_1:3;
then f1 = f2 by A1, A3, A5, A7, XBOOLE_0:3;
hence x1 = x2 by A1, A3, A4, A6, A7, FUNCT_1:def 4;
end;
hence thesis by FUNCT_1:def 4;
end;
begin :: into GLIB_000
::$CT 9
definition
let X be non empty set, f be Graph-yielding ManySortedSet of X;
let x be Element of X;
redefine func f.x -> _Graph; :: redefines . (FUNCT_1, definition)
coherence
proof
dom f = X & x in X by PARTFUN1:def 2;
hence thesis by GLIB_000:def 53;
end;
end;
begin :: into GLIB_001
Lm1:
for G being _Graph, P being Path of G
holds dom(P.vertexSeq() | P.length()) = Seg P.length()
proof
let G be _Graph, P be Path of G;
A1: P.length() + 0 <= P.length() + 1 by XREAL_1:6;
thus dom(P.vertexSeq() | P.length())
= dom (P.vertexSeq() | Seg P.length()) by FINSEQ_1:def 16
.= dom P.vertexSeq() /\ Seg P.length() by RELAT_1:61
.= Seg len P.vertexSeq() /\ Seg P.length() by FINSEQ_1:def 3
.= Seg(P.length() + 1) /\ Seg P.length() by GLIB_009:28
.= Seg P.length() by A1, FINSEQ_1:7;
end;
registration
let G being _Graph, P being Path of G;
cluster P.vertexSeq() | P.length() -> one-to-one;
coherence
proof
set f = P.vertexSeq() | P.length();
now
let x1, x2 be object;
A1: dom f = Seg P.length() by Lm1;
assume A2: x1 in dom f & x2 in dom f & f.x1 = f.x2;
then reconsider n1 = x1 as Nat;
A3: 1 <= n1 & n1 <= P.length() by A1, A2, FINSEQ_1:1;
reconsider n2 = x2 as Nat by A2;
A4: 1 <= n2 & n2 <= P.length() by A1, A2, FINSEQ_1:1;
P.length() + 0 <= P.length() + 1 by XREAL_1:6;
then P.length() + 0 <= len P.vertexSeq() by GLIB_009:28;
then A5: n1 <= len P.vertexSeq() & n2 <= len P.vertexSeq()
by A3, A4, XXREAL_0:2;
A6: f.n1 = (P.vertexSeq() | Seg P.length()).n1 by FINSEQ_1:def 16
.= P.vertexSeq().n1 by A1, A2, FUNCT_1:49
.= P.(2*n1 - 1) by A3, A5, GLIB_001:def 14;
f.n2 = (P.vertexSeq() | Seg P.length()).n2 by FINSEQ_1:def 16
.= P.vertexSeq().n2 by A1, A2, FUNCT_1:49
.= P.(2*n2 - 1) by A4, A5, GLIB_001:def 14;
then A7: P.(2*n1 - 1) = P.(2*n2 - 1) by A2, A6;
2*1 <= 2*n1 & 2*1 <= 2*n2 by A3, A4, XREAL_1:64;
then 2 - 1 <= 2*n1 - 1 & 2 - 1 <= 2*n2 - 1 by XREAL_1:9;
then reconsider m1 = 2*n1-1, m2 = 2*n2-1 as Element of NAT by INT_1:3;
A8: 2*n1 <= 2*P.length() & 2*n2 <= 2*P.length() by A3, A4, XREAL_1:64;
2*P.length() + 0 <= 2*P.length() + 2 by XREAL_1:6;
then 2*n1 <= 2*P.length()+2 & 2*n2 <= 2*P.length()+2 by A8, XXREAL_0:2;
then m1 <= 2*P.length()+2-1 & m2 <= 2*P.length()+2-1 by XREAL_1:9;
then m1 <= 2*P.length()+1 & m2 <= 2*P.length()+1;
then A9: m1 <= len P & m2 <= len P by GLIB_001:112;
assume x1 <> x2;
then per cases by XXREAL_0:1;
suppose n1 < n2;
then 2*n1 < 2*n2 by XREAL_1:68;
then m1 < m2 & m2 <= len P by A9, XREAL_1:9;
then m2 = len P by A7, GLIB_001:def 28
.= 2*P.length() + 1 by GLIB_001:112;
then 2*P.length() + 2 <= 2*P.length() + 0 by A8;
hence contradiction by XREAL_1:6;
end;
suppose n2 < n1;
then 2*n2 < 2*n1 by XREAL_1:68;
then m2 < m1 & m1 <= len P by A9, XREAL_1:9;
then m1 = len P by A7, GLIB_001:def 28
.= 2*P.length() + 1 by GLIB_001:112;
then 2*P.length() + 2 <= 2*P.length() + 0 by A8;
hence contradiction by XREAL_1:6;
end;
end;
hence thesis by FUNCT_1:def 4;
end;
end;
:: compare GLIB_001:154
theorem
for G being _Graph, P being Path of G holds P.length() c= G.order()
proof
let G be _Graph, P be Path of G;
A1: dom(P.vertexSeq() | P.length()) = Seg P.length() by Lm1;
rng(P.vertexSeq() | P.length()) c= the_Vertices_of G;
then card Seg P.length() c= card the_Vertices_of G by A1, CARD_1:10;
then card P.length() c= card the_Vertices_of G by FINSEQ_1:55;
hence thesis;
end;
:: compare GLIB_001:144
theorem
for G being _Graph, T being Trail of G holds T.length() c= G.size()
proof
let G be _Graph, T be Trail of G;
A1: dom T.edgeSeq() = Seg len T.edgeSeq() by FINSEQ_1:def 3
.= Seg T.length();
rng T.edgeSeq() c= the_Edges_of G & T.edgeSeq() is one-to-one
by GLIB_001:def 27;
then card Seg T.length() c= card the_Edges_of G by A1, CARD_1:10;
then card T.length() c= card the_Edges_of G by FINSEQ_1:55;
hence thesis;
end;
Lm2:
for G being _Graph, W being Walk of G st len W = 3
ex e being object st e Joins W.first(),W.last(),G &
W = G.walkOf(W.first(),e,W.last())
proof
let G be _Graph, W be Walk of G;
assume A1: len W = 3;
then A2: W.(1+1) Joins W.1,W.(1+2),G by GLIB_001:def 3, POLYFORM:4;
take W.2;
A3: W.1 = W.first() & W.3 = W.last() by A1;
hence A4: W.2 Joins W.first(),W.last(),G by A2;
thus W = <* W.1, W.2, W.3 *> by A1, FINSEQ_1:45
.= G.walkOf(W.first(),W.2,W.last()) by A3, A4, GLIB_001:def 5;
end;
theorem Th28:
for G being _Graph, W being Walk of G st len W = 3 or W.length() = 1
ex e being object st e Joins W.first(),W.last(),G &
W = G.walkOf(W.first(),e,W.last())
proof
let G be _Graph, W be Walk of G;
assume len W = 3 or W.length() = 1;
then per cases;
suppose len W = 3;
hence thesis by Lm2;
end;
suppose W.length() = 1;
then len W = 2*1 + 1 by GLIB_001:112;
hence thesis by Lm2;
end;
end;
theorem
for G being _Graph, W being Walk of G, e being object
st e in W.edges() & not e in G.loops() & W is Circuit-like
ex e0 being object st e0 in W.edges() & e0 <> e
proof
let G be _Graph, W be Walk of G, e be object;
assume A1: e in W.edges() & not e in G.loops() & W is Circuit-like;
then consider n being odd Element of NAT such that
A2: n < len W & W.(n+1) = e by GLIB_001:100;
A3: len W > 3
proof
assume len W <= 3;
then len W + 0 <= 3+1 by XREAL_1:7;
then per cases by CHORD:7;
suppose len W = 1;
then 2*W.length()+1 = 2*0+1 by GLIB_001:112;
hence contradiction by A1, GLIB_001:def 26;
end;
suppose len W = 3;
then 2*W.length()+1 = 2*1+1 by GLIB_001:112;
then consider e0 being object such that
A4: e0 Joins W.first(),W.last(),G & W = G.walkOf(W.first(),e0,W.last())
by Th28;
W.edges() = {e0} by A4, GLIB_001:108;
then A5: e = e0 by A1, TARSKI:def 1;
W.first() = W.last() by A1, GLIB_001:def 24;
hence contradiction by A1, A4, A5, GLIB_009:def 2;
end;
end;
per cases;
suppose A6: n = 1;
reconsider m=n+2 as odd Element of NAT;
take W.(m+1);
thus W.(m+1) in W.edges() by A3, A6, GLIB_001:100;
m+1 <= len W by A3, A6, NAT_1:13;
then W.(n+1) <> W.(m+1) by A1, A6, GLIB_001:138;
hence thesis by A2;
end;
suppose A7: n <> 1;
reconsider m=1 as odd Element of NAT by POLYFORM:4;
take W.(m+1);
m < len W by A3, XXREAL_0:2;
hence W.(m+1) in W.edges() by GLIB_001:100;
1 <= n by CHORD:2;
then m < n by A7, XXREAL_0:1;
then A8: m+1 < n+1 by XREAL_1:6;
n+1 < len W + 1 by A2, XREAL_1:6;
then n+1 <= len W by NAT_1:13;
then W.(n+1) <> W.(m+1) by A1, A8, GLIB_001:138;
hence thesis by A2;
end;
end;
:: compare GLIB_001:149 and CHORD:93
theorem Th30:
for G being _Graph, P being Path of G, n, m being odd Element of NAT
st n < m & m <= len P & (n <> 1 or m <> len P) holds P.cut(n,m) is open
proof
let G be _Graph, P be Path of G, n, m be odd Element of NAT;
assume A1: n < m & m <= len P & (n <> 1 or m <> len P);
then A2: P.cut(n,m).first() = P.n & P.cut(n,m).last()=P.m by GLIB_001:37;
assume P.cut(n,m) is closed;
then P.n = P.m by A2, GLIB_001:def 24;
hence contradiction by A1, GLIB_001:def 28;
end;
:: cutting a closed walk at an edge
theorem Th31:
for G being _Graph, W being closed Walk of G, n being odd Element of NAT
st n < len W holds
W.cut(n+2,len W).append(W.cut(1,n)) is_Walk_from W.(n+2),W.n &
(W is Trail-like implies
W.cut(n+2,len W).edges() misses W.cut(1,n).edges() &
W.cut(n+2,len W).append(W.cut(1,n)).edges() = W.edges() \ {W.(n+1)}) &
(W is Path-like implies
W.cut(n+2,len W).vertices() /\ W.cut(1,n).vertices() = {W.first()} &
(not W.(n+1) in G.loops()
implies W.cut(n+2,len W).append(W.cut(1,n)) is open) &
W.cut(n+2,len W).append(W.cut(1,n)) is Path-like)
proof
let G be _Graph, W be closed Walk of G, n be odd Element of NAT;
assume A1: n < len W;
set W7 = W.cut(n+2,len W), W8 = W.cut(1,n), W9 = W7.append(W8), e = W.(n+1);
A2: 0+1 <= n+1 & n+2 <= len W by A1, CHORD:4, XREAL_1:6;
then A3: W7 is_Walk_from W.(n+2), W.len W by GLIB_001:37;
A4: n <= len W by A1;
A5: 1 <= n & 1 is odd by CHORD:2, POLYFORM:4;
then A6: W8 is_Walk_from W.1, W.n by A4, GLIB_001:37;
A7: W.len W = W.last()
.= W.first() by GLIB_001:def 24
.= W.1;
hence W9 is_Walk_from W.(n+2),W.n by A3, A6, GLIB_001:31;
A8: W7.last() = W.len W & W8.first() = W.1 by A3, A6, GLIB_001:def 23;
then A9: len W9 + 1 = len W7 + len W8 by A7, GLIB_001:28;
A10: len W8 = n by A4, GLIB_001:45;
A11: len W7 + (n+2) = len W + 1 by A2, GLIB_001:36;
thus W is Trail-like implies
W7.edges() misses W8.edges() & W9.edges() = W.edges() \ {W.(n+1)}
proof
assume A12: W is Trail-like;
W7.edges() /\ W8.edges() = {}
proof
assume W7.edges() /\ W8.edges() <> {};
then consider x being object such that
A13: x in W7.edges() /\ W8.edges() by XBOOLE_0:def 1;
A14: x in W7.edges() & x in W8.edges() by A13, XBOOLE_0:def 4;
then consider n1 being odd Element of NAT such that
A15: n1 < len W7 & W7.(n1+1) = x by GLIB_001:100;
consider n2 being odd Element of NAT such that
A16: n2 < len W8 & W8.(n2+1) = x by A14, GLIB_001:100;
A17: W.(1+n2) = x by A4, A5, A16, GLIB_001:36
.= W.(n+2+n1) by A2, A15, GLIB_001:36;
1+0 <= 2+n1 by XREAL_1:7;
then A18: 1+n2 < 2+n1+n by A10, A16, XREAL_1:8;
n+2+n1 < n+2+len W7 by A15, XREAL_1:6;
then n+2+n1 < len W + 1 by A11;
then A19: n+2+n1 <= len W by NAT_1:13;
1+0 <= 1+n2 by XREAL_1:6;
hence contradiction by A12, A17, A18, A19, GLIB_001:138;
end;
hence W7.edges() misses W8.edges() by XBOOLE_0:def 7;
:: show that W satisfies the edges property (very technical)
now
let x be object;
:: first inclusion
hereby
assume x in W9.edges();
then consider m being odd Element of NAT such that
A20: m < len W9 & W9.(m+1) = x by GLIB_001:100;
m+1 in dom W9 by A20, GLIB_001:12;
then per cases by GLIB_001:34;
suppose A21: m+1 in dom W7;
then A22: x = W7.(m+1) by A20, GLIB_001:32
.= W.(n+2+(m+1)-1) by A2, A21, GLIB_001:47
.= W.(n+2+m);
n+2+(m+1)-1 in dom W by A2, A21, GLIB_001:47;
then A23: n+2+m <= len W by FINSEQ_3:25;
1+0 < 2+m by XREAL_1:8;
then n+1 < n+(2+m) by XREAL_1:8;
then A24: W.(n+1) <> W.(n+2+m) by A12, A2, A23, GLIB_001:138;
n+1+m+1 < len W + 1 by A23, NAT_1:13;
then x in W.edges() by A22, XREAL_1:6, GLIB_001:100;
hence x in W.edges()\{e} by A22, A24, ZFMISC_1:56;
end;
suppose ex k being Element of NAT st k < len W8 & m+1 = len W7 + k;
then consider k being Element of NAT such that
A25: k < len W8 & m+1 = len W7 + k;
A26: x = W8.(k+1) by A7, A8, A20, A25, GLIB_001:33
.= W.(1+k) by A4, A5, A25, GLIB_001:36;
A27: 1+0 <= k+1 by XREAL_1:6;
A28: k is odd by A25;
A29: k+1 < n+1 by A10, A25, XREAL_1:8;
n+1 <= len W by A1, NAT_1:13;
then W.(k+1) <> W.(n+1) by A12, A27, A28, A29, GLIB_001:138;
then A30: x <> e by A26;
k < len W by A1, A10, A25, XXREAL_0:2;
then x in W.edges() by A26, A28, GLIB_001:100;
hence x in W.edges()\{e} by A30, ZFMISC_1:56;
end;
end;
:: second inclusion
assume x in W.edges()\{e};
then A31: x in W.edges() & x <> e by ZFMISC_1:56;
then consider m being odd Element of NAT such that
A32: m < len W & W.(m+1) = x by GLIB_001:100;
per cases by A31, A32, XXREAL_0:1;
suppose A33: m < n;
A34: x = W8.(m+1) by A4, A5, A10, A32, A33, GLIB_001:36
.= W9.(len W7 + m) by A7, A8, A10, A33, GLIB_001:33;
1 <= m & 0 <= len W7 by CHORD:2;
then A35: 1+0 <= m + len W7 by XREAL_1:7;
len W7 + m < len W7 + len W8 by A10, A33, XREAL_1:8;
then len W7 + m <= len W9 by A9, NAT_1:13;
hence x in W9.edges() by A34, A35, GLIB_001:99;
end;
suppose n < m;
then len W8 + 1 <= m by A10, NAT_1:13;
then consider k being Nat such that
A36: m = len W8 + 1 + k by NAT_1:10;
reconsider k as odd Element of NAT by A36, ORDINAL1:def 12;
A37: k < len W7
proof
assume len W7 <= k;
then len W7 + (len W8 + 1) <= k + (len W8 + 1) by XREAL_1:6;
hence contradiction by A10, A11, A32, A36;
end;
then A38: k+1 in dom W7 by GLIB_001:12;
A39: x = W.(n+2 + k) by A10, A32, A36
.= W7.(k+1) by A2, A37, GLIB_001:36
.= W9.(k+1) by A38, GLIB_001:32;
len W7 <= len W9 by A7, A8, GLIB_001:29;
then k < len W9 by A37, XXREAL_0:2;
hence x in W9.edges() by A39, GLIB_001:100;
end;
end;
hence W9.edges() = W.edges()\{e} by TARSKI:2;
end;
assume A40: W is Path-like;
now
let x be object;
hereby
assume x in W7.vertices() /\ W8.vertices();
then A41: x in W7.vertices() & x in W8.vertices() by XBOOLE_0:def 4;
then consider n1 being odd Element of NAT such that
A42: n1 <= len W7 & W7.n1 = x by GLIB_001:87;
consider n2 being odd Element of NAT such that
A43: n2 <= len W8 & W8.n2 = x by A41, GLIB_001:87;
reconsider n3=n1-1, n4=n2-1 as Nat by CHORD:2;
reconsider n3, n4 as even Element of NAT by ORDINAL1:def 12;
n3+1 < len W7 + 1 & n4+1 < len W8 + 1 by A42, A43, NAT_1:13;
then A44: n3 < len W7 & n4 < len W8 by XREAL_1:6;
then A45: W.(n+2+n3) = W7.(n3+1) by A2, GLIB_001:36
.= x by A42;
A46: x = W.(1+n4) by A4, A5, A43, A44, GLIB_001:36;
A47: n2+0 < n+(2+n3) by A10, A43, XREAL_1:8;
n+2+n3 = n+1+n1;
then n+2+n3 <= n+1+len W7 by A42, XREAL_1:6;
then 1+n4 = 1 by A11, A40, A45, A46, A47, GLIB_001:def 28;
hence x = W.first() by A46;
end;
assume x = W.first();
then x = W.1;
then x in W7.vertices() & x in W8.vertices() by A7, A8, GLIB_001:88;
hence x in W7.vertices() /\ W8.vertices() by XBOOLE_0:def 4;
end;
hence A48: W7.vertices() /\ W8.vertices() = {W.first()} by TARSKI:def 1;
thus not W.(n+1) in G.loops() implies W9 is open
proof
assume A49: not W.(n+1) in G.loops() & W9 is closed;
A50: W.(n+2) = W7.first() by A3, GLIB_001:def 23
.= W9.first() by A7, A8, GLIB_001:30
.= W9.last() by A49, GLIB_001:def 24
.= W8.last() by A7, A8, GLIB_001:30
.= W.n by A6, GLIB_001:def 23;
n+0 < n+2 by XREAL_1:8;
then A51: n = 1 & n+2 = len W by A2, A40, A50, GLIB_001:def 28;
W.(n+1) Joins W.n,W.(n+2),G by A1, GLIB_001:def 3;
hence contradiction by A7, A49, A51, GLIB_009:def 2;
end;
per cases;
suppose n = 1;
then W8 is trivial by A4, GLIB_001:131;
hence thesis by A40, GLIB_001:130;
end;
suppose n+2 = len W;
then W7 is trivial by GLIB_001:131;
hence thesis by A7, A8, A40, HELLY:16;
end;
suppose A52: n <> 1 & n+2 <> len W;
then 1 < n & n <> len W by A1, A5, XXREAL_0:1;
then A53: W8 is open by A4, A40, Th30, POLYFORM:4;
n+2 < len W & n+2 <> 1 by A2, A52, XXREAL_0:1;
then W7 is open by A40, Th30;
hence thesis by A7, A8, A40, A48, A53, HELLY:19;
end;
end;
:: extension of GLIB_001:157
theorem Th32:
for G being _Graph, W1 being Walk of G, e,x,y being object
st e Joins x,y,G & e in W1.edges() & W1 is Cycle-like
ex W2 being Path of G st W2 is_Walk_from x,y &
W2.edges() = W1.edges() \ {e} & (not e in G.loops() implies W2 is open)
proof
let G be _Graph, W1 be Walk of G, e,x,y be object;
assume A1: e Joins x,y,G & e in W1.edges() & W1 is Cycle-like;
then consider n being odd Element of NAT such that
A2: n < len W1 & W1.(n+1) = e by GLIB_001:100;
set W7 = W1.cut(n+2,len W1), W8 = W1.cut(1,n), W9 = W7.append(W8);
A3: W9 is_Walk_from W1.(n+2),W1.n by A1, A2, Th31;
A4: W9.edges() = W1.edges() \ {e} by A1, A2, Th31;
A5: W9 is Path-like & (not e in G.loops() implies W9 is open)
by A1, A2, Th31;
W1.(n+1) Joins W1.n,W1.(n+2),G by A2, GLIB_001:def 3;
then per cases by A1, A2, GLIB_000:15;
suppose A6: W1.n = y & W1.(n+2) = x;
reconsider W2 = W9 as Path of G by A5;
take W2;
thus thesis by A3, A4, A5, A6;
end;
suppose A7: W1.n = x & W1.(n+2) = y;
reconsider W2 = W9.reverse() as Path of G by A5;
take W2;
A8: W2 is_Walk_from x,y by A3, A7, GLIB_001:23;
W2.edges() = W1.edges() \ {e} by A4, GLIB_001:107;
hence thesis by A5, A8, GLIB_001:120;
end;
end;
theorem
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 len W1 <= len W2;
then 2*W1.length() + 1 <= len W2 by GLIB_001:112;
then 2*W1.length() + 1 <= 2*W2.length() + 1 by GLIB_001:112;
then 2*W1.length() <= 2*W2.length() by XREAL_1:6;
then 2*W1.length()/2 <= 2*W2.length()/2 by XREAL_1:72;
hence W1.length() <= W2.length();
end;
assume W1.length() <= W2.length();
then 2*W1.length() <= 2*W2.length() by XREAL_1:64;
then 2*W1.length() + 1 <= 2*W2.length() + 1 by XREAL_1:6;
then len W1 <= 2*W2.length() + 1 by GLIB_001:112;
hence thesis by GLIB_001:112;
end;
theorem
for G being _Graph, W being Walk of G
holds W.length() = W.reverse().length()
proof
let G be _Graph, W be Walk of G;
len W = len W.reverse() by GLIB_001:21;
hence thesis by GLIB_001:113;
end;
theorem Th36:
for G being _Graph, W being Walk of G, e being object
st not e in W.last().edgesInOut() holds W.addEdge(e) = W
proof
let G be _Graph, W be Walk of G, e be object;
set v = the Element of the_Vertices_of G;
A1: e is set by TARSKI:1;
assume not e in W.last().edgesInOut();
then A2: not e Joins W.last(),W.last().adj(e),G by A1, GLIB_000:67;
thus W.addEdge(e)
= W.append(G.walkOf(W.last(), e, W.last().adj(e)))
.= W.append(G.walkOf(v)) by A2, GLIB_001:def 5
.= W by GLIB_001:130;
end;
theorem
for G being _Graph, W being Walk of G, e,x being object
st e Joins W.last(),x,G holds W.addEdge(e).length() = W.length() + 1
proof
let G be _Graph, W be Walk of G, e,x be object;
assume A1: e Joins W.last(),x,G;
2*W.addEdge(e).length()+1 = len W.addEdge(e) by GLIB_001:112
.= len W + 2 by A1, GLIB_001:64
.= 2*W.length()+1 + 2 by GLIB_001:112
.= 2*(W.length()+1) + 1;
hence thesis;
end;
theorem Th38:
for G1 being _Graph, E being set, G2 being removeEdges of G1, E
for W1 being Walk of G1 st W1.edges() misses E holds W1 is Walk of G2
proof
let G1 be _Graph, E be set, G2 be removeEdges of G1,E;
let W1 be Walk of G1;
assume A1: W1.edges() misses E;
A2: W1.edges() c= the_Edges_of G1 & the_Edges_of G2 = the_Edges_of G1 \ E
by GLIB_000:53;
the_Vertices_of G1 = the_Vertices_of G2 by GLIB_000:53;
then W1.vertices() c= the_Vertices_of G2;
hence thesis by A1, A2, XBOOLE_1:86, GLIB_001:170;
end;
begin :: into GLIB_002
theorem Th39:
for G1, G2 being _Graph, G3 being Component of G1 st G2 == G3
holds G2 is Component of G1
proof
let G1, G2 be _Graph, G3 be Component of G1;
assume A1: G2 == G3;
now
thus G2 is connected by A1, GLIB_002:8;
given G9 being connected Subgraph of G1 such that
A2: G2 c< G9;
A3: G2 c= G9 & G2 != G9 by A2, GLIB_000:def 36;
then G2 is Subgraph of G9 by GLIB_000:def 35;
then A4: G3 is Subgraph of G9 by A1, GLIB_000:92;
G3 != G9 by A1, A3, GLIB_000:85;
then G3 c< G9 by A4, GLIB_000:def 35, GLIB_000:def 36;
hence contradiction by GLIB_002:def 7;
end;
hence thesis by A1, GLIB_000:92, GLIB_002:def 7;
end;
theorem
for G1, G2 being _Graph, G3 being Component of G1 st G1 == G2
holds G3 is Component of G2
proof
let G1, G2 be _Graph, G3 be Component of G1;
assume A1: G1 == G2;
now
given G4 being connected Subgraph of G2 such that
A2: G3 c< G4;
G4 is Subgraph of G1 by A1, GLIB_000:91;
hence contradiction by A2, GLIB_002:def 7;
end;
hence thesis by A1, GLIB_000:91, GLIB_002:def 7;
end;
:: or into HELLY
theorem
for G being Tree-like _Graph, H being spanning Subgraph of G
st H is connected holds G == H
proof
let G be Tree-like _Graph, H be spanning Subgraph of G;
assume A1: H is connected;
A2: G is Subgraph of G by GLIB_000:40;
A3: the_Vertices_of G = the_Vertices_of H by GLIB_000:def 33;
the_Edges_of G c= the_Edges_of H
proof
assume not the_Edges_of G c= the_Edges_of H;
then the_Edges_of G \ the_Edges_of H <> {} by XBOOLE_1:37;
then consider e being object such that
A4: e in the_Edges_of G \ the_Edges_of H by XBOOLE_0:def 1;
set v = (the_Source_of G).e, w = (the_Target_of G).e;
A5: e in the_Edges_of G & not e in the_Edges_of H by A4, XBOOLE_0:def 5;
then A6: e Joins v,w,G by GLIB_000:def 13;
then reconsider v, w as Vertex of G by GLIB_000:13;
reconsider v1 = v, w1 = w as Vertex of H by A3;
consider W9 being Walk of H such that
A7: W9 is_Walk_from v1, w1 by A1, GLIB_002:def 1;
set P9 = the Path of W9;
reconsider P = P9 as Path of G by GLIB_001:167, GLIB_001:176;
P9 is_Walk_from v1,w1 by A7, GLIB_001:160;
then A8: P is_Walk_from v,w by GLIB_001:19;
G.walkOf(v,e,w) = G.pathBetween(v,w) by A6, GLIB_008:29
.= P9 by A8, HELLY:def 2;
then P9.edges() = G.walkOf(v,e,w).edges() by GLIB_001:110
.= {e} by A6, GLIB_001:108;
then e in P9.edges() by TARSKI:def 1;
hence contradiction by A5;
end;
then G is Subgraph of H by A2, A3, GLIB_000:44;
hence thesis by GLIB_000:87;
end;
registration
let G be _Graph;
cluster -> non empty for Element of G.componentSet();
coherence
proof
let C be Element of G.componentSet();
consider v being Vertex of G such that
A1: C = G.reachableFrom(v) by GLIB_002:def 8;
thus thesis by A1;
end;
end;
registration
let G be _Graph;
cluster G.componentSet() -> mutually-disjoint;
coherence
proof
G.componentSet() is a_partition of the_Vertices_of G by GLIB_008:23;
hence thesis;
end;
end;
begin :: into CHORD
theorem Th42:
for G being _Graph, v,w being Vertex of G
holds v,w are_adjacent iff w in v.allNeighbors()
proof
let G be _Graph, v,w be Vertex of G;
hereby
assume v,w are_adjacent;
then ex e being object st e Joins v,w,G by CHORD:def 3;
hence w in v.allNeighbors() by GLIB_000:71;
end;
assume w in v.allNeighbors();
then ex e being object st e Joins v,w,G by GLIB_000:71;
hence thesis by CHORD:def 3;
end;
:: the necessary existence clustering is from _008, but should be in _002
theorem Th43:
for G being _Graph, S being set, v being Vertex of G
st not v in S & S meets G.reachableFrom(v) holds G.AdjacentSet(S) <> {}
proof
let G be _Graph, S be set, v be Vertex of G;
assume A1: not v in S & S meets G.reachableFrom(v);
then consider w being object such that
A2: w in S & w in G.reachableFrom(v) by XBOOLE_0:3;
consider W being Walk of G such that
A3: W is_Walk_from v,w by A2, GLIB_002:def 5;
ex n being odd Nat st n < len W & not W.n in S & W.(n+2) in S
proof
assume A4: for n being odd Nat holds n >= len W or
W.n in S or not W.(n+2) in S;
defpred P[Nat] means 2*$1+1 <= len W implies not W.(2*$1+1) in S;
A5: P[0]
proof
assume 2*0+1 <= len W;
W.(2*0+1) = W.first()
.= v by A3, GLIB_001:def 23;
hence thesis by A1;
end;
A6: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A7: P[k] & 2*(k+1)+1 <= len W;
k+0 < k+1 by XREAL_1:8;
then 2*k < 2*(k+1) by XREAL_1:68;
then 2*k+1 < 2*(k+1)+1 by XREAL_1:8;
then 2*k+1 < len W by A7, XXREAL_0:2;
then not W.(2*k+1+2) in S by A4, A7;
hence thesis;
end;
A8: for k being Nat holds P[k] from NAT_1:sch 2(A5,A6);
reconsider m = len W - 1 as Nat by CHORD:2;
set k = m div 2;
m = 2*k by ABIAN:def 1, NAT_D:3;
then 2*k+1 = len W;
then not W.len W in S by A8;
then not W.last() in S;
hence contradiction by A2, A3, GLIB_001:def 23;
end;
then consider n being odd Nat such that
A9: n < len W & not W.n in S & W.(n+2) in S;
n is odd Element of NAT by ORDINAL1:def 12;
then A10: W.(n+1) Joins W.n,W.(n+2),G by A9, GLIB_001:def 3;
then reconsider u1 = W.n, u2 = W.(n+2) as Vertex of G by GLIB_000:13;
u1, u2 are_adjacent by A10, CHORD:def 3;
hence thesis by A9, CHORD:50;
end;
:: the necessary existence clustering is from _008, but should be in _002
registration
let G be non _trivial connected _Graph;
let S be non empty proper Subset of the_Vertices_of G;
cluster G.AdjacentSet(S) -> non empty;
coherence
proof
set w = the Element of S, v = the Element of ((the_Vertices_of G) \ S);
not the_Vertices_of G c= S by SUBSET_1:def 6, XBOOLE_0:def 10;
then (the_Vertices_of G) \ S <> {} by XBOOLE_1:37;
then A1: v in the_Vertices_of G & not v in S by XBOOLE_0:def 5;
then reconsider v as Vertex of G;
G.reachableFrom(v) = the_Vertices_of G by GLIB_002:16;
then w in S & w in G.reachableFrom(v);
then S meets G.reachableFrom(v) by XBOOLE_0:3;
hence thesis by A1, Th43;
end;
end;
theorem Th44:
for G being complete _Graph, v being Vertex of G
holds the_Vertices_of G \ {v} c= v.allNeighbors()
proof
let G be complete _Graph, v be Vertex of G;
now
let x be object;
assume x in the_Vertices_of G \ {v};
then A1: x in the_Vertices_of G & not x in {v} by XBOOLE_0:def 5;
then reconsider w = x as Vertex of G;
v <> w by A1, TARSKI:def 1;
then ex e being object st e Joins v,w,G by CHORD:def 3, CHORD:def 6;
hence x in v.allNeighbors() by GLIB_000:71;
end;
hence thesis by TARSKI:def 3;
end;
theorem Th45:
for G being loopless complete _Graph, v being Vertex of G
holds v.allNeighbors() = the_Vertices_of G \ {v}
proof
let G be loopless complete _Graph, v be Vertex of G;
now
let x be object;
assume A1: x in v.allNeighbors();
for e being object holds not e Joins v,v,G by GLIB_000:18;
then not v in v.allNeighbors() by GLIB_000:71;
then not x in {v} by A1, TARSKI:def 1;
hence x in the_Vertices_of G \ {v} by A1, XBOOLE_0:def 5;
end;
then A2: v.allNeighbors() c= the_Vertices_of G \ {v} by TARSKI:def 3;
the_Vertices_of G \ {v} c= v.allNeighbors() by Th44;
hence thesis by A2, XBOOLE_0:def 10;
end;
theorem
for G being simple complete _Graph, v being Vertex of G
holds v.degree()+`1 = G.order()
proof
let G be simple complete _Graph, v be Vertex of G;
v in {v} by TARSKI:def 1;
then not v in the_Vertices_of G \ {v} by XBOOLE_0:def 5;
then A1: not v in v.allNeighbors() by Th45;
thus v.degree()+`1 = v.degree() +` card {v} by CARD_1:30
.= card v.allNeighbors() +` card {v} by GLIB_000:111
.= card (v.allNeighbors() \/ {v}) by A1, ZFMISC_1:50, CARD_2:35
.= card (the_Vertices_of G \ {v} \/ {v}) by Th45
.= G.order() by ZFMISC_1:116;
end;
registration
let G be _Graph;
cluster trivial -> minlength for Walk of G;
coherence
proof
let W be Walk of G;
assume W is trivial;
then A1: len W = 1 by GLIB_001:126;
now
let W2 be Walk of G;
assume W2 is_Walk_from W.first(),W.last();
per cases;
suppose W2 is trivial;
hence len W2 >= len W by A1, GLIB_001:126;
end;
suppose W2 is non trivial;
then len W2 >= 3 & 3 >= 1 by GLIB_001:125;
hence len W2 >= len W by A1, XXREAL_0:2;
end;
end;
hence thesis by CHORD:def 2;
end;
cluster minlength Path-like for Walk of G;
existence
proof
take the trivial Walk of G;
thus thesis;
end;
end;
registration
let G be _Graph, W be minlength Walk of G;
cluster W.reverse() -> minlength;
coherence
proof
set W2 = W.reverse();
now
let W3 be Walk of G;
assume W3 is_Walk_from W2.first(),W2.last();
then W3.reverse() is_Walk_from W2.last(),W2.first() by GLIB_001:23;
then W3.reverse() is_Walk_from W.first(),W2.first() by GLIB_001:22;
then W3.reverse() is_Walk_from W.first(),W.last() by GLIB_001:22;
then len W3.reverse() >= len W by CHORD:def 2;
then len W3 >= len W by GLIB_001:21;
hence len W3 >= len W2 by GLIB_001:21;
end;
hence thesis by CHORD:def 2;
end;
end;
theorem Th47:
for G1 being _Graph, G2 being Subgraph of G1
for W1 being Walk of G1, W2 being Walk of G2
st W1 = W2 & W1 is minlength holds W2 is minlength
proof
let G1 be _Graph, G2 be Subgraph of G1, W1 be Walk of G1, W2 be Walk of G2;
assume A1: W1 = W2 & W1 is minlength;
now
given W9 being Walk of G2 such that
A2: W9 is_Walk_from W2.first(),W2.last() & len W9 < len W2;
reconsider W8 = W9 as Walk of G1 by GLIB_001:167;
W8 is_Walk_from W2.first(),W2.last() by A2, GLIB_001:19;
then W8 is_Walk_from W1.first(),W2.last() by A1;
then W8 is_Walk_from W1.first(),W1.last() by A1;
hence contradiction by A1, A2, CHORD:def 2;
end;
hence thesis by CHORD:def 2;
end;
theorem Th48:
for G being _Graph, v being Vertex of G, W being Walk of G
st W is_Walk_from v,v holds W is minlength iff W = G.walkOf(v)
proof
let G be _Graph, v be Vertex of G, W be Walk of G;
assume A1: W is_Walk_from v,v;
hereby
assume A2: W is minlength;
G.walkOf(v) is_Walk_from v,v by GLIB_001:13;
then G.walkOf(v) is_Walk_from W.first(),v by A1, GLIB_001:def 23;
then G.walkOf(v) is_Walk_from W.first(),W.last() by A1, GLIB_001:def 23;
then len G.walkOf(v) >= len W by A2, CHORD:def 2;
then A3: 1 >= len W by GLIB_001:13;
1 <= len W by CHORD:2;
then W is trivial by A3, XXREAL_0:1, GLIB_001:126;
then consider v0 being Vertex of G such that
A4: W = G.walkOf(v0) by GLIB_001:128;
W.first() = v0 by A4;
hence W = G.walkOf(v) by A1, A4, GLIB_001:def 23;
end;
assume A5: W = G.walkOf(v);
now
let W9 be Walk of G;
assume W9 is_Walk_from W.first(),W.last();
len W9 >= 1 by CHORD:2;
hence len W9 >= len W by A5, GLIB_001:13;
end;
hence thesis by CHORD:def 2;
end;
theorem Th49:
for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
st G1 == G2 & W1 = W2 & W1 is minlength holds W2 is minlength
proof
let G1, G2 be _Graph, W1 be Walk of G1, W2 be Walk of G2;
assume A1: G1 == G2 & W1 = W2 & W1 is minlength;
now
let W4 be Walk of G2;
assume A2: W4 is_Walk_from W2.first(),W2.last();
reconsider W3 = W4 as Walk of G1 by A1, GLIB_001:179;
W3 is_Walk_from W2.first(),W2.last() by A2, GLIB_001:19;
then W3 is_Walk_from W1.first(),W2.last() by A1;
then W3 is_Walk_from W1.first(),W1.last() by A1;
hence len W4 >= len W2 by A1, CHORD:def 2;
end;
hence thesis by CHORD:def 2;
end;
begin :: into GLIB_006
:: other direction of first part of GLIB_000:72 and GLIB_006:70
theorem Th50:
for G1, G2 being _Graph
st the_Vertices_of G2 c= the_Vertices_of G1 &
(for e,x,y being object st e DJoins x,y,G2 holds e DJoins x,y,G1)
holds G2 is Subgraph of G1 & G1 is Supergraph of G2
proof
let G1, G2 be _Graph;
assume that A1: the_Vertices_of G2 c= the_Vertices_of G1 and
A2: for e,x,y being object st e DJoins x,y,G2 holds e DJoins x,y,G1;
now
let e be object;
assume e in the_Edges_of G2;
then e DJoins (the_Source_of G2).e,(the_Target_of G2).e,G1
by A2, GLIB_000:def 14;
hence e in the_Edges_of G1 by GLIB_000:def 14;
end;
then A3: the_Edges_of G2 c= the_Edges_of G1 by TARSKI:def 3;
now
let e be set;
assume e in the_Edges_of G2;
then e DJoins (the_Source_of G2).e,(the_Target_of G2).e,G1
by A2, GLIB_000:def 14;
hence (the_Source_of G2).e = (the_Source_of G1).e &
(the_Target_of G2).e = (the_Target_of G1).e by GLIB_000:def 14;
end;
hence G2 is Subgraph of G1 by A1, A3, GLIB_000:def 32;
hence thesis by GLIB_006:57;
end;
theorem
for G1 being _Graph, G3 being Subgraph of G1, v,e,w being object
for G2 being addEdge of G3,v,e,w st e DJoins v,w,G1
holds G2 is Subgraph of G1
proof
let G1 be _Graph, G3 be Subgraph of G1, v,e,w be object;
let G2 be addEdge of G3,v,e,w;
assume A1: e DJoins v,w,G1;
per cases;
suppose A2: v in the_Vertices_of G3 & w in the_Vertices_of G3 &
not e in the_Edges_of G3;
now
the_Vertices_of G2 = the_Vertices_of G3 by A2, GLIB_006:def 11;
hence the_Vertices_of G2 c= the_Vertices_of G1;
A3: {e} c= the_Edges_of G1 by A1, GLIB_000:def 14, ZFMISC_1:31;
A4: the_Edges_of G3 \/ {e} c= the_Edges_of G1 by A3, XBOOLE_1:8;
A5: the_Edges_of G2 = the_Edges_of G3 \/ {e} by A2, GLIB_006:def 11;
hence the_Edges_of G2 c= the_Edges_of G1 by A4;
let e0 be set;
assume e0 in the_Edges_of G2;
then per cases by A5, ZFMISC_1:136;
suppose A6: e0 in the_Edges_of G3;
hence (the_Source_of G2).e0 = (the_Source_of G3).e0 by GLIB_006:def 9
.= (the_Source_of G1).e0 by A6, GLIB_000:def 32;
thus (the_Target_of G2).e0
= (the_Target_of G3).e0 by A6, GLIB_006:def 9
.= (the_Target_of G1).e0 by A6, GLIB_000:def 32;
end;
suppose A7: e0 = e;
A8: e DJoins v,w,G2 by A2, GLIB_006:105;
hence (the_Source_of G2).e0 = v by A7, GLIB_000:def 14
.= (the_Source_of G1).e0 by A1, A7, GLIB_000:def 14;
thus (the_Target_of G2).e0 = w by A7, A8, GLIB_000:def 14
.= (the_Target_of G1).e0 by A1, A7, GLIB_000:def 14;
end;
end;
hence thesis by GLIB_000:def 32;
end;
suppose not(v in the_Vertices_of G3 & w in the_Vertices_of G3 &
not e in the_Edges_of G3);
then G2 == G3 by GLIB_006:def 11;
hence thesis by GLIB_000:92;
end;
end;
:: adding an edge to a tree makes it unicyclic
theorem
for G being Tree-like _Graph, v1,v2 being Vertex of G, e being object
for H being addEdge of G,v1,e,v2 st not e in the_Edges_of G holds
H is non acyclic & for W1, W2 being Walk of H
st W1 is Cycle-like & W2 is Cycle-like holds W1.edges() = W2.edges()
proof
let G be Tree-like _Graph, v1,v2 be Vertex of G, e be object;
let H be addEdge of G,v1,e,v2;
assume A1: not e in the_Edges_of G;
v2 in the_Vertices_of G;
then v2 in G.reachableFrom v1 by GLIB_002:16;
hence H is non acyclic by A1, GLIB_006:119;
let W1, W2 be Walk of H;
assume A2: W1 is Cycle-like & W2 is Cycle-like;
A3: e in W1.edges()
proof
assume not e in W1.edges();
then reconsider W7 = W1 as Walk of G by GLIB_006:109;
W7 is Cycle-like by A2, GLIB_006:24;
hence contradiction by GLIB_002:def 2;
end;
A4: e in W2.edges()
proof
assume not e in W2.edges();
then reconsider W8 = W2 as Walk of G by GLIB_006:109;
W8 is Cycle-like by A2, GLIB_006:24;
hence contradiction by GLIB_002:def 2;
end;
e DJoins v1,v2,H by A1, GLIB_006:105;
then A5: e Joins v1,v2,H by GLIB_000:16;
consider W3 being Path of H such that
A6: W3 is_Walk_from v1,v2 & W3.edges() = W1.edges() \ {e} and
not e in H.loops() implies W3 is open by A2, A3, A5, Th32;
consider W4 being Path of H such that
A7: W4 is_Walk_from v1,v2 & W4.edges() = W2.edges() \ {e} and
not e in H.loops() implies W4 is open by A2, A4, A5, Th32;
e in {e} by TARSKI:def 1;
then A8: not e in W3.edges() & not e in W4.edges() by A6, A7, XBOOLE_0:def 5;
then reconsider W5 = W3 as Walk of G by GLIB_006:109;
reconsider W6 = W4 as Walk of G by A8, GLIB_006:109;
A9: W5 is_Walk_from v1,v2 & W5 is Path-like by A6, GLIB_001:19, GLIB_006:23;
A10: W6 is_Walk_from v1,v2 & W6 is Path-like by A7, GLIB_001:19, GLIB_006:23;
A11: W3.edges()
= G.pathBetween(v1,v2).edges() by A9, HELLY:def 2, GLIB_001:110
.= W4.edges() by A10, HELLY:def 2, GLIB_001:110;
thus W1.edges() = W3.edges() \/ {e} by A3, A6, ZFMISC_1:116
.= W2.edges() by A4, A7, A11, ZFMISC_1:116;
end;
:: if adding an edge to a graph makes it unicyclic, it has been a tree before
theorem
for G being connected _Graph
st ex v1,v2 being Vertex of G, e being object, H being addEdge of G,v1,e,v2
st not e in the_Edges_of G & for W1, W2 being Walk of H
st W1 is Cycle-like & W2 is Cycle-like holds W1.edges() = W2.edges()
holds G is Tree-like
proof
let G be connected _Graph;
given v1,v2 being Vertex of G, e being object, H being addEdge of G,v1,e,v2
such that A1: not e in the_Edges_of G and
A2: for W1, W2 being Walk of H st W1 is Cycle-like & W2 is Cycle-like
holds W1.edges() = W2.edges();
G is acyclic
proof
assume G is non acyclic;
then consider W1 being Walk of G such that
A3: W1 is Cycle-like by GLIB_002:def 2;
reconsider W3 = W1 as Walk of H by GLIB_006:75;
A4: W3 is Cycle-like by A3, GLIB_006:24;
e DJoins v1,v2,H by A1, GLIB_006:105;
then A5: e Joins v2,v1,H by GLIB_000:16;
not e in W1.edges() by A1;
then A6: not e in W3.edges() by GLIB_001:110;
per cases;
suppose A7: v1 <> v2;
consider W2 being Walk of G such that
A8: W2 is_Walk_from v1,v2 by GLIB_002:def 1;
set P2 = the Path-like Subwalk of W2;
reconsider P4 = P2 as Walk of H by GLIB_006:75;
set W4 = P4.addEdge(e);
P2 is_Walk_from v1,v2 by A8, GLIB_001:160;
then P4 is_Walk_from v1,v2 by GLIB_001:19;
then A9: P4 is Path-like & P4 is_Walk_from v1,v2 by GLIB_006:23;
then A10: W4 is closed by A5, GLIB_001:66, GLIB_001:119;
A11: P4.first() = v1 & P4.last() = v2 by A9, GLIB_001:def 23;
then A12: W4 is non trivial by A5, GLIB_001:132;
A13: P4 is open by A7, A11, GLIB_001:def 24;
not e in P2.edges() by A1;
then A14: not e in P4.edges() by GLIB_001:110;
for n being odd Element of NAT st 1 < n & n <= len P4 holds P4.n <> v1
by POLYFORM:4, GLIB_001:def 28, A7, A11;
then A16: W4 is Path-like by A5, A9, A11, A13, A14, GLIB_001:150;
e in {e} by TARSKI:def 1;
then e in P4.edges() \/ {e} by XBOOLE_0:def 3;
then e in W4.edges() by A5, A11, GLIB_001:111;
hence contradiction by A2, A4, A6, A10, A12, A16;
end;
suppose A17: v1 = v2;
set W4 = H.walkOf(v2,e,v1);
W4.edges() = {e} by A5, GLIB_001:108;
then A18: e in W4.edges() by TARSKI:def 1;
W4 is Cycle-like by A5, A17, GLIB_001:156;
hence contradiction by A2, A4, A6, A18;
end;
end;
hence thesis;
end;
theorem Th54:
for G2 being _Graph, v,e,w being object, G1 being addAdjVertex of G2,v,e,w
holds the_Vertices_of G1 c= the_Vertices_of G2 \/ {v,w} &
the_Edges_of G1 c= the_Edges_of G2 \/ {e}
proof
let G2 be _Graph, v,e,w be object, G1 be addAdjVertex of G2,v,e,w;
per cases;
suppose v in the_Vertices_of G2 & not w in the_Vertices_of G2 &
not e in the_Edges_of G2;
then the_Vertices_of G1 = the_Vertices_of G2 \/ {w} &
the_Edges_of G1 = the_Edges_of G2 \/ {e} by GLIB_006:def 12;
hence thesis by ZFMISC_1:7, XBOOLE_1:9;
end;
suppose not v in the_Vertices_of G2 & w in the_Vertices_of G2 &
not e in the_Edges_of G2;
then the_Vertices_of G1 = the_Vertices_of G2 \/ {v} &
the_Edges_of G1 = the_Edges_of G2 \/ {e} by GLIB_006:def 12;
hence thesis by ZFMISC_1:7, XBOOLE_1:9;
end;
suppose not((v in the_Vertices_of G2 & not w in the_Vertices_of G2 &
not e in the_Edges_of G2)or(not v in the_Vertices_of G2 &
w in the_Vertices_of G2 & not e in the_Edges_of G2));
then G1 == G2 by GLIB_006:def 12;
then the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 by GLIB_000:def 34;
hence thesis by XBOOLE_1:7;
end;
end;
theorem Th55:
for G2 being _Graph, v,v2 being Vertex of G2, e,w being object
for G1 being addAdjVertex of G2,v,e,w, v1 being Vertex of G1
st v1 = v2 & not v in G2.reachableFrom(v2) &
not e in the_Edges_of G2 & not w in the_Vertices_of G2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2)
proof
let G2 be _Graph, v,v2 be Vertex of G2, e,w be object;
let G1 be addAdjVertex of G2,v,e,w, v1 be Vertex of G1;
assume that A1: v1 = v2 & not v in G2.reachableFrom(v2) and
A2: not e in the_Edges_of G2 & not w in the_Vertices_of G2;
A3: G2 is Subgraph of G1 by GLIB_006:57;
then A4: G2.reachableFrom(v2) c= G1.reachableFrom(v1) by A1, GLIB_002:14;
now
let x be object;
assume x in G1.reachableFrom(v1);
then consider W1 being Walk of G1 such that
A5: W1 is_Walk_from v1,x by GLIB_002:def 5;
set P1 = the Path of W1;
x is set by TARSKI:1;
then A6: P1 is_Walk_from v1,x by A5, GLIB_001:160;
then A7: P1.first() = v1 & P1.last() = x by GLIB_001:def 23;
A8: x <> w
proof
per cases;
suppose P1 is trivial;
then v1 = x by A7, GLIB_001:127;
hence thesis by A1, A2;
end;
suppose P1 is non trivial;
then A9: 3 <= len P1 by GLIB_001:125;
then 3-3 <= len P1 -2 & len P1 -2 < len P1 -0 by XREAL_1:10, 13;
then A10: len P1-2 in NAT & len P1-2 < len P1 by INT_1:3;
then reconsider m=len P1-2 as odd Element of NAT by POLYFORM:5;
P1.(m+1) Joins P1.m,P1.(m+2),G1 by A10, GLIB_001:def 3;
then A11: P1.(m+1) Joins P1.m,x,G1 by A7;
assume x = w;
then A12: P1.m = v by A2, A11, GLIB_006:133;
set P2 = P1.cut(1,m);
3-2 <= m & m <= len P1-0 by A9, XREAL_1:9, XREAL_1:10;
then P2.first() = P1.1 & P2.last() = P1.m by GLIB_001:37, POLYFORM:4;
then A13: P2.first()=v2 & P2.last()=v by A1, A7, A12;
v2 <> v by A1, GLIB_002:9;
then A14: P2 is non trivial by A13, GLIB_001:127;
not e in P2.edges() by A2, A13, GLIB_006:147;
then reconsider P2 as Walk of G2 by A2, A14, GLIB_006:145;
P2.first() = v2 & P2.last() = v by A13;
then P2 is_Walk_from v2, v by GLIB_001:def 23;
hence contradiction by A1, GLIB_002:def 5;
end;
end;
the_Vertices_of G1 = the_Vertices_of G2 \/ {w} by A2, GLIB_006:def 12;
then x in the_Vertices_of G2 or x in {w} by A7, XBOOLE_0:def 3;
then A15: not e in P1.edges()
by A1, A2, A7, A8, TARSKI:def 1, GLIB_006:147;
P1 is Walk of G2
proof
per cases;
suppose P1 is trivial;
hence thesis by A1, A3, A7, GLIB_001:168;
end;
suppose P1 is non trivial;
hence thesis by A2, A15, GLIB_006:145;
end;
end;
then reconsider P2 = P1 as Walk of G2;
P2 is_Walk_from v2,x by A1, A6, GLIB_001:19;
hence x in G2.reachableFrom(v2) by GLIB_002:def 5;
end;
then G1.reachableFrom(v1) c= G2.reachableFrom(v2) by TARSKI:def 3;
hence thesis by A4, XBOOLE_0:def 10;
end;
theorem Th56:
for G2 being _Graph, w,v2 being Vertex of G2, v,e being object
for G1 being addAdjVertex of G2,v,e,w, v1 being Vertex of G1
st v1 = v2 & not w in G2.reachableFrom(v2) &
not e in the_Edges_of G2 & not v in the_Vertices_of G2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2)
proof
let G2 be _Graph, w,v2 be Vertex of G2, v,e be object;
let G1 be addAdjVertex of G2,v,e,w, v1 be Vertex of G1;
assume that A1: v1 = v2 & not w in G2.reachableFrom(v2) and
A2: not e in the_Edges_of G2 & not v in the_Vertices_of G2;
A3: G2 is Subgraph of G1 by GLIB_006:57;
then A4: G2.reachableFrom(v2) c= G1.reachableFrom(v1) by A1, GLIB_002:14;
now
let x be object;
assume x in G1.reachableFrom(v1);
then consider W1 being Walk of G1 such that
A5: W1 is_Walk_from v1,x by GLIB_002:def 5;
set P1 = the Path of W1;
x is set by TARSKI:1;
then A6: P1 is_Walk_from v1,x by A5, GLIB_001:160;
then A7: P1.first() = v1 & P1.last() = x by GLIB_001:def 23;
A8: x <> v
proof
per cases;
suppose P1 is trivial;
then v1 = x by A7, GLIB_001:127;
hence thesis by A1, A2;
end;
suppose P1 is non trivial;
then A9: 3 <= len P1 by GLIB_001:125;
then 3-3 <= len P1 -2 & len P1 -2 < len P1 -0 by XREAL_1:10, 13;
then A10: len P1-2 in NAT & len P1-2 < len P1 by INT_1:3;
then reconsider m=len P1-2 as odd Element of NAT by POLYFORM:5;
P1.(m+1) Joins P1.m,P1.(m+2),G1 by A10, GLIB_001:def 3;
then P1.(m+1) Joins P1.m,x,G1 by A7;
then A11: P1.(m+1) Joins x,P1.m,G1 by GLIB_000:14;
assume x = v;
then A12: P1.m = w by A2, A11, GLIB_006:134;
set P2 = P1.cut(1,m);
3-2 <= m & m <= len P1-0 by A9, XREAL_1:9, XREAL_1:10;
then P2.first() = P1.1 & P2.last() = P1.m by GLIB_001:37, POLYFORM:4;
then A13: P2.first()=v2 & P2.last()=w by A1, A7, A12;
v2 <> w by A1, GLIB_002:9;
then A14: P2 is non trivial by A13, GLIB_001:127;
not e in P2.edges() by A2, A13, GLIB_006:147;
then reconsider P2 as Walk of G2 by A2, A14, GLIB_006:146;
P2.first() = v2 & P2.last() = w by A13;
then P2 is_Walk_from v2, w by GLIB_001:def 23;
hence contradiction by A1, GLIB_002:def 5;
end;
end;
the_Vertices_of G1 = the_Vertices_of G2 \/ {v} by A2, GLIB_006:def 12;
then x in the_Vertices_of G2 or x in {v} by A7, XBOOLE_0:def 3;
then A15: not e in P1.edges()
by A1, A2, A7, A8, TARSKI:def 1, GLIB_006:147;
P1 is Walk of G2
proof
per cases;
suppose P1 is trivial;
hence thesis by A1, A3, A7, GLIB_001:168;
end;
suppose P1 is non trivial;
hence thesis by A2, A15, GLIB_006:146;
end;
end;
then reconsider P2 = P1 as Walk of G2;
P2 is_Walk_from v2,x by A1, A6, GLIB_001:19;
hence x in G2.reachableFrom(v2) by GLIB_002:def 5;
end;
then G1.reachableFrom(v1) c= G2.reachableFrom(v2) by TARSKI:def 3;
hence thesis by A4, XBOOLE_0:def 10;
end;
theorem Th57:
for G2 being _Graph, v being Vertex of G2, e,w being object
for G1 being addAdjVertex of G2,v,e,w, v1 being Vertex of G1
st v1 = v & not e in the_Edges_of G2 & not w in the_Vertices_of G2
holds G1.reachableFrom(v1) = G2.reachableFrom(v) \/ {w}
proof
let G2 be _Graph, v be Vertex of G2, e,w be object;
let G1 be addAdjVertex of G2,v,e,w, v1 be Vertex of G1;
assume A1: v1 = v & not e in the_Edges_of G2 & not w in the_Vertices_of G2;
G2 is Subgraph of G1 by GLIB_006:57;
then A2: G2.reachableFrom(v) c= G1.reachableFrom(v1) by A1, GLIB_002:14;
A3: e Joins v1,w,G1 by A1, GLIB_006:131;
v1 in G1.reachableFrom(v1) by GLIB_002:9;
then {w} c= G1.reachableFrom(v1) by A3, GLIB_002:10, ZFMISC_1:31;
then A4: G2.reachableFrom(v)\/{w} c= G1.reachableFrom(v1) by A2, XBOOLE_1:8;
now
let x be object;
assume x in G1.reachableFrom(v1);
then consider W1 being Walk of G1 such that
A5: W1 is_Walk_from v1,x by GLIB_002:def 5;
set P1 = the Path of W1;
x is set by TARSKI:1;
then A6: P1 is_Walk_from v1,x by A5, GLIB_001:160;
then A7: P1.first() = v1 & P1.last() = x by GLIB_001:def 23;
per cases;
suppose A8: P1 is non trivial & x <> w;
the_Vertices_of G1 = the_Vertices_of G2 \/ {w} by A1, GLIB_006:def 12;
then x in the_Vertices_of G2 by A7, A8, ZFMISC_1:136;
then not e in P1.edges() by A1, A7, GLIB_006:147;
then reconsider P2=P1 as Walk of G2 by A1, A8, GLIB_006:145;
P2 is_Walk_from v,x by A1, A6, GLIB_001:19;
then x in G2.reachableFrom(v) by GLIB_002:def 5;
hence x in G2.reachableFrom(v)\/{w} by XBOOLE_0:def 3;
end;
suppose P1 is trivial;
then x = v1 by A7, GLIB_001:127;
then x in G2.reachableFrom(v) by A1, GLIB_002:9;
hence x in G2.reachableFrom(v)\/{w} by XBOOLE_0:def 3;
end;
suppose x = w;
then x in {w} by TARSKI:def 1;
hence x in G2.reachableFrom(v)\/{w} by XBOOLE_0:def 3;
end;
end;
then G1.reachableFrom(v1) c= G2.reachableFrom(v) \/ {w} by TARSKI:def 3;
hence thesis by A4, XBOOLE_0:def 10;
end;
theorem Th58:
for G2 being _Graph, v,e being object, w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w, v1 being Vertex of G1
st v1 = w & not e in the_Edges_of G2 & not v in the_Vertices_of G2
holds G1.reachableFrom(v1) = G2.reachableFrom(w) \/ {v}
proof
let G2 be _Graph, v,e be object, w be Vertex of G2;
let G1 be addAdjVertex of G2,v,e,w, v1 be Vertex of G1;
assume A1: v1 = w & not e in the_Edges_of G2 & not v in the_Vertices_of G2;
G2 is Subgraph of G1 by GLIB_006:57;
then A2: G2.reachableFrom(w) c= G1.reachableFrom(v1) by A1, GLIB_002:14;
e Joins v,v1,G1 by A1, GLIB_006:132;
then A3: e Joins v1,v,G1 by GLIB_000:14;
v1 in G1.reachableFrom(v1) by GLIB_002:9;
then {v} c= G1.reachableFrom(v1) by A3, GLIB_002:10, ZFMISC_1:31;
then A4: G2.reachableFrom(w)\/{v} c= G1.reachableFrom(v1) by A2, XBOOLE_1:8;
now
let x be object;
assume x in G1.reachableFrom(v1);
then consider W1 being Walk of G1 such that
A5: W1 is_Walk_from v1,x by GLIB_002:def 5;
set P1 = the Path of W1;
x is set by TARSKI:1;
then A6: P1 is_Walk_from v1,x by A5, GLIB_001:160;
then A7: P1.first() = v1 & P1.last() = x by GLIB_001:def 23;
per cases;
suppose A8: P1 is non trivial & x <> v;
the_Vertices_of G1 = the_Vertices_of G2 \/ {v} by A1, GLIB_006:def 12;
then x in the_Vertices_of G2 by A7, A8, ZFMISC_1:136;
then not e in P1.edges() by A1, A7, GLIB_006:147;
then reconsider P2=P1 as Walk of G2 by A1, A8, GLIB_006:146;
P2 is_Walk_from w,x by A1, A6, GLIB_001:19;
then x in G2.reachableFrom(w) by GLIB_002:def 5;
hence x in G2.reachableFrom(w)\/{v} by XBOOLE_0:def 3;
end;
suppose P1 is trivial;
then x = v1 by A7, GLIB_001:127;
then x in G2.reachableFrom(w) by A1, GLIB_002:9;
hence x in G2.reachableFrom(w)\/{v} by XBOOLE_0:def 3;
end;
suppose x = v;
then x in {v} by TARSKI:def 1;
hence x in G2.reachableFrom(w)\/{v} by XBOOLE_0:def 3;
end;
end;
then G1.reachableFrom(v1) c= G2.reachableFrom(w) \/ {v} by TARSKI:def 3;
hence thesis by A4, XBOOLE_0:def 10;
end;
theorem
for G2 being _Graph, v being Vertex of G2, e,w being object
for G1 being addAdjVertex of G2,v,e,w
st not e in the_Edges_of G2 & not w in the_Vertices_of G2
holds G1.componentSet() =
G2.componentSet() \ {G2.reachableFrom(v)} \/ {G2.reachableFrom(v) \/ {w}}
proof
let G2 be _Graph, v be Vertex of G2, e,w be object;
let G1 be addAdjVertex of G2,v,e,w;
set M1 = G2.componentSet() \ {G2.reachableFrom(v)};
set M2 = {G2.reachableFrom(v) \/ {w}};
assume A1: not e in the_Edges_of G2 & not w in the_Vertices_of G2;
then A2: the_Vertices_of G1 = the_Vertices_of G2\/{w} by GLIB_006:def 12;
then reconsider v9 = v as Vertex of G1 by XBOOLE_0:def 3;
A3: e Joins v,w,G1 by A1, GLIB_006:131;
now
let x be object;
hereby
assume x in G1.componentSet();
then consider v1 being Vertex of G1 such that
A4: x = G1.reachableFrom(v1) by GLIB_002:def 8;
per cases;
suppose v1 <> w;
then not v1 in {w} by TARSKI:def 1;
then reconsider v2 = v1 as Vertex of G2 by A2, XBOOLE_0:def 3;
per cases;
suppose not v2 in G2.reachableFrom(v);
then A5: G2.reachableFrom(v2) misses G2.reachableFrom(v)
by GLIB_008:22;
then A6: x = G2.reachableFrom(v2) by A1, A4, Th55, GLIB_002:12;
then A7: x in G2.componentSet() by GLIB_002:def 8;
not x in {G2.reachableFrom(v)} by A6, A5, TARSKI:def 1;
hence x in M1 or x in M2 by A7, XBOOLE_0:def 5;
end;
suppose A8: v2 in G2.reachableFrom(v);
A9: G1.reachableFrom(v9) = G2.reachableFrom(v)\/{w} by A1, Th57;
G2 is Subgraph of G1 by GLIB_006:57;
then G2.reachableFrom(v) c= G1.reachableFrom(v9) by GLIB_002:14;
then x = G2.reachableFrom(v) \/ {w} by A4, A8, A9, GLIB_002:12;
hence x in M1 or x in M2 by TARSKI:def 1;
end;
end;
suppose A10: v1 = w;
A11: G1.reachableFrom(v9) = G2.reachableFrom(v) \/ {w} by A1, Th57;
v1 in G1.reachableFrom(v9) by A3, A10, GLIB_002:9, GLIB_002:10;
then x = G2.reachableFrom(v) \/ {w} by A4, A11, GLIB_002:12;
hence x in M1 or x in M2 by TARSKI:def 1;
end;
end;
assume x in M1 or x in M2;
then per cases;
suppose x in M1;
then A12: x in G2.componentSet() & not x in {G2.reachableFrom(v)}
by XBOOLE_0:def 5;
then consider v2 being Vertex of G2 such that
A13: x = G2.reachableFrom(v2) by GLIB_002:def 8;
reconsider v1 = v2 as Vertex of G1 by A2, XBOOLE_0:def 3;
x <> G2.reachableFrom(v) by A12, TARSKI:def 1;
then x = G1.reachableFrom(v1) by A1, A13, Th55, GLIB_002:12;
hence x in G1.componentSet() by GLIB_002:def 8;
end;
suppose x in M2;
then A14: x = G2.reachableFrom(v) \/ {w} by TARSKI:def 1;
G1.reachableFrom(v9) = G2.reachableFrom(v) \/ {w} by A1, Th57;
hence x in G1.componentSet() by A14, GLIB_002:def 8;
end;
end;
hence thesis by XBOOLE_0:def 3;
end;
theorem
for G2 being _Graph, v,e being object, w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
st not e in the_Edges_of G2 & not v in the_Vertices_of G2
holds G1.componentSet() =
G2.componentSet() \ {G2.reachableFrom(w)} \/ {G2.reachableFrom(w) \/ {v}}
proof
let G2 be _Graph, v,e be object, w be Vertex of G2;
let G1 be addAdjVertex of G2,v,e,w;
set M1 = G2.componentSet() \ {G2.reachableFrom(w)};
set M2 = {G2.reachableFrom(w) \/ {v}};
assume A1: not e in the_Edges_of G2 & not v in the_Vertices_of G2;
then A2: the_Vertices_of G1 = the_Vertices_of G2\/{v} by GLIB_006:def 12;
then reconsider v9 = w as Vertex of G1 by XBOOLE_0:def 3;
e Joins v,w,G1 by A1, GLIB_006:132;
then A3: e Joins w,v,G1 by GLIB_000:14;
now
let x be object;
hereby
assume x in G1.componentSet();
then consider v1 being Vertex of G1 such that
A4: x = G1.reachableFrom(v1) by GLIB_002:def 8;
per cases;
suppose v1 <> v;
then not v1 in {v} by TARSKI:def 1;
then reconsider v2 = v1 as Vertex of G2 by A2, XBOOLE_0:def 3;
per cases;
suppose not v2 in G2.reachableFrom(w);
then A5: G2.reachableFrom(v2) misses G2.reachableFrom(w)
by GLIB_008:22;
then A6: x = G2.reachableFrom(v2) by A1, A4, Th56, GLIB_002:12;
then A7: x in G2.componentSet() by GLIB_002:def 8;
not x in {G2.reachableFrom(w)} by A6, A5, TARSKI:def 1;
hence x in M1 or x in M2 by A7, XBOOLE_0:def 5;
end;
suppose A8: v2 in G2.reachableFrom(w);
A9: G1.reachableFrom(v9) = G2.reachableFrom(w)\/{v} by A1, Th58;
G2 is Subgraph of G1 by GLIB_006:57;
then G2.reachableFrom(w) c= G1.reachableFrom(v9) by GLIB_002:14;
then x = G2.reachableFrom(w) \/ {v} by A4, A8, A9, GLIB_002:12;
hence x in M1 or x in M2 by TARSKI:def 1;
end;
end;
suppose A10: v1 = v;
A11: G1.reachableFrom(v9) = G2.reachableFrom(w) \/ {v} by A1, Th58;
v1 in G1.reachableFrom(v9) by A3, A10, GLIB_002:9, GLIB_002:10;
then x = G2.reachableFrom(w) \/ {v} by A4, A11, GLIB_002:12;
hence x in M1 or x in M2 by TARSKI:def 1;
end;
end;
assume x in M1 or x in M2;
then per cases;
suppose x in M1;
then A12: x in G2.componentSet() & not x in {G2.reachableFrom(w)}
by XBOOLE_0:def 5;
then consider v2 being Vertex of G2 such that
A13: x = G2.reachableFrom(v2) by GLIB_002:def 8;
reconsider v1 = v2 as Vertex of G1 by A2, XBOOLE_0:def 3;
x <> G2.reachableFrom(w) by A12, TARSKI:def 1;
then x = G1.reachableFrom(v1) by A1, A13, Th56, GLIB_002:12;
hence x in G1.componentSet() by GLIB_002:def 8;
end;
suppose x in M2;
then A14: x = G2.reachableFrom(w) \/ {v} by TARSKI:def 1;
G1.reachableFrom(v9) = G2.reachableFrom(w) \/ {v} by A1, Th58;
hence x in G1.componentSet() by A14, GLIB_002:def 8;
end;
end;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th61:
for G2 being _Graph, v,e,w being object, G1 being addAdjVertex of G2,v,e,w
for W1 being Walk of G1, W2 being Walk of G2
st W1 = W2 & W2 is minlength holds W1 is minlength
proof
let G2 be _Graph, v,e,w be object, G1 be addAdjVertex of G2,v,e,w;
let W1 be Walk of G1, W2 be Walk of G2;
assume A1: W1 = W2 & W2 is minlength;
then W1.first() = W2.first() & W1.last() = W2.last();
then A2: W1.first() in the_Vertices_of G2 & W1.last() in the_Vertices_of G2;
per cases;
suppose A3: not e in the_Edges_of G2 & not v in the_Vertices_of G2 &
w in the_Vertices_of G2;
now
let W3 be Walk of G1;
assume A4: W3 is_Walk_from W1.first(),W1.last();
set T = the Trail of W3;
A5: T is_Walk_from W1.first(),W1.last() by A4, GLIB_001:160;
then A6: T.first()=W1.first() & T.last()=W1.last() by GLIB_001:def 23;
then A7: not e in T.edges() by A2, A3, GLIB_006:147;
T is Walk of G2
proof
per cases;
suppose T is trivial;
then consider v0 being Vertex of G1 such that
A8: T = G1.walkOf(v0) by GLIB_001:128;
A9: v0 in the_Vertices_of G2 by A2, A6, A8;
T.vertices() = {v0} by A8, GLIB_001:90;
then not v in T.vertices() by A3, A9, TARSKI:def 1;
hence thesis by A3, GLIB_006:146;
end;
suppose T is non trivial;
hence thesis by A3, A7, GLIB_006:146;
end;
end;
then reconsider W4 = T as Walk of G2;
W4 is_Walk_from W1.first(),W1.last() by A5, GLIB_001:19;
then W4 is_Walk_from W2.first(),W1.last() by A1;
then W4 is_Walk_from W2.first(),W2.last() by A1;
then A10: len T >= len W1 by A1, CHORD:def 2;
len W3 >= len T by GLIB_001:162;
hence len W3 >= len W1 by A10, XXREAL_0:2;
end;
hence thesis by CHORD:def 2;
end;
suppose A11: not e in the_Edges_of G2 & not w in the_Vertices_of G2 &
v in the_Vertices_of G2;
now
let W3 be Walk of G1;
assume A12: W3 is_Walk_from W1.first(),W1.last();
set T = the Trail of W3;
A13: T is_Walk_from W1.first(),W1.last() by A12, GLIB_001:160;
then A14: T.first()=W1.first() & T.last()=W1.last() by GLIB_001:def 23;
then A15: not e in T.edges() by A2, A11, GLIB_006:147;
T is Walk of G2
proof
per cases;
suppose T is trivial;
then consider v0 being Vertex of G1 such that
A16: T = G1.walkOf(v0) by GLIB_001:128;
A17: v0 in the_Vertices_of G2 by A2, A14, A16;
T.vertices() = {v0} by A16, GLIB_001:90;
then not w in T.vertices() by A11, A17, TARSKI:def 1;
hence thesis by A11, GLIB_006:145;
end;
suppose T is non trivial;
hence thesis by A11, A15, GLIB_006:145;
end;
end;
then reconsider W4 = T as Walk of G2;
W4 is_Walk_from W1.first(),W1.last() by A13, GLIB_001:19;
then W4 is_Walk_from W2.first(),W1.last() by A1;
then W4 is_Walk_from W2.first(),W2.last() by A1;
then A18: len T >= len W1 by A1, CHORD:def 2;
len W3 >= len T by GLIB_001:162;
hence len W3 >= len W1 by A18, XXREAL_0:2;
end;
hence thesis by CHORD:def 2;
end;
suppose not((not e in the_Edges_of G2 & not v in the_Vertices_of G2 &
w in the_Vertices_of G2) or (not e in the_Edges_of G2 &
not w in the_Vertices_of G2 & v in the_Vertices_of G2));
then G1 == G2 by GLIB_006:def 12;
hence thesis by A1, Th49;
end;
end;
:: the necessary existence clustering is from _008, but should be in _002
theorem
for G1 being non _trivial connected _Graph
for G2 being non spanning Subgraph of G1
ex v,e,w being object
st v <> w & e DJoins v,w,G1 & not e in the_Edges_of G2 &
(for G3 being addAdjVertex of G2,v,e,w holds G3 is Subgraph of G1) &
((v in the_Vertices_of G2 & not w in the_Vertices_of G2) or
(not v in the_Vertices_of G2 & w in the_Vertices_of G2))
proof
let G1 be non _trivial connected _Graph, G2 be non spanning Subgraph of G1;
set S = the_Vertices_of G2;
A1: S is non empty proper Subset of the_Vertices_of G1
by GLIB_000:def 33, SUBSET_1:def 6;
set v0 = the Element of G1.AdjacentSet(S);
reconsider v0 as Vertex of G1 by A1, TARSKI:def 3;
consider w0 being Vertex of G1 such that
A2: w0 in S & v0,w0 are_adjacent by A1, CHORD:50;
consider e being object such that
A3: e Joins v0,w0,G1 by A2, CHORD:def 3;
set v = (the_Source_of G1).e, w = (the_Target_of G1).e;
take v,e,w;
A4: e in the_Edges_of G1 by A3, GLIB_000:def 13;
then A5: e DJoins v,w,G1 & e Joins v,w,G1 by GLIB_000:def 13, def 14;
then A6: v = v0 & w = w0 or v = w0 & w = v0 by A3, GLIB_000:15;
A7: not v0 in S by A1, CHORD:50;
hence v <> w & e DJoins v,w,G1 by A2, A5, A6;
thus A8: not e in the_Edges_of G2
proof
assume e in the_Edges_of G2;
then e Joins v,w,G2 by A5, GLIB_000:73;
hence contradiction by A6, A7, GLIB_000:13;
end;
hereby
let G3 be addAdjVertex of G2,v,e,w;
now
v in the_Vertices_of G1 & w in the_Vertices_of G1 by A5, GLIB_000:13;
then A9: {v,w} c= the_Vertices_of G1 by ZFMISC_1:32;
A10: the_Vertices_of G2 \/ {v,w} c= the_Vertices_of G1 by A9, XBOOLE_1:8;
the_Vertices_of G3 c= the_Vertices_of G2 \/ {v,w} by Th54;
hence the_Vertices_of G3 c= the_Vertices_of G1 by A10, XBOOLE_1:1;
A11: {e} c= the_Edges_of G1 by A4, ZFMISC_1:31;
A12: the_Edges_of G2 \/ {e} c= the_Edges_of G1 by A11, XBOOLE_1:8;
A13: the_Edges_of G3 c= the_Edges_of G2 \/ {e} by Th54;
hence the_Edges_of G3 c= the_Edges_of G1 by A12, XBOOLE_1:1;
let e0 be set;
assume e0 in the_Edges_of G3;
then per cases by A13, ZFMISC_1:136;
suppose A14: e0 in the_Edges_of G2;
hence (the_Source_of G3).e0 = (the_Source_of G2).e0 by GLIB_006:def 9
.= (the_Source_of G1).e0 by A14, GLIB_000:def 32;
thus (the_Target_of G3).e0
= (the_Target_of G2).e0 by A14, GLIB_006:def 9
.= (the_Target_of G1).e0 by A14, GLIB_000:def 32;
end;
suppose A15: e0 = e;
A16: e DJoins v,w,G3 by A2, A6, A7, A8, GLIB_006:131, GLIB_006:132;
hence (the_Source_of G3).e0 = (the_Source_of G1).e0
by A15, GLIB_000:def 14;
thus (the_Target_of G3).e0 = (the_Target_of G1).e0
by A15, A16, GLIB_000:def 14;
end;
end;
hence G3 is Subgraph of G1 by GLIB_000:def 32;
end;
thus thesis by A2, A6, A7;
end;
theorem
for G2 being _Graph, v being Vertex of G2, e,w,x being object
for G1 being addAdjVertex of G2,v,e,w
for W1 being Walk of G1, W2 being Walk of G2
st W1 = W2 & W2 is minlength & W2 is_Walk_from x,v & not e in the_Edges_of G2
holds W1.addEdge(e) is minlength
proof
let G2 be _Graph, v be Vertex of G2, e,w,x be object;
let G1 be addAdjVertex of G2,v,e,w;
let W1 be Walk of G1, W2 be Walk of G2;
assume that
A1: W1 = W2 & W2 is minlength & W2 is_Walk_from x,v and
A2: not e in the_Edges_of G2;
per cases;
suppose A3: not w in the_Vertices_of G2;
then A4: e Joins v,w,G1 by A2, GLIB_006:131;
A5: v = W2.last() by A1, GLIB_001:def 23
.= W1.last() by A1;
now
let W3 be Walk of G1;
assume W3 is_Walk_from W1.addEdge(e).first(),W1.addEdge(e).last();
then W3 is_Walk_from W1.first(),W1.addEdge(e).last()
by A4, A5, GLIB_001:63;
then A6: W3 is_Walk_from W1.first(),w by A4, A5, GLIB_001:63;
then A7: W3 is_Walk_from W2.first(),w by A1;
now
assume A8: W3 is trivial;
W2.first() = W3.first() by A7, GLIB_001:def 23
.= W3.last() by A8, GLIB_001:127
.= w by A7, GLIB_001:def 23;
hence contradiction by A3;
end;
then A9: 3-2 <= len W3 - 2 by GLIB_001:125, XREAL_1:9;
then reconsider m=len W3-2 as odd Element of NAT by INT_1:3, POLYFORM:5;
A10: m < len W3 - 0 & m <= len W3 - 0 by XREAL_1:10;
then W3.(m+1) Joins W3.m,W3.(m+2),G1
by GLIB_001:def 3;
then W3.(m+1) Joins W3.m,W3.last(),G1;
then W3.(m+1) Joins W3.m,w,G1 by A7, GLIB_001:def 23;
then A11: W3.m = v by A2, A3, GLIB_006:133;
set W = W3.cut(1,m);
W is_Walk_from W3.1,W3.m by A9, A10, GLIB_001:37, POLYFORM:4;
then W is_Walk_from W3.first(),W3.m;
then W is_Walk_from W1.first(),W3.m by A6, GLIB_001:def 23;
then W is_Walk_from W1.first(),W2.last() by A1, A11, GLIB_001:def 23;
then A12: W is_Walk_from W1.first(),W1.last() by A1;
A13: len W + 1 = m + 1 by A9, A10, GLIB_001:36, POLYFORM:4;
W1 is minlength by A1, Th61;
then len W + 2 >= len W1 + 2 by A12, CHORD:def 2, XREAL_1:6;
hence len W3 >= len W1.addEdge(e) by A4, A5, A13, GLIB_001:64;
end;
hence thesis by CHORD:def 2;
end;
suppose w in the_Vertices_of G2;
then G1 == G2 by GLIB_006:def 12;
then not e in the_Edges_of G1 by A2, GLIB_000:def 34;
then not e in W1.last().edgesInOut();
hence thesis by A1, Th36, Th61;
end;
end;
theorem
for G2 being _Graph, v,e,x being object, w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
for W1 being Walk of G1, W2 being Walk of G2
st W1 = W2 & W2 is minlength & W2 is_Walk_from x,w & not e in the_Edges_of G2
holds W1.addEdge(e) is minlength
proof
let G2 be _Graph, v,e,x be object, w be Vertex of G2;
let G1 be addAdjVertex of G2,v,e,w;
let W1 be Walk of G1, W2 be Walk of G2;
assume that
A1: W1 = W2 & W2 is minlength & W2 is_Walk_from x,w and
A2: not e in the_Edges_of G2;
per cases;
suppose A3: not v in the_Vertices_of G2;
then e Joins v,w,G1 by A2, GLIB_006:132;
then A4: e Joins w,v,G1 by GLIB_000:14;
A5: w = W2.last() by A1, GLIB_001:def 23
.= W1.last() by A1;
now
let W3 be Walk of G1;
assume W3 is_Walk_from W1.addEdge(e).first(),W1.addEdge(e).last();
then W3 is_Walk_from W1.first(),W1.addEdge(e).last()
by A4, A5, GLIB_001:63;
then A6: W3 is_Walk_from W1.first(),v by A4, A5, GLIB_001:63;
then A7: W3 is_Walk_from W2.first(),v by A1;
now
assume A8: W3 is trivial;
W2.first() = W3.first() by A7, GLIB_001:def 23
.= W3.last() by A8, GLIB_001:127
.= v by A7, GLIB_001:def 23;
hence contradiction by A3;
end;
then A9: 3-2 <= len W3 - 2 by GLIB_001:125, XREAL_1:9;
then reconsider m=len W3-2 as odd Element of NAT by INT_1:3, POLYFORM:5;
A10: m < len W3 - 0 & m <= len W3 - 0 by XREAL_1:10;
then W3.(m+1) Joins W3.m,W3.(m+2),G1
by GLIB_001:def 3;
then W3.(m+1) Joins W3.m,W3.last(),G1;
then W3.(m+1) Joins W3.m,v,G1 by A7, GLIB_001:def 23;
then W3.(m+1) Joins v,W3.m,G1 by GLIB_000:14;
then A11: W3.m = w by A2, A3, GLIB_006:134;
set W = W3.cut(1,m);
W is_Walk_from W3.1,W3.m by A9, A10, GLIB_001:37, POLYFORM:4;
then W is_Walk_from W3.first(),W3.m;
then W is_Walk_from W1.first(),W3.m by A6, GLIB_001:def 23;
then W is_Walk_from W1.first(),W2.last() by A1, A11, GLIB_001:def 23;
then A12: W is_Walk_from W1.first(),W1.last() by A1;
A13: len W + 1 = m + 1 by A9, A10, GLIB_001:36, POLYFORM:4;
W1 is minlength by A1, Th61;
then len W + 2 >= len W1 + 2 by A12, CHORD:def 2, XREAL_1:6;
hence len W3 >= len W1.addEdge(e) by A4, A5, A13, GLIB_001:64;
end;
hence thesis by CHORD:def 2;
end;
suppose v in the_Vertices_of G2;
then G1 == G2 by GLIB_006:def 12;
then not e in the_Edges_of G1 by A2, GLIB_000:def 34;
then not e in W1.last().edgesInOut();
hence thesis by A1, Th36, Th61;
end;
end;
registration
cluster non empty non non-Dmulti non non-multi for Graph-yielding Function;
existence
proof
set G = the non non-Dmulti non non-multi _Graph;
take F = NAT --> G;
set n = the Nat;
F.n = G by ORDINAL1:def 12, FUNCOP_1:7;
hence thesis;
end;
end;
registration
cluster non empty non acyclic non connected for Graph-yielding Function;
existence
proof
set G0 = the non connected _Graph;
set v = the Vertex of G0;
set G = the addEdge of G0,v,the_Edges_of G0,v;
take F = NAT --> G;
A1: v in G0.reachableFrom(v) by GLIB_002:9;
set n = the Nat;
F.n = G by ORDINAL1:def 12, FUNCOP_1:7;
hence thesis by A1, GLIB_006:120;
end;
end;
registration
cluster non empty non edgeless for Graph-yielding Function;
existence
proof
take the non empty non acyclic Graph-yielding Function;
thus thesis;
end;
end;
registration
cluster non empty non loopfull for Graph-yielding Function;
existence
proof
take the non empty edgeless Graph-yielding Function;
thus thesis;
end;
end;
begin :: into GLIB_007
theorem
for G2,G3 being _Graph, V, E being set, G1 being addVertices of G3, V
for G4 being reverseEdgeDirections of G3, E
holds G2 is reverseEdgeDirections of G1, E iff G2 is addVertices of G4, V
proof
let G2, G3 be _Graph, V, E be set, G1 be addVertices of G3, V;
let G4 be reverseEdgeDirections of G3, E;
per cases;
suppose A1: E c= the_Edges_of G3;
then A2: E c= the_Edges_of G1 by GLIB_006:def 10;
hereby
assume A3: G2 is reverseEdgeDirections of G1, E;
then A4: the_Vertices_of G2 = the_Vertices_of G1 by A2, GLIB_007:def 1
.= the_Vertices_of G3 \/ V by GLIB_006:def 10
.= the_Vertices_of G4 \/ V by A1, GLIB_007:def 1;
then A5: the_Vertices_of G4 c= the_Vertices_of G2 by XBOOLE_1:7;
now
let e,v,w be object;
assume A6: e DJoins v,w,G4;
per cases;
suppose A7: e in E;
then e DJoins w,v,G3 by A1, A6, GLIB_007:7;
then e DJoins w,v,G1 by GLIB_006:85;
hence e DJoins v,w,G2 by A2, A3, A7, GLIB_007:7;
end;
suppose A8: not e in E;
then e DJoins v,w,G3 by A1, A6, GLIB_007:8;
then e DJoins v,w,G1 by GLIB_006:85;
hence e DJoins v,w,G2 by A2, A3, A8, GLIB_007:8;
end;
end;
then A9: G2 is Supergraph of G4 by A5, Th50;
A10: the_Edges_of G2 = the_Edges_of G1 by A2, A3, GLIB_007:def 1
.= the_Edges_of G3 by GLIB_006:def 10
.= the_Edges_of G4 by A1, GLIB_007:def 1;
A11: the_Source_of G2 = the_Source_of G1 +* ((the_Target_of G1) | E)
by A2, A3, GLIB_007:def 1
.= the_Source_of G3 +* ((the_Target_of G1) | E) by GLIB_006:def 10
.= the_Source_of G3 +* ((the_Target_of G3) | E) by GLIB_006:def 10
.= the_Source_of G4 by A1, GLIB_007:def 1;
the_Target_of G2 = the_Target_of G1 +* ((the_Source_of G1) | E)
by A2, A3, GLIB_007:def 1
.= the_Target_of G3 +* ((the_Source_of G1) | E) by GLIB_006:def 10
.= the_Target_of G3 +* ((the_Source_of G3) | E) by GLIB_006:def 10
.= the_Target_of G4 by A1, GLIB_007:def 1;
hence G2 is addVertices of G4, V by A4, A9, A10, A11, GLIB_006:def 10;
end;
assume A12: G2 is addVertices of G4, V;
then A13: the_Vertices_of G2 = the_Vertices_of G4 \/ V by GLIB_006:def 10
.= the_Vertices_of G3 \/ V by A1, GLIB_007:def 1
.= the_Vertices_of G1 by GLIB_006:def 10;
A14: the_Edges_of G2 = the_Edges_of G4 by A12, GLIB_006:def 10
.= the_Edges_of G3 by A1, GLIB_007:def 1
.= the_Edges_of G1 by GLIB_006:def 10;
A15: the_Source_of G2 = the_Source_of G4 by A12, GLIB_006:def 10
.= the_Source_of G3 +* ((the_Target_of G3)|E) by A1, GLIB_007:def 1
.= the_Source_of G1 +* ((the_Target_of G3)|E) by GLIB_006:def 10
.= the_Source_of G1 +* ((the_Target_of G1)|E) by GLIB_006:def 10;
the_Target_of G2 = the_Target_of G4 by A12, GLIB_006:def 10
.= the_Target_of G3 +* ((the_Source_of G3)|E) by A1, GLIB_007:def 1
.= the_Target_of G1 +* ((the_Source_of G3)|E) by GLIB_006:def 10
.= the_Target_of G1 +* ((the_Source_of G1)|E) by GLIB_006:def 10;
hence thesis by A2, A13, A14, A15, GLIB_007:def 1;
end;
suppose A16: not E c= the_Edges_of G3;
then A17: not E c= the_Edges_of G1 by GLIB_006:def 10;
A18: G4 == G3 by A16, GLIB_007:def 1;
hereby
assume G2 is reverseEdgeDirections of G1, E;
then G2 == G1 by A17, GLIB_007:def 1;
then G2 is addVertices of G3, V by GLIB_006:80;
hence G2 is addVertices of G4, V by A18, GLIB_008:32;
end;
assume G2 is addVertices of G4, V;
then G2 is addVertices of G3, V by A18, GLIB_008:32;
then G1 == G2 by GLIB_006:77;
hence thesis by A17, GLIB_007:def 1;
end;
end;
theorem Th66: :: ThD3
for G2,G3 being _Graph, v,e,w being object
for G1 being addEdge of G3,v,e,w st not e in the_Edges_of G3
holds G2 is reverseEdgeDirections of G1, {e} iff G2 is addEdge of G3,w,e,v
proof
let G2, G3 be _Graph, v,e,w be object;
let G1 be addEdge of G3,v,e,w;
assume A1: not e in the_Edges_of G3;
per cases;
suppose A2: v in the_Vertices_of G3 & w in the_Vertices_of G3;
then the_Edges_of G1 = the_Edges_of G3 \/ {e} by A1, GLIB_006:def 11;
then A3: {e} c= the_Edges_of G1 by XBOOLE_1:7;
dom the_Source_of G1 = the_Edges_of G1 &
dom the_Target_of G1 = the_Edges_of G1 by FUNCT_2:def 1;
then A4: e in dom the_Source_of G1 & e in dom the_Target_of G1 &
e is set by A3, ZFMISC_1:31, TARSKI:1;
set S = the_Source_of G3, T = the_Target_of G3;
hereby
assume A5: G2 is reverseEdgeDirections of G1, {e};
then A6: the_Vertices_of G2 = the_Vertices_of G1 by A3, GLIB_007:def 1
.= the_Vertices_of G3 by A2, GLIB_006:102;
now
let e0,v0,w0 be object;
assume A7: e0 DJoins v0,w0,G3;
then e0 in the_Edges_of G3 by GLIB_000:def 14;
then A8: not e0 in {e} by A1, TARSKI:def 1;
v0 is set & w0 is set by TARSKI:1;
then e0 DJoins v0,w0,G1 by A7, GLIB_006:70;
hence e0 DJoins v0,w0,G2 by A3, A5, A8, GLIB_007:8;
end;
then A9: G2 is Supergraph of G3 by A6, Th50;
A10: the_Edges_of G2 = the_Edges_of G1 by A3, A5, GLIB_007:def 1
.= the_Edges_of G3 \/ {e} by A1, A2, GLIB_006:def 11;
A11: the_Source_of G2 = the_Source_of G1 +* ((the_Target_of G1) | {e})
by A5, A3, GLIB_007:def 1
.= the_Source_of G1 +* (e .--> (the_Target_of G1).e) by A4, FUNCT_7:6
.= S +* (e .--> v) +* (e .--> (the_Target_of G1).e)
by A1, A2, GLIB_006:def 11
.= S +* (e .--> v) +* (e .--> (T +* (e .--> w)).e)
by A1, A2, GLIB_006:def 11
.= S +* (e .--> v) +* (e .--> w) by FUNCT_4:113
.= S +* (e .--> w) by FUNCT_4:114;
the_Target_of G2 = the_Target_of G1 +* ((the_Source_of G1) | {e})
by A5, A3, GLIB_007:def 1
.= the_Target_of G1 +* (e .--> (the_Source_of G1).e) by A4, FUNCT_7:6
.= T +* (e .--> w) +* (e .--> (the_Source_of G1).e)
by A1, A2, GLIB_006:def 11
.= T +* (e .--> w) +* (e .--> (S +* (e .--> v)).e)
by A1, A2, GLIB_006:def 11
.= T +* (e .--> w) +* (e .--> v) by FUNCT_4:113
.= T +* (e .--> v) by FUNCT_4:114;
hence G2 is addEdge of G3,w,e,v
by A1, A2, A6, A9, A10, A11, GLIB_006: def 11;
end;
assume A12: G2 is addEdge of G3,w,e,v;
then A13: the_Vertices_of G2 = the_Vertices_of G3 by A2, GLIB_006:102
.= the_Vertices_of G1 by A2, GLIB_006:102;
A14: the_Edges_of G2
= the_Edges_of G3 \/ {e} by A1, A2, A12, GLIB_006:def 11
.= the_Edges_of G1 by A1, A2, GLIB_006:def 11;
A15: the_Source_of G2 = S +* (e .--> w) by A1, A2, A12, GLIB_006:def 11
.= S +* (e .--> v) +* (e .--> w) by FUNCT_4:114
.= S +* (e .--> v) +* (e .--> (T +* (e .--> w)).e) by FUNCT_4:113
.= S +* (e .--> v) +* (e .--> (the_Target_of G1).e)
by A1, A2, GLIB_006:def 11
.= the_Source_of G1 +* (e .--> (the_Target_of G1).e)
by A1, A2, GLIB_006:def 11
.= the_Source_of G1 +* ((the_Target_of G1) | {e}) by A4, FUNCT_7:6;
the_Target_of G2 = T +* (e .--> v) by A1, A2, A12, GLIB_006:def 11
.= T +* (e .--> w) +* (e .--> v) by FUNCT_4:114
.= T +* (e .--> w) +* (e .--> (S +* (e .--> v)).e) by FUNCT_4:113
.= T +* (e .--> w) +* (e .--> (the_Source_of G1).e)
by A1, A2, GLIB_006:def 11
.= the_Target_of G1 +* (e .--> (the_Source_of G1).e)
by A1, A2, GLIB_006:def 11
.= the_Target_of G1 +* ((the_Source_of G1) | {e}) by A4, FUNCT_7:6;
hence thesis by A3, A13, A14, A15, GLIB_007:def 1;
end;
suppose A16: not(v in the_Vertices_of G3 & w in the_Vertices_of G3);
then A17: G1 == G3 by GLIB_006:def 11;
then the_Edges_of G1 = the_Edges_of G3 by GLIB_000:def 34;
then A18: not {e} c= the_Edges_of G1 by A1, ZFMISC_1:31;
hereby
assume G2 is reverseEdgeDirections of G1, {e};
then G2 == G1 by A18, GLIB_007:def 1;
then A19: G2 == G3 by A17, GLIB_000:85;
then G2 is Supergraph of G3 by GLIB_006:59;
hence G2 is addEdge of G3,w,e,v by A16, A19, GLIB_006:def 11;
end;
assume G2 is addEdge of G3,w,e,v;
then G2 == G3 by A16, GLIB_006:def 11;
then G2 == G1 by A17, GLIB_000:85;
hence thesis by A18, GLIB_007:def 1;
end;
end;
theorem
for G2, G3 being _Graph, v,e,w being object
for G1 being addAdjVertex of G3,v,e,w st not e in the_Edges_of G3 holds
G2 is reverseEdgeDirections of G1, {e} iff G2 is addAdjVertex of G3,w,e,v
proof
let G2, G3 be _Graph, v,e,w be object;
let G1 be addAdjVertex of G3,v,e,w;
assume A1: not e in the_Edges_of G3;
per cases;
suppose A2: v in the_Vertices_of G3 & not w in the_Vertices_of G3;
then consider G4 being addVertex of G3,w such that
A3: G1 is addEdge of G4,v,e,w by A1, GLIB_006:125;
A4: the_Edges_of G4 = the_Edges_of G3 by GLIB_006:def 10;
hereby
assume G2 is reverseEdgeDirections of G1, {e};
then G2 is addEdge of G4,w,e,v by A1, A3, A4, Th66;
hence G2 is addAdjVertex of G3,w,e,v by A1, A2, GLIB_006:128;
end;
assume G2 is addAdjVertex of G3,w,e,v;
then consider G5 being addVertex of G3,w such that
A5: G2 is addEdge of G5,w,e,v by A1, A2, GLIB_006:126;
G2 is addEdge of G4,w,e,v by A5, GLIB_006:77, GLIB_008:36;
hence G2 is reverseEdgeDirections of G1, {e} by A1, A3, A4, Th66;
end;
suppose A6: not v in the_Vertices_of G3 & w in the_Vertices_of G3;
then consider G4 being addVertex of G3,v such that
A7: G1 is addEdge of G4,v,e,w by A1, GLIB_006:126;
A8: the_Edges_of G4 = the_Edges_of G3 by GLIB_006:def 10;
hereby
assume G2 is reverseEdgeDirections of G1, {e};
then G2 is addEdge of G4,w,e,v by A1, A7, A8, Th66;
hence G2 is addAdjVertex of G3,w,e,v by A1, A6, GLIB_006:127;
end;
assume G2 is addAdjVertex of G3,w,e,v;
then consider G5 being addVertex of G3,v such that
A9: G2 is addEdge of G5,w,e,v by A1, A6, GLIB_006:125;
G2 is addEdge of G4,w,e,v by A9, GLIB_006:77, GLIB_008:36;
hence G2 is reverseEdgeDirections of G1, {e} by A1, A7, A8, Th66;
end;
suppose A10: not((v in the_Vertices_of G3 & not w in the_Vertices_of G3) or
(not v in the_Vertices_of G3 & w in the_Vertices_of G3));
then A11: G1 == G3 by GLIB_006:def 12;
then the_Edges_of G1 = the_Edges_of G3 by GLIB_000:def 34;
then A12: not {e} c= the_Edges_of G1 by A1, ZFMISC_1:31;
hereby
assume G2 is reverseEdgeDirections of G1, {e};
then G2 == G1 by A12, GLIB_007:def 1;
then A13: G2 == G3 by A11, GLIB_000:85;
then G2 is Supergraph of G3 by GLIB_006:59;
hence G2 is addAdjVertex of G3,w,e,v by A10, A13, GLIB_006:def 12;
end;
assume G2 is addAdjVertex of G3,w,e,v;
then G2 == G3 by A10, GLIB_006:def 12;
then G2 == G1 by A11, GLIB_000:85;
hence thesis by A12, GLIB_007:def 1;
end;
end;
Lm3:
for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
for W1 being Walk of G1, W2 being Walk of G2
st W1 = W2 holds W1 is minlength implies W2 is minlength
proof
let G1 be _Graph, E be set, G2 be reverseEdgeDirections of G1, E;
let W1 be Walk of G1, W2 be Walk of G2;
assume A1: W1 = W2 & W1 is minlength;
now
let W4 be Walk of G2;
reconsider W3 = W4 as Walk of G1 by GLIB_007:15;
assume W4 is_Walk_from W2.first(),W2.last();
then W3 is_Walk_from W2.first(),W2.last() by GLIB_001:19;
then W3 is_Walk_from W1.first(),W2.last() by A1;
then W3 is_Walk_from W1.first(),W1.last() by A1;
hence len W4 >= len W2 by A1, CHORD:def 2;
end;
hence thesis by CHORD:def 2;
end;
theorem
for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
for W1 being Walk of G1, W2 being Walk of G2
st W1 = W2 holds W1 is minlength iff W2 is minlength
proof
let G1 be _Graph, E be set, G2 be reverseEdgeDirections of G1, E;
let W1 be Walk of G1, W2 be Walk of G2;
assume A1: W1 = W2;
hence W1 is minlength implies W2 is minlength by Lm3;
G1 is reverseEdgeDirections of G2, E by GLIB_007:3;
hence thesis by A1, Lm3;
end;
begin :: into GLIB_008
theorem
for G1 being edgeless _Graph, G2 being _Graph
holds G1 is Subgraph of G2 iff the_Vertices_of G1 c= the_Vertices_of G2
proof
let G1 be edgeless _Graph, G2 be _Graph;
thus G1 is Subgraph of G2 implies the_Vertices_of G1 c= the_Vertices_of G2
by GLIB_000:def 32;
assume A1: the_Vertices_of G1 c= the_Vertices_of G2;
for e being set st e in the_Edges_of G1 holds
(the_Source_of G1).e = (the_Source_of G2).e &
(the_Target_of G1).e = (the_Target_of G2).e;
hence thesis by A1, XBOOLE_1:2, GLIB_000:def 32;
end;
registration
cluster loopless non edgeless for _Graph;
existence
proof :: construct a K_2
set G0 = the _trivial loopless _Graph;
set v = the Vertex of G0;
set G = the addAdjVertex of G0,v,the_Edges_of G0,the_Vertices_of G0;
take G;
thus thesis;
end;
end;
begin :: into GLIB_009
registration
let G be _Graph;
cluster plain spanning acyclic for Subgraph of G;
existence
proof
set H0 = the spanning acyclic Subgraph of G;
set H = H0 | _GraphSelectors;
A1: H == H0 by GLIB_000:128;
then H is Subgraph of H0 by GLIB_000:87;
then reconsider H as Subgraph of G by GLIB_000:43;
take H;
the_Vertices_of H = the_Vertices_of H0 by A1, GLIB_000:def 34
.= the_Vertices_of G by GLIB_000:def 33;
hence thesis by A1, GLIB_002:44, GLIB_000:def 33;
end;
cluster plain Tree-like for Subgraph of G;
existence
proof
set H0 = the Tree-like Subgraph of G;
set H = H0 | _GraphSelectors;
A2: H == H0 by GLIB_000:128;
then H is Subgraph of H0 by GLIB_000:87;
then reconsider H as Subgraph of G by GLIB_000:43;
take H;
A3: H is acyclic by A2, GLIB_002:44;
H is connected by A2, GLIB_002:8;
hence thesis by A3;
end;
cluster plain for Component of G;
existence
proof
set H0 = the Component of G;
set H = H0 | _GraphSelectors;
H == H0 by GLIB_000:128;
then reconsider H as Component of G by Th39;
take H;
thus thesis;
end;
end;
theorem
for G being plain _Graph holds G = createGraph(the_Vertices_of G,
the_Edges_of G, the_Source_of G, the_Target_of G)
proof
let G be plain _Graph;
set H = createGraph(the_Vertices_of G, the_Edges_of G,
the_Source_of G, the_Target_of G);
the_Vertices_of G = the_Vertices_of H &
the_Edges_of G = the_Edges_of H &
the_Source_of G = the_Source_of H &
the_Target_of G = the_Target_of H;
hence thesis by GLIB_000:def 34, GLIB_009:44;
end;
theorem
for G being _Graph, H being removeLoops of G
holds the_Edges_of G = G.loops() iff H is edgeless
proof
let G be _Graph, H be removeLoops of G;
thus the_Edges_of G = G.loops() implies H is edgeless;
assume A1: H is edgeless;
the_Edges_of G \ G.loops() = the_Edges_of H by GLIB_000:53
.= {} by A1;
then the_Edges_of G c= G.loops() by XBOOLE_1:37;
hence thesis by XBOOLE_0:def 10;
end;
theorem
for G being _Graph, H being removeLoops of G, H9 being loopless Subgraph of G
holds H9 is Subgraph of H
proof
let G be _Graph, H be removeLoops of G, H9 be loopless Subgraph of G;
the_Vertices_of H = the_Vertices_of G by GLIB_000:53;
then A1: the_Vertices_of H9 c= the_Vertices_of H;
A2: the_Edges_of H = the_Edges_of G \ G.loops() by GLIB_000:53;
the_Edges_of H9 /\ G.loops() = {}
proof
assume the_Edges_of H9 /\ G.loops() <> {};
then consider x being object such that
A3: x in the_Edges_of H9 /\ G.loops() by XBOOLE_0:def 1;
A4: x in the_Edges_of H9 & x in G.loops() by A3, XBOOLE_0:def 4;
then consider v being object such that
A5: x Joins v,v,G by GLIB_009:def 2;
x is set & v is set by TARSKI:1;
then x Joins v,v,H9 by A4, A5, GLIB_000:73;
hence contradiction by GLIB_000:18;
end;
then the_Edges_of H9 misses G.loops() by XBOOLE_0:def 7;
hence thesis by A1, A2, XBOOLE_1:86, GLIB_000:44;
end;
theorem
for G1 being _Graph, G2 being removeLoops of G1
for W1 being minlength Walk of G1 holds W1 is Walk of G2
proof
let G1 be _Graph, G2 be removeLoops of G1;
let W1 be minlength Walk of G1;
reconsider P = W1 as Path of G1 by CHORD:36;
now
assume P.edges() meets G1.loops();
then consider v,e being object such that
A1: e Joins v,v,G1 & P = G1.walkOf(v,e,v) by GLIB_009:57;
reconsider v as Vertex of G1 by A1, GLIB_000:13;
A2: P.first() = v & P.last() = v & len P = 3 by A1, GLIB_001:14,15;
len G1.walkOf(v) = 1 by GLIB_001:13;
hence contradiction by A2, GLIB_001:13, CHORD:def 2;
end;
hence thesis by Th38;
end;
theorem
for G1 being _Graph, G2 being removeLoops of G1
for W1 being Walk of G1, W2 being Walk of G2
st W1 = W2 holds W1 is minlength iff W2 is minlength
proof
let G1 be _Graph, G2 be removeLoops of G1;
let W1 be Walk of G1, W2 be Walk of G2;
assume A1: W1 = W2;
hence W1 is minlength implies W2 is minlength by Th47;
assume A2: W2 is minlength;
now
let W be Walk of G1;
set P = the Path of W;
assume W is_Walk_from W1.first(),W1.last();
then A3: P is_Walk_from W1.first(),W1.last() by GLIB_001:160;
per cases by GLIB_009:57;
suppose P.edges() misses G1.loops();
then reconsider W9 = P as Walk of G2 by Th38;
W9 is_Walk_from W1.first(),W1.last() by A3, GLIB_001:19;
then W9 is_Walk_from W2.first(),W1.last() by A1;
then W9 is_Walk_from W2.first(),W2.last() by A1;
then A4: len P >= len W1 by A1, A2, CHORD:def 2;
len W >= len P by GLIB_001:162;
hence len W >= len W1 by A4, XXREAL_0:2;
end;
suppose ex v,e being object st e Joins v,v,G1 & P = G1.walkOf(v,e,v);
then consider v,e being object such that
A5: e Joins v,v,G1 & P = G1.walkOf(v,e,v);
P.first() = v & P.last() = v by A5, GLIB_001:15;
then W1.first() = v & W1.last() = v by A3, GLIB_001:def 23;
then A6: W2.first() = v & W2.last() = v by A1;
then reconsider v as Vertex of G2;
W2 is_Walk_from v,v by A6, GLIB_001:def 23;
then W2 = G2.walkOf(v) by A2, Th48;
then A7: len P = 3 & len W2 = 1 by A5, GLIB_001:13, GLIB_001:14;
len W >= len P by GLIB_001:162;
hence len W >= len W1 by A1, A7, XXREAL_0:2;
end;
end;
hence thesis by CHORD:def 2;
end;
theorem Th75:
for G1 being _Graph, G2 being removeLoops of G1
for v1,w1 being Vertex of G1, v2,w2 being Vertex of G2
st v1 = v2 & w1 = w2 & v1 <> w1
holds v1,w1 are_adjacent iff v2,w2 are_adjacent
proof
let G1 be _Graph, G2 be removeLoops of G1;
let v1,w1 be Vertex of G1, v2,w2 be Vertex of G2;
assume A1: v1 = v2 & w1 = w2 & v1 <> w1;
hereby
assume v1,w1 are_adjacent;
then w1 in v1.allNeighbors() \ {v1} by A1, Th42, ZFMISC_1:56;
then w2 in v2.allNeighbors() by A1, GLIBPRE0:63;
hence v2,w2 are_adjacent by Th42;
end;
assume v2,w2 are_adjacent;
then w2 in v2.allNeighbors() by Th42;
then w1 in v1.allNeighbors() \ {v1} by A1, GLIBPRE0:63;
hence v1,w1 are_adjacent by Th42, ZFMISC_1:56;
end;
theorem Th76:
for G1 being _Graph, G2 being removeParallelEdges of G1
for v1,w1 being Vertex of G1, v2,w2 being Vertex of G2
st v1 = v2 & w1 = w2 holds v1,w1 are_adjacent iff v2,w2 are_adjacent
proof
let G1 be _Graph, G2 be removeParallelEdges of G1;
let v1,w1 be Vertex of G1, v2,w2 be Vertex of G2;
assume A1: v1 = v2 & w1 = w2;
hereby
assume v1,w1 are_adjacent;
then w1 in v1.allNeighbors() by Th42;
then w2 in v2.allNeighbors() by A1, GLIBPRE0:64;
hence v2,w2 are_adjacent by Th42;
end;
assume v2,w2 are_adjacent;
then w2 in v2.allNeighbors() by Th42;
then w1 in v1.allNeighbors() by A1, GLIBPRE0:64;
hence v1,w1 are_adjacent by Th42;
end;
theorem Th77:
for G1 being _Graph, G2 being removeDParallelEdges of G1
for v1,w1 being Vertex of G1, v2,w2 being Vertex of G2
st v1 = v2 & w1 = w2 holds v1,w1 are_adjacent iff v2,w2 are_adjacent
proof
let G1 be _Graph, G2 be removeDParallelEdges of G1;
let v1,w1 be Vertex of G1, v2,w2 be Vertex of G2;
assume A1: v1 = v2 & w1 = w2;
hereby
assume v1,w1 are_adjacent;
then w1 in v1.allNeighbors() by Th42;
then w2 in v2.allNeighbors() by A1, GLIBPRE0:65;
hence v2,w2 are_adjacent by Th42;
end;
assume v2,w2 are_adjacent;
then w2 in v2.allNeighbors() by Th42;
then w1 in v1.allNeighbors() by A1, GLIBPRE0:65;
hence v1,w1 are_adjacent by Th42;
end;
theorem
for G1 being _Graph, G2 being SimpleGraph of G1
for v1,w1 being Vertex of G1, v2,w2 being Vertex of G2
st v1 = v2 & w1 = w2 & v1 <> w1
holds v1,w1 are_adjacent iff v2,w2 are_adjacent
proof
let G1 be _Graph, G2 be SimpleGraph of G1;
let v1,w1 be Vertex of G1, v2,w2 be Vertex of G2;
assume A1: v1 = v2 & w1 = w2 & v1 <> w1;
consider G9 being removeParallelEdges of G1 such that
A2: G2 is removeLoops of G9 by GLIB_009:119;
reconsider v9 = v2, w9 = w2 as Vertex of G9 by A2, GLIB_000:def 33;
v1,w1 are_adjacent iff v9,w9 are_adjacent by A1, Th76;
hence thesis by A1, A2, Th75;
end;
theorem
for G1 being _Graph, G2 being DSimpleGraph of G1
for v1,w1 being Vertex of G1, v2,w2 being Vertex of G2
st v1 = v2 & w1 = w2 & v1 <> w1
holds v1,w1 are_adjacent iff v2,w2 are_adjacent
proof
let G1 be _Graph, G2 be DSimpleGraph of G1;
let v1,w1 be Vertex of G1, v2,w2 be Vertex of G2;
assume A1: v1 = v2 & w1 = w2 & v1 <> w1;
consider G9 being removeDParallelEdges of G1 such that
A2: G2 is removeLoops of G9 by GLIB_009:120;
reconsider v9 = v2, w9 = w2 as Vertex of G9 by A2, GLIB_000:def 33;
v1,w1 are_adjacent iff v9,w9 are_adjacent by A1, Th77;
hence thesis by A1, A2, Th75;
end;
begin :: into GLIB_010
theorem Th80:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v1 being Vertex of G1, v2 being Vertex of G2
st v2 = F_V.v1 & F is total
holds F_V.:G1.reachableFrom(v1) c= G2.reachableFrom(v2)
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v2 = F_V.v1 & F is total;
then reconsider F0 = F as non empty PGraphMapping of G1, G2;
now
let y be object;
assume y in F_V.:G1.reachableFrom(v1);
then consider x being object such that
A2: x in dom F_V & x in G1.reachableFrom(v1) & y=F_V.x by FUNCT_1:def 6;
consider W1 being Walk of G1 such that
A3: W1 is_Walk_from v1,x by A2, GLIB_002:def 5;
reconsider W1 as F0-defined Walk of G1 by A1, GLIB_010:121;
F0.:W1 is_Walk_from F0_V.v1,F0_V.x by A3, GLIB_010:132;
hence y in G2.reachableFrom(v2) by A1, A2, GLIB_002:def 5;
end;
hence thesis by TARSKI:def 3;
end;
:: onto would be enough, but there are no theorems for that
:: (there could be multiple walks of G1 mapping to a specific one of G2)
theorem Th81:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 in dom F_V & v2 = F_V.v1 & F is one-to-one onto
holds G2.reachableFrom(v2) c= F_V.:G1.reachableFrom(v1)
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 in dom F_V & v2 = F_V.v1 & F is one-to-one onto;
then reconsider F0 = F as non empty one-to-one PGraphMapping of G1, G2;
A2: F0"_V.v2 = v1 by A1, FUNCT_1:34;
now
let y be object;
assume y in G2.reachableFrom(v2);
then consider W2 being Walk of G2 such that
A3: W2 is_Walk_from v2,y by GLIB_002:def 5;
W2 is F0-valued by A1, GLIB_010:122;
then reconsider W2 as F0"-defined Walk of G2;
F0".:W2 is_Walk_from F0"_V.v2,F0"_V.y by A3, GLIB_010:132;
then A4: F0"_V.y in G1.reachableFrom(v1) by A2, GLIB_002:def 5;
y is Vertex of G2 & rng F_V = the_Vertices_of G2
by A1, A3, GLIB_001:18, GLIB_010:def 12;
then F0_V".y in dom F_V & y = F0_V.(F0_V".y) by FUNCT_1:32;
hence y in F_V.:G1.reachableFrom(v1) by A4, FUNCT_1:def 6;
end;
hence thesis by TARSKI:def 3;
end;
theorem Th82:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v1 being Vertex of G1, v2 being Vertex of G2
st v2 = F_V.v1 & F is isomorphism
holds F_V.:G1.reachableFrom(v1) = G2.reachableFrom(v2)
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v2 = F_V.v1 & F is isomorphism;
then A2: F_V.:G1.reachableFrom(v1) c= G2.reachableFrom(v2) by Th80;
the_Vertices_of G1 = dom F_V by A1, GLIB_010:def 11;
then G2.reachableFrom(v2) c= F_V.:G1.reachableFrom(v1) by A1, Th81;
hence thesis by A2, XBOOLE_0:def 10;
end;
theorem Th83:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is isomorphism holds G2.componentSet() =
the set of all F_V.:C where C is Element of G1.componentSet()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
set S = the set of all F_V.:C where C is Element of G1.componentSet();
assume A1: F is isomorphism;
now
let x be object;
reconsider X = x as set by TARSKI:1;
hereby
assume x in G2.componentSet();
then consider v2 being Vertex of G2 such that
A2: X = G2.reachableFrom(v2) by GLIB_002:def 8;
the_Vertices_of G2 = rng F_V by A1, GLIB_010:def 12;
then consider v1 being object such that
A3: v1 in dom F_V & F_V.v1 = v2 by FUNCT_1:def 3;
reconsider v1 as Vertex of G1 by A3;
A4: X = F_V.:G1.reachableFrom(v1) by A1, A2, A3, Th82;
G1.reachableFrom(v1) in G1.componentSet() by GLIB_002:def 8;
hence x in S by A4;
end;
assume x in S;
then consider C being Element of G1.componentSet() such that
A5: x = F_V.:C;
consider v1 being Vertex of G1 such that
A6: C = G1.reachableFrom(v1) by GLIB_002:def 8;
the_Vertices_of G1 = dom F_V by A1, GLIB_010:def 11;
then F_V.v1 in rng F_V by FUNCT_1:3;
then reconsider v2 = F_V.v1 as Vertex of G2;
x = G2.reachableFrom(v2) by A1, A5, A6, Th82;
hence x in G2.componentSet() by GLIB_002:def 8;
end;
hence thesis by TARSKI:2;
end;
theorem
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is isomorphism holds G1.numComponents() = G2.numComponents()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
set S = the set of all F_V.:C where C is Element of G1.componentSet();
assume A1: F is isomorphism;
A2: G1.componentSet() is non empty Subset of bool dom F_V
by A1, GLIB_010:def 11;
A3: (.:(F_V))|G1.componentSet() is one-to-one by A1, FUNCT_1:52;
A4: rng((.:(F_V))|G1.componentSet()) = S by A1, A2, Th6;
A5: dom((.:(F_V))|G1.componentSet())
= dom(.:(F_V)) /\ G1.componentSet() by RELAT_1:61
.= (bool dom F_V) /\ G1.componentSet() by FUNCT_3:def 1
.= G1.componentSet() by A2, XBOOLE_1:28;
thus G1.numComponents() = card G1.componentSet() by GLIB_002:def 9
.= card S by A3, A4, A5, CARD_1:70
.= card G2.componentSet() by A1, Th83
.= G2.numComponents() by GLIB_002:def 9;
end;
registration
let G be loopless _Graph;
cluster G-isomorphic -> loopless for _Graph;
coherence
proof
let G1 be _Graph;
assume G1 is G-isomorphic;
then consider F being PGraphMapping of G,G1 such that
A1: F is isomorphism by GLIB_010:def 23;
thus thesis by A1, GLIB_010:37;
end;
end;
theorem Th85:
for G1, G2, G3, G4 being _Graph, F1 being empty PGraphMapping of G1, G2
for F2 being empty PGraphMapping of G3, G4 holds F1 = F2
proof
let G1, G2, G3, G4 be _Graph, F1 be empty PGraphMapping of G1, G2;
let F2 be empty PGraphMapping of G3, G4;
[F1_V, F1_E] = [F2_V, F2_E];
hence thesis;
end;
theorem Th86:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
holds F | dom F = F & (rng F) |` F = F
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
per cases;
suppose A1: F is non empty;
A2: (F | dom F)_V = F_V | dom F_V by A1, GLIB_010:54
.= F_V;
(F | dom F)_E = F_E | dom F_E by A1, GLIB_010:54
.= F_E;
then [(F | dom F)_V, (F | dom F)_E] = [F_V, F_E] by A2;
hence F | dom F = F;
A3: ((rng F) |` F)_V = (rng F_V) |` F_V by A1, GLIB_010:54
.= F_V;
((rng F) |` F)_E = (rng F_E) |` F_E by A1, GLIB_010:54
.= F_E;
then [((rng F) |` F)_V, ((rng F) |` F)_E] = [F_V, F_E] by A3;
hence thesis;
end;
suppose A4: F is empty;
hence F | dom F = F by Th85;
thus thesis by A4, Th85;
end;
end;
theorem Th87:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is total holds (rng F) |` F is total
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: F is total;
A2: dom((rng F)|`F)_V = dom F_V by Th86
.= the_Vertices_of G1 by A1, GLIB_010:def 11;
dom((rng F)|`F)_E = dom F_E by Th86
.= the_Edges_of G1 by A1, GLIB_010:def 11;
hence thesis by A2, GLIB_010:def 11;
end;
theorem
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is onto holds F | dom F is onto
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: F is onto;
A2: rng(F|dom F)_V = rng F_V by Th86
.= the_Vertices_of G2 by A1, GLIB_010:def 12;
rng(F|dom F)_E = rng F_E by Th86
.= the_Edges_of G2 by A1, GLIB_010:def 12;
hence thesis by A2, GLIB_010:def 12;
end;
theorem
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
holds F is PGraphMapping of G1, rng F
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
F = (rng F) |` F by Th86;
hence thesis;
end;
theorem
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
holds F is PGraphMapping of dom F, G2
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
F = F | dom F by Th86;
hence thesis;
end;
:: Proof mostly taken from GLIB_010:46, generalization of the same
theorem Th91:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for X,Y being Subset of the_Vertices_of G1 st F is total
holds F_E.:G1.edgesBetween(X,Y) c= G2.edgesBetween(F_V.:X,F_V.:Y)
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
let X,Y be Subset of the_Vertices_of G1;
assume A1: F is total;
set f = F_E | G1.edgesBetween(X,Y);
A2: dom f = dom F_E /\ G1.edgesBetween(X,Y) by RELAT_1:61
.= the_Edges_of G1 /\ G1.edgesBetween(X,Y) by A1, GLIB_010:def 11
.= G1.edgesBetween(X,Y) by XBOOLE_1:28;
for y being object holds y in rng f implies
y in G2.edgesBetween(F_V.:X,F_V.:Y)
proof
let y be object;
assume y in rng f;
then consider x being object such that
A3: x in dom f & f.x = y by FUNCT_1:def 3;
set v = (the_Source_of G1).x, w = (the_Target_of G1).x;
A4: x SJoins X,Y,G1 by A2, A3, GLIB_000:def 30;
then per cases by GLIB_000:def 15;
suppose A5: v in X & w in Y;
then v in the_Vertices_of G1 & w in the_Vertices_of G1;
then A6: v in dom F_V & w in dom F_V by A1, GLIB_010:def 11;
A7: x in the_Edges_of G1 by A4, GLIB_000:def 15;
then A8: x in dom F_E by A1, GLIB_010:def 11;
x Joins v,w,G1 by A7, GLIB_000:def 13;
then F_E.x Joins F_V.v,F_V.w,G2 by A6, A8, GLIB_010:4;
then A9: y Joins F_V.v,F_V.w,G2 by A3, FUNCT_1:47;
F_V.v in F_V.:X & F_V.w in F_V.:Y by A5, A6, FUNCT_1:def 6;
then y SJoins F_V.:X,F_V.:Y,G2 by A9, GLIB_000:17;
hence thesis by GLIB_000:def 30;
end;
suppose A10: v in Y & w in X;
then v in the_Vertices_of G1 & w in the_Vertices_of G1;
then A11: v in dom F_V & w in dom F_V by A1, GLIB_010:def 11;
A12: x in the_Edges_of G1 by A4, GLIB_000:def 15;
then A13: x in dom F_E by A1, GLIB_010:def 11;
x Joins v,w,G1 by A12, GLIB_000:def 13;
then F_E.x Joins F_V.v,F_V.w,G2 by A11, A13, GLIB_010:4;
then A14: y Joins F_V.v,F_V.w,G2 by A3, FUNCT_1:47;
F_V.v in F_V.:Y & F_V.w in F_V.:X by A10, A11, FUNCT_1:def 6;
then y SJoins F_V.:X,F_V.:Y,G2 by A14, GLIB_000:17;
hence thesis by GLIB_000:def 30;
end;
end;
then rng f c= G2.edgesBetween(F_V.:X,F_V.:Y) by TARSKI:def 3;
hence thesis by RELAT_1:115;
end;
:: generalization of GLIB_010:7 and GLIB_010:46
theorem Th103:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2, V being set
holds F_E.:G1.edgesBetween(V) c= G2.edgesBetween(F_V.:V)
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2, V be set;
now
let e be object;
assume e in F_E.:G1.edgesBetween(V);
then consider e0 being object such that
A1: e0 in dom F_E & e0 in G1.edgesBetween(V) & F_E.e0 = e
by FUNCT_1:def 6;
set v0 = (the_Source_of G1).e0, w0 = (the_Target_of G1).e0;
A2: v0 in dom F_V & w0 in dom F_V by A1, GLIB_010:5;
e0 Joins v0,w0,G1 by A1, GLIB_000:def 13;
then A3: e Joins F_V.v0,F_V.w0,G2 by A1, A2, GLIB_010:4;
v0 in V & w0 in V by A1, GLIB_000:31;
then F_V.v0 in F_V.:V & F_V.w0 in F_V.:V by A2, FUNCT_1:def 6;
hence e in G2.edgesBetween(F_V.:V) by A3, GLIB_000:32;
end;
hence thesis by TARSKI:def 3;
end;
:: generalization of GLIB_010:86
theorem
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for X,Y being Subset of the_Vertices_of G1 st F is weak_SG-embedding onto
holds F_E.:G1.edgesBetween(X,Y) = G2.edgesBetween(F_V.:X,F_V.:Y)
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
let X,Y be Subset of the_Vertices_of G1;
assume A1: F is weak_SG-embedding onto;
then reconsider F9 = F as one-to-one PGraphMapping of G1, G2;
A2: F_E.:G1.edgesBetween(X,Y) c= G2.edgesBetween(F_V.:X,F_V.:Y) by A1, Th91;
A3: dom F_V = the_Vertices_of G1 & dom F_E = the_Edges_of G1
by A1, GLIB_010:def 11;
G1.edgesBetween(F9"_V.:(F_V.:X),F9"_V.:(F_V.:Y))
= G1.edgesBetween(F9_V"(F9_V.:X),F9_V".:(F_V.:Y)) by FUNCT_1:85
.= G1.edgesBetween(F9_V"(F9_V.:X),F9_V"(F_V.:Y)) by FUNCT_1:85
.= G1.edgesBetween(X,F9_V"(F_V.:Y)) by A3, FUNCT_1:94
.= G1.edgesBetween(X,Y) by A3, FUNCT_1:94;
then A4: F9"_E.:G2.edgesBetween(F_V.:X,F_V.:Y) c= G1.edgesBetween(X,Y)
by A1, GLIB_010:72, Th91;
A5: rng F_E = the_Edges_of G2 by A1, GLIB_010:def 12;
F_E.:(F9"_E.:G2.edgesBetween(F_V.:X,F_V.:Y))
= F_E.:(F9_E"G2.edgesBetween(F_V.:X,F_V.:Y)) by FUNCT_1:85
.= G2.edgesBetween(F_V.:X,F_V.:Y) by A5, FUNCT_1:77;
then G2.edgesBetween(F_V.:X,F_V.:Y) c= F_E.:(G1.edgesBetween(X,Y))
by A4, RELAT_1:123;
hence thesis by A2, XBOOLE_0:def 10;
end;
:: generalization of GLIB_010:87
theorem Th104:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2, V being set
st F is continuous holds F_E.:G1.edgesBetween(V) = G2.edgesBetween(F_V.:V)
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2, V be set;
assume A1: F is continuous;
A2: F_E.:G1.edgesBetween(V) c= G2.edgesBetween(F_V.:V) by Th103;
now
let e be object;
set v = (the_Source_of G2).e, w = (the_Target_of G2).e;
assume e in G2.edgesBetween(F_V.:V);
then A3: e in the_Edges_of G2 & v in F_V.:V & w in F_V.:V by GLIB_000:31;
then A4: e Joins v,w,G2 by GLIB_000:def 13;
consider v0 being object such that
A5: v0 in dom F_V & v0 in V & F_V.v0 = v by A3, FUNCT_1:def 6;
consider w0 being object such that
A6: w0 in dom F_V & w0 in V & F_V.w0 = w by A3, FUNCT_1:def 6;
consider e0 being object such that
A7: e0 Joins v0,w0,G1 & e0 in dom F_E & F_E.e0 = e
by A1, A4, A5, A6, GLIB_010:def 16;
e0 in G1.edgesBetween(V) by A5, A6, A7, GLIB_000:32;
hence e in F_E.:G1.edgesBetween(V) by A7, FUNCT_1:def 6;
end;
then G2.edgesBetween(F_V.:V) c= F_E.:G1.edgesBetween(V) by TARSKI:def 3;
hence thesis by A2, XBOOLE_0:def 10;
end;
theorem Th95:
for G1, G2 being _Graph, F being non empty one-to-one PGraphMapping of G1, G2
for W2 being F-valued Walk of G2
holds (F"W2).vertices() = F_V"W2.vertices()
proof
let G1, G2 be _Graph, F be non empty one-to-one PGraphMapping of G1, G2;
let W2 be F-valued Walk of G2;
thus (F"W2).vertices() = (F"_V).:W2.vertices() by GLIB_010:135
.= F_V"W2.vertices() by FUNCT_1:85;
end;
theorem Th96:
for G1, G2 being _Graph, F being non empty one-to-one PGraphMapping of G1, G2
for W2 being F-valued Walk of G2
holds (F"W2).edges() = F_E"W2.edges()
proof
let G1, G2 be _Graph, F be non empty one-to-one PGraphMapping of G1, G2;
let W2 be F-valued Walk of G2;
thus (F"W2).edges() = (F"_E).:W2.edges() by GLIB_010:136
.= F_E"W2.edges() by FUNCT_1:85;
end;
theorem Th97:
for G1, G2 being _Graph, F being non empty one-to-one PGraphMapping of G1, G2
for W2 being F-valued Walk of G2, v,w being object
holds W2 is_Walk_from v,w implies F"W2 is_Walk_from F"_V.v, F"_V.w
by GLIB_010:132;
theorem
for G1, G2 being _Graph, F being one-to-one PGraphMapping of G1, G2
for v1 being Vertex of G1, v2 being Vertex of G2
st v2 = F_V.v1 & F is isomorphism
holds F_V"G2.reachableFrom(v2) = G1.reachableFrom(v1)
proof
let G1, G2 be _Graph, F be one-to-one PGraphMapping of G1, G2;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v2 = F_V.v1 & F is isomorphism;
then the_Vertices_of G1 = dom F_V by GLIB_010:def 11;
then A2: F"_V.v2 = v1 by A1, FUNCT_1:34;
thus F_V"G2.reachableFrom(v2)
= F_V".:G2.reachableFrom(v2) by FUNCT_1:85
.= G1.reachableFrom(v1) by A1, A2, Th82, GLIB_010:75;
end;
theorem Th99:
for G1, G2 being _Graph
for F being PGraphMapping of G1, G2, H being Subgraph of G2
holds F_E"the_Edges_of H c= G1.edgesBetween(F_V"the_Vertices_of H)
proof
let G1, G2 be _Graph;
let F be PGraphMapping of G1, G2, H be Subgraph of G2;
now
let x be object;
assume x in F_E"the_Edges_of H;
then A1: x in dom F_E & F_E.x in the_Edges_of H by FUNCT_1:def 7;
set v = (the_Source_of G1).x, w = (the_Target_of G1).x;
A2: v in dom F_V & w in dom F_V by A1, GLIB_010:5;
A3: x Joins v,w,G1 by A1, GLIB_000:def 13;
then F_E.x Joins F_V.v,F_V.w,G2 by A1, A2, GLIB_010:4;
then F_E.x Joins F_V.v,F_V.w,H by A1, GLIB_000:73;
then F_V.v in the_Vertices_of H & F_V.w in the_Vertices_of H
by GLIB_000:13;
then v in F_V"the_Vertices_of H & w in F_V"the_Vertices_of H
by A2, FUNCT_1:def 7;
hence x in G1.edgesBetween(F_V"the_Vertices_of H) by A3, GLIB_000:32;
end;
hence thesis by TARSKI:def 3;
end;
theorem
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1, G2, H2 being Subgraph of rng F
for H1 being inducedSubgraph of G1,F_V"the_Vertices_of H2,F_E"the_Edges_of H2
holds rng(F | H1) == H2
proof
let G1, G2 be _Graph;
let F be non empty PGraphMapping of G1, G2; let H2 be Subgraph of rng F;
let H1 be inducedSubgraph of G1,F_V"the_Vertices_of H2,F_E"the_Edges_of H2;
A1: H2 is Subgraph of G2 by GLIB_000:43;
A2: F_E"the_Edges_of H2 c= G1.edgesBetween(F_V"the_Vertices_of H2)
by A1, Th99;
set v = the Vertex of H2;
v in the_Vertices_of H2;
then v in the_Vertices_of rng F;
then v in rng F_V by GLIB_010:54;
then consider x being object such that
A3: x in dom F_V & F_V.x = v by FUNCT_1:def 3;
A4: x in F_V"the_Vertices_of H2 by A3, FUNCT_1:def 7;
then A5: the_Vertices_of H1 = F_V"the_Vertices_of H2 &
the_Edges_of H1 = F_E"the_Edges_of H2 by A2, GLIB_000:def 37;
the_Vertices_of H2 c= the_Vertices_of rng F;
then A6: the_Vertices_of H2 c= rng F_V by GLIB_010:54;
the_Edges_of H2 c= the_Edges_of rng F;
then A7: the_Edges_of H2 c= rng F_E by GLIB_010:54;
x in (dom F_V) /\ the_Vertices_of H1 by A5, A3, A4, XBOOLE_0:def 4;
then x in dom(F | H1)_V by RELAT_1:61;
then A8: F | H1 is non empty;
then A9: the_Vertices_of rng(F | H1)
= rng(F_V | the_Vertices_of H1) by GLIB_010:54
.= F_V.:(F_V"the_Vertices_of H2) by A5, RELAT_1:115
.= the_Vertices_of H2 by A6, FUNCT_1:77;
the_Edges_of rng(F | H1)
= rng(F_E | the_Edges_of H1) by A8, GLIB_010:54
.= F_E.:(F_E"the_Edges_of H2) by A5, RELAT_1:115
.= the_Edges_of H2 by A7, FUNCT_1:77;
hence thesis by A1, A9, GLIB_000:86;
end;
theorem Th101:
for G1, G2 being _Graph, F being non empty PGraphMapping of G1, G2
for V2 being non empty Subset of the_Vertices_of rng F
for H being inducedSubgraph of rng F, V2
st G1.edgesBetween(F_V"the_Vertices_of H) c= dom F_E
holds F_E"the_Edges_of H = G1.edgesBetween(F_V"the_Vertices_of H)
proof
let G1, G2 be _Graph, F be non empty PGraphMapping of G1, G2;
let V2 be non empty Subset of the_Vertices_of rng F;
let H be inducedSubgraph of rng F, V2;
assume A1: G1.edgesBetween(F_V"the_Vertices_of H) c= dom F_E;
H is Subgraph of G2 by GLIB_000:43;
then A2: F_E"the_Edges_of H c= G1.edgesBetween(F_V"the_Vertices_of H)
by Th99;
now
let e be object;
set v = (the_Source_of G1).e, w = (the_Target_of G1).e;
assume A3: e in G1.edgesBetween(F_V"the_Vertices_of H);
then A4: e in dom F_E by A1;
A5: e in the_Edges_of G1 & v in F_V"the_Vertices_of H &
w in F_V"the_Vertices_of H by A3, GLIB_000:31;
then A6: v in dom F_V & F_V.v in the_Vertices_of H & w in dom F_V &
F_V.w in the_Vertices_of H by FUNCT_1:def 7;
e Joins v,w,G1 by A5, GLIB_000:def 13;
then A7: F_E.e Joins F_V.v,F_V.w,G2 by A4, A6, GLIB_010:4;
F_E.e in rng F_E by A4, FUNCT_1:3;
then F_E.e in the_Edges_of rng F by GLIB_010:54;
then F_E.e Joins F_V.v,F_V.w,rng F by A7, GLIB_000:73;
then F_E.e in (rng F).edgesBetween(the_Vertices_of H) by A6, GLIB_000:32;
then F_E.e in (rng F).edgesBetween(V2) by GLIB_000:def 37;
then F_E.e in the_Edges_of H by GLIB_000:def 37;
hence e in F_E"the_Edges_of H by A4, FUNCT_1:def 7;
end;
then G1.edgesBetween(F_V"the_Vertices_of H) c= F_E"the_Edges_of H
by TARSKI:def 3;
hence thesis by A2, XBOOLE_0:def 10;
end;
theorem
for G1, G2 being _Graph, F being non empty PGraphMapping of G1, G2
for V2 being non empty Subset of the_Vertices_of rng F
for H2 being inducedSubgraph of rng F, V2
for H1 being inducedSubgraph of G1,F_V"the_Vertices_of H2
st G1.edgesBetween(F_V"the_Vertices_of H2) c= dom F_E holds rng(F | H1) == H2
proof
let G1, G2 be _Graph, F be non empty PGraphMapping of G1, G2;
let V2 be non empty Subset of the_Vertices_of rng F;
let H2 be inducedSubgraph of rng F, V2;
let H1 be inducedSubgraph of G1,F_V"the_Vertices_of H2;
assume A1: G1.edgesBetween(F_V"the_Vertices_of H2) c= dom F_E;
A2: H2 is Subgraph of G2 by GLIB_000:43;
A3: F_E"the_Edges_of H2 = G1.edgesBetween(F_V"the_Vertices_of H2)
by A1, Th101;
set v = the Vertex of H2;
v in the_Vertices_of H2;
then v in the_Vertices_of rng F;
then v in rng F_V by GLIB_010:54;
then consider x being object such that
A4: x in dom F_V & F_V.x = v by FUNCT_1:def 3;
A5: x in F_V"the_Vertices_of H2 by A4, FUNCT_1:def 7;
then A6: the_Vertices_of H1 = F_V"the_Vertices_of H2 &
the_Edges_of H1 = F_E"the_Edges_of H2 by A3, GLIB_000:def 37;
the_Vertices_of H2 c= the_Vertices_of rng F;
then A7: the_Vertices_of H2 c= rng F_V by GLIB_010:54;
the_Edges_of H2 c= the_Edges_of rng F;
then A8: the_Edges_of H2 c= rng F_E by GLIB_010:54;
x in (dom F_V) /\ the_Vertices_of H1 by A6, A4, A5, XBOOLE_0:def 4;
then x in dom(F | H1)_V by RELAT_1:61;
then A9: F | H1 is non empty;
then A10: the_Vertices_of rng(F | H1)
= rng(F_V | the_Vertices_of H1) by GLIB_010:54
.= F_V.:(F_V"the_Vertices_of H2) by A6, RELAT_1:115
.= the_Vertices_of H2 by A7, FUNCT_1:77;
the_Edges_of rng(F | H1)
= rng(F_E | the_Edges_of H1) by A9, GLIB_010:54
.= F_E.:(F_E"the_Edges_of H2) by A6, RELAT_1:115
.= the_Edges_of H2 by A8, FUNCT_1:77;
hence thesis by A2, A10, GLIB_000:86;
end;
theorem
for G1, G2 being _Graph, F being non empty PGraphMapping of G1, G2
for V being non empty Subset of the_Vertices_of dom F
for H being inducedSubgraph of G1, V st F is continuous
holds rng(F | H) is inducedSubgraph of G2, F_V.:V
proof
let G1, G2 be _Graph, F be non empty PGraphMapping of G1, G2;
let V be non empty Subset of the_Vertices_of dom F;
A1: V is non empty Subset of the_Vertices_of G1 by XBOOLE_1:1;
let H be inducedSubgraph of G1, V;
assume A2: F is continuous;
set v = the Vertex of H;
v in the_Vertices_of H;
then v in V by A1, GLIB_000:def 37;
then v in the_Vertices_of H /\ the_Vertices_of dom F by XBOOLE_0:def 4;
then v in the_Vertices_of H /\ dom F_V by GLIB_010:54;
then v in dom((F|H)_V) by RELAT_1:61;
then A3: F | H is non empty;
then A4: the_Vertices_of rng(F|H) = rng((F|H)_V) by GLIB_010:54
.= F_V.:the_Vertices_of H by RELAT_1:115
.= F_V.:V by A1, GLIB_000:def 37;
the_Edges_of rng(F|H) = rng((F|H)_E) by A3, GLIB_010:54
.= F_E.:the_Edges_of H by RELAT_1:115
.= F_E.:G1.edgesBetween(V) by A1, GLIB_000:def 37
.= G2.edgesBetween(F_V.:V) by A2, Th104;
hence thesis by A4, GLIB_000:def 37;
end;
theorem Th106:
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1, G2, H2 being Subgraph of rng F
for H1 being inducedSubgraph of G1,F_V"the_Vertices_of H2,F_E"the_Edges_of H2
for W1 being Walk of H1 holds W1 is F-defined Walk of G1
proof
let G1, G2 be _Graph;
let F be non empty PGraphMapping of G1, G2, H2 be Subgraph of rng F;
let H1 be inducedSubgraph of G1,F_V"the_Vertices_of H2,F_E"the_Edges_of H2;
let W1 be Walk of H1;
A1: the_Vertices_of H1 = F_V"the_Vertices_of H2 &
the_Edges_of H1 = F_E"the_Edges_of H2
proof
set v = the Vertex of H2;
v in the_Vertices_of H2;
then v in the_Vertices_of rng F;
then v in rng F_V by GLIB_010:54;
then consider x being object such that
A2: x in dom F_V & F_V.x = v by FUNCT_1:def 3;
A3: F_V"the_Vertices_of H2 is non empty by A2, FUNCT_1:def 7;
H2 is Subgraph of G2 by GLIB_000:43;
then F_E"the_Edges_of H2 c= G1.edgesBetween(F_V"the_Vertices_of H2)
by Th99;
hence thesis by A3, GLIB_000:def 37;
end;
the_Vertices_of H1 c=dom F_V & the_Edges_of H1 c=dom F_E by A1, RELAT_1:132;
then A4: W1.vertices() c= dom F_V & W1.edges() c= dom F_E by XBOOLE_1:1;
reconsider W = W1 as Walk of G1 by GLIB_001:167;
W.vertices() = W1.vertices() & W.edges() = W1.edges()
by GLIB_001:98, GLIB_001:110;
hence thesis by A4, GLIB_010:def 35;
end;
theorem Th107:
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1, G2, H2 being Subgraph of rng F
for H1 being inducedSubgraph of G1,F_V"the_Vertices_of H2,F_E"the_Edges_of H2
for W1 being F-defined Walk of G1 st W1 is Walk of H1
holds F.:W1 is Walk of H2
proof
let G1, G2 be _Graph;
let F be non empty PGraphMapping of G1, G2;
let H2 be Subgraph of rng F;
let H1 be inducedSubgraph of G1,F_V"the_Vertices_of H2,F_E"the_Edges_of H2;
A1: H2 is Subgraph of G2 by GLIB_000:43;
let W1 be F-defined Walk of G1;
assume W1 is Walk of H1;
then reconsider W = W1 as Walk of H1;
A2: W.vertices() = W1.vertices() & W.edges() = W1.edges()
by GLIB_001:98, GLIB_001:110;
A3: the_Vertices_of H1 = F_V"the_Vertices_of H2 &
the_Edges_of H1 = F_E"the_Edges_of H2
proof
set v = the Vertex of H2;
v in the_Vertices_of H2;
then v in the_Vertices_of rng F;
then v in rng F_V by GLIB_010:54;
then consider x being object such that
A4: x in dom F_V & F_V.x = v by FUNCT_1:def 3;
A5: F_V"the_Vertices_of H2 is non empty by A4, FUNCT_1:def 7;
H2 is Subgraph of G2 by GLIB_000:43;
then F_E"the_Edges_of H2 c= G1.edgesBetween(F_V"the_Vertices_of H2)
by Th99;
hence thesis by A5, GLIB_000:def 37;
end;
A6: (F.:W1).vertices() c= the_Vertices_of H2
proof
(F.:W1).vertices() = F_V.:W1.vertices() by GLIB_010:135;
then A7: (F.:W1).vertices() c= F_V.:the_Vertices_of H1 by A2, RELAT_1:123;
F_V.:the_Vertices_of H1 c= the_Vertices_of H2 by A3, FUNCT_1:75;
hence thesis by A7, XBOOLE_1:1;
end;
(F.:W1).edges() c= the_Edges_of H2
proof
(F.:W1).edges() = F_E.:W1.edges() by GLIB_010:136;
then A8: (F.:W1).edges() c= F_E.:the_Edges_of H1 by A2, RELAT_1:123;
F_E.:the_Edges_of H1 c= the_Edges_of H2 by A3, FUNCT_1:75;
hence thesis by A8, XBOOLE_1:1;
end;
hence thesis by A1, A6, GLIB_001:170;
end;
theorem Th108:
for G1, G2 being _Graph, F being non empty PGraphMapping of G1, G2
for H being Subgraph of rng F, W being Walk of H
holds W is F-valued Walk of G2
proof
let G1, G2 be _Graph, F be non empty PGraphMapping of G1, G2;
let H be Subgraph of rng F, W be Walk of H;
H is Subgraph of G2 by GLIB_000:43;
then reconsider W9 = W as Walk of G2 by GLIB_001:167;
the_Vertices_of H c= the_Vertices_of rng F &
the_Edges_of H c= the_Edges_of rng F;
then W.vertices() c= the_Vertices_of rng F &
W.edges() c= the_Edges_of rng F by XBOOLE_1:1;
then W.vertices() c= rng F_V & W.edges() c= rng F_E by GLIB_010:54;
then W9.vertices() c= rng F_V & W9.edges() c= rng F_E
by GLIB_001:98, GLIB_001:110;
hence thesis by GLIB_010:def 36;
end;
theorem Th109:
for G1, G2 being _Graph, F being non empty one-to-one PGraphMapping of G1,G2
for H2 being Subgraph of rng F
for H1 being inducedSubgraph of G1,F_V"the_Vertices_of H2,F_E"the_Edges_of H2
for W2 being F-valued Walk of G2 st W2 is Walk of H2
holds F"W2 is Walk of H1
proof
let G1, G2 be _Graph, F be non empty one-to-one PGraphMapping of G1, G2;
let H2 be Subgraph of rng F;
let H1 be inducedSubgraph of G1,F_V"the_Vertices_of H2,F_E"the_Edges_of H2;
let W2 be F-valued Walk of G2;
assume W2 is Walk of H2;
then reconsider W = W2 as Walk of H2;
A1: W.vertices() = W2.vertices() & W.edges() = W2.edges()
by GLIB_001:98, GLIB_001:110;
A2: the_Vertices_of H1 = F_V"the_Vertices_of H2 &
the_Edges_of H1 = F_E"the_Edges_of H2
proof
set v = the Vertex of H2;
v in the_Vertices_of H2;
then v in the_Vertices_of rng F;
then v in rng F_V by GLIB_010:54;
then consider x being object such that
A3: x in dom F_V & F_V.x = v by FUNCT_1:def 3;
A4: F_V"the_Vertices_of H2 is non empty by A3, FUNCT_1:def 7;
H2 is Subgraph of G2 by GLIB_000:43;
then F_E"the_Edges_of H2 c= G1.edgesBetween(F_V"the_Vertices_of H2)
by Th99;
hence thesis by A4, GLIB_000:def 37;
end;
A5: (F"W2).vertices() c= the_Vertices_of H1
proof
(F"W2).vertices() = F_V"W2.vertices() by Th95;
hence thesis by A1, A2, RELAT_1:143;
end;
(F"W2).edges() c= the_Edges_of H1
proof
(F"W2).edges() = F_E"W2.edges() by Th96;
hence thesis by A1, A2, RELAT_1:143;
end;
hence thesis by A5, GLIB_001:170;
end;
theorem
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1, G2
for H2 being acyclic Subgraph of rng F
for H1 being inducedSubgraph of G1,F_V"the_Vertices_of H2,F_E"the_Edges_of H2
holds H1 is acyclic
proof
let G1, G2 be _Graph;
let F be non empty one-to-one PGraphMapping of G1, G2;
let H2 be acyclic Subgraph of rng F;
let H1 be inducedSubgraph of G1,F_V"the_Vertices_of H2,F_E"the_Edges_of H2;
assume H1 is non acyclic;
then consider W1 being Walk of H1 such that
A1: W1 is Cycle-like by GLIB_002:def 2;
reconsider W = W1 as F-defined Walk of G1 by Th106;
W is Cycle-like by A1, GLIB_006:24;
then A2: F.:W is Cycle-like by GLIB_010:138;
reconsider W2 = F.:W as Walk of H2 by Th107;
W2 is Cycle-like by A2, GLIB_006:24;
hence contradiction by GLIB_002:def 2;
end;
theorem
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1, G2
for H2 being connected Subgraph of rng F
for H1 being inducedSubgraph of G1,F_V"the_Vertices_of H2,F_E"the_Edges_of H2
holds H1 is connected
proof
let G1, G2 be _Graph;
let F be non empty one-to-one PGraphMapping of G1, G2;
let H2 be connected Subgraph of rng F;
let H1 be inducedSubgraph of G1,F_V"the_Vertices_of H2,F_E"the_Edges_of H2;
now
let v1, w1 be Vertex of H1;
H2 is Subgraph of G2 by GLIB_000:43;
then A1: F_E"the_Edges_of H2 c= G1.edgesBetween(F_V"the_Vertices_of H2)
by Th99;
set v = the Vertex of H2;
v in the_Vertices_of H2;
then v in the_Vertices_of rng F;
then v in rng F_V by GLIB_010:54;
then consider x being object such that
A2: x in dom F_V & F_V.x = v by FUNCT_1:def 3;
x in F_V"the_Vertices_of H2 by A2, FUNCT_1:def 7;
then the_Vertices_of H1 = F_V"the_Vertices_of H2 &
the_Edges_of H1 = F_E"the_Edges_of H2 by A1, GLIB_000:def 37;
then A3: v1 in dom F_V & F_V.v1 in the_Vertices_of H2 &
w1 in dom F_V & F_V.w1 in the_Vertices_of H2 by FUNCT_1:def 7;
then consider W2 being Walk of H2 such that
A4: W2 is_Walk_from F_V.v1, F_V.w1 by GLIB_002:def 1;
reconsider W3 = W2 as F-valued Walk of G2 by Th108;
reconsider W1 = F"W3 as Walk of H1 by Th109;
take W1;
W3 is_Walk_from F_V.v1, F_V.w1 by A4, GLIB_001:19;
then F"W3 is_Walk_from F"_V.(F_V.v1), F"_V.(F_V.w1) by Th97;
then W1 is_Walk_from F"_V.(F_V.v1), F"_V.(F_V.w1) by GLIB_001:19;
then W1 is_Walk_from v1, F_V".(F_V.w1) by A3, FUNCT_1:34;
hence W1 is_Walk_from v1,w1 by A3, FUNCT_1:34;
end;
hence thesis by GLIB_002:def 1;
end;
:: To see why F_E being one-to-one is necessary for (D)continuity
:: consider the surjective mapping from K_4 to K_2. It is (D)continuous,
:: but if you take H = 2K_2, then the induced map isn't (D)continuous anymore
:: (but it still is semi-(D)continuous).
theorem Th112:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for H being Subgraph of G1
for F9 being PGraphMapping of H, rng(F | H) st F9 = F | H holds
(F9 is non empty implies F9 is onto) &
(F is total implies F9 is total) &
(F is one-to-one implies F9 is one-to-one) &
(F is directed implies F9 is directed) &
(F is semi-continuous implies F9 is semi-continuous) &
(F is continuous & F_E is one-to-one implies F9 is continuous) &
(F is semi-Dcontinuous implies F9 is semi-Dcontinuous) &
(F is Dcontinuous & F_E is one-to-one implies F9 is Dcontinuous)
proof
let G1, G2 be _Graph;
let F be PGraphMapping of G1, G2, H being Subgraph of G1;
let F9 be PGraphMapping of H, rng(F | H);
assume A1: F9 = F | H;
then A2: F9 = (rng(F | H)) |` (F | H) by Th86;
:: onto
hereby
assume F9 is non empty;
then F|H is non empty by A1;
then rng F9_V = the_Vertices_of rng(F|H) &
rng F9_E = the_Edges_of rng(F|H) by A1, GLIB_010:54;
hence F9 is onto by GLIB_010:def 12;
end;
:: total
hereby
assume F is total;
then F | H is total by GLIB_010:57;
hence F9 is total by A2, Th87;
end;
:: one-to-one
thus F is one-to-one implies F9 is one-to-one by A2;
:: directed
hereby
assume A3: F is directed;
now
let e,v,w be object;
assume A4: e in dom F9_E & v in dom F9_V & w in dom F9_V;
then A5: F9_E.e = F_E.e & F9_V.v = F_V.v & F9_V.w = F_V.w
by A1, FUNCT_1:47;
A6: v is set & w is set & e is set by TARSKI:1;
dom F9_V = dom F_V /\ the_Vertices_of H &
dom F9_E = dom F_E /\ the_Edges_of H by A1, GLIB_010:59;
then A7: e in dom F_E & v in dom F_V & w in dom F_V
by A4, XBOOLE_0:def 4;
assume e DJoins v,w,H;
then e DJoins v,w,G1 by A6, GLIB_000:72;
then A8: F9_E.e DJoins F9_V.v,F9_V.w,G2 by A3, A5, A7, GLIB_010:def 14;
F9_E.e in the_Edges_of rng(F | H)
proof
F9_E.e in rng F9_E by A4, FUNCT_1:3;
hence thesis;
end;
hence F9_E.e DJoins F9_V.v, F9_V.w, rng(F | H) by A8, GLIB_000:73;
end;
hence F9 is directed by GLIB_010:def 14;
end;
:: semi-continuous
hereby
assume A9: F is semi-continuous;
now
let e,v,w be object;
assume A10: e in dom F9_E & v in dom F9_V & w in dom F9_V;
then A11: F9_E.e = F_E.e & F9_V.v = F_V.v & F9_V.w = F_V.w
by A1, FUNCT_1:47;
assume F9_E.e Joins F9_V.v, F9_V.w, rng(F|H);
then A12: F_E.e Joins F_V.v, F_V.w, G2 by A11, GLIB_000:72;
dom F9_V = dom F_V /\ the_Vertices_of H &
dom F9_E = dom F_E /\ the_Edges_of H by A1, GLIB_010:59;
then e in dom F_E & v in dom F_V & w in dom F_V by A10, XBOOLE_0:def 4;
then e Joins v,w,G1 by A9, A12, GLIB_010:def 15;
hence e Joins v,w,H by A10, GLIB_000:73;
end;
hence F9 is semi-continuous by GLIB_010:def 15;
end;
:: continuous
hereby
assume A13: F is continuous & F_E is one-to-one;
now
let e9,v,w be object;
assume A14: v in dom F9_V & w in dom F9_V;
then A15: F9_V.v = F_V.v & F9_V.w = F_V.w
by A1, FUNCT_1:47;
assume A16: e9 Joins F9_V.v, F9_V.w, rng(F|H);
then A17: e9 Joins F_V.v, F_V.w, G2 by A15, GLIB_000:72;
A18: dom F9_V = dom F_V /\ the_Vertices_of H &
dom F9_E = dom F_E /\ the_Edges_of H by A1, GLIB_010:59;
A19: F|H is non empty by A1, A14;
e9 in the_Edges_of rng(F|H) by A16, GLIB_000:def 13;
then e9 in rng (F|H)_E by A19, GLIB_010:54;
then consider e0 being object such that
A20: e0 in dom (F|H)_E & (F|H)_E.e0 = e9 by FUNCT_1:def 3;
v in dom F_V & w in dom F_V by A14, A18, XBOOLE_0:def 4;
then consider e being object such that
A21: e Joins v,w,G1 & e in dom F_E & F_E.e = e9
by A13, A17, GLIB_010:def 16;
take e;
A22: e0 in dom F_E & e0 in the_Edges_of H by A1, A18, A20
, XBOOLE_0:def 4;
F_E.e = F_E.e0 by A20, A21, FUNCT_1:49;
then A23: e = e0 by A13, A21, A22, FUNCT_1:def 4;
e0 is set & v is set & w is set by TARSKI:1;
hence e Joins v,w,H by A21, A22, A23, GLIB_000:73;
thus e in dom F9_E & F9_E.e = e9 by A1, A20, A23;
end;
hence F9 is continuous by GLIB_010:def 16;
end;
:: semi-Dcontinuous
hereby
assume A24: F is semi-Dcontinuous;
now
let e,v,w be object;
assume A25: e in dom F9_E & v in dom F9_V & w in dom F9_V;
then A26: F9_E.e = F_E.e & F9_V.v = F_V.v & F9_V.w = F_V.w
by A1, FUNCT_1:47;
assume F9_E.e DJoins F9_V.v, F9_V.w, rng(F|H);
then A27: F_E.e DJoins F_V.v, F_V.w, G2 by A26, GLIB_000:72;
dom F9_V = dom F_V /\ the_Vertices_of H &
dom F9_E = dom F_E /\ the_Edges_of H by A1, GLIB_010:59;
then e in dom F_E & v in dom F_V & w in dom F_V by A25, XBOOLE_0:def 4;
then e DJoins v,w,G1 by A24, A27, GLIB_010:def 17;
hence e DJoins v,w,H by A25, GLIB_000:73;
end;
hence F9 is semi-Dcontinuous by GLIB_010:def 17;
end;
:: Dcontinuous
hereby
assume A28: F is Dcontinuous & F_E is one-to-one;
now
let e9,v,w be object;
assume A29: v in dom F9_V & w in dom F9_V;
then A30: F9_V.v = F_V.v & F9_V.w = F_V.w
by A1, FUNCT_1:47;
assume A31: e9 DJoins F9_V.v, F9_V.w, rng(F|H);
then A32: e9 DJoins F_V.v, F_V.w, G2 by A30, GLIB_000:72;
A33: dom F9_V = dom F_V /\ the_Vertices_of H &
dom F9_E = dom F_E /\ the_Edges_of H by A1, GLIB_010:59;
A34: F|H is non empty by A1, A29;
e9 in the_Edges_of rng(F|H) by A31, GLIB_000:def 14;
then e9 in rng (F|H)_E by A34, GLIB_010:54;
then consider e0 being object such that
A35: e0 in dom (F|H)_E & (F|H)_E.e0 = e9 by FUNCT_1:def 3;
v in dom F_V & w in dom F_V by A29, A33, XBOOLE_0:def 4;
then consider e being object such that
A36: e DJoins v,w,G1 & e in dom F_E & F_E.e = e9
by A28, A32, GLIB_010:def 18;
take e;
A37: e0 in dom F_E & e0 in the_Edges_of H by A1, A33, A35
, XBOOLE_0:def 4;
F_E.e = F_E.e0 by A35, A36, FUNCT_1:49;
then A38: e = e0 by A28, A36, A37, FUNCT_1:def 4;
e0 is set & v is set & w is set by TARSKI:1;
hence e DJoins v,w,H by A36, A37, A38, GLIB_000:73;
thus e in dom F9_E & F9_E.e = e9 by A1, A35, A38;
end;
hence F9 is Dcontinuous by GLIB_010:def 18;
end;
end;
theorem
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for H being Subgraph of G1
for F9 being PGraphMapping of H, rng(F | H) st F9 = F | H holds
(F is weak_SG-embedding implies F9 is weak_SG-embedding) &
(F is strong_SG-embedding implies F9 is isomorphism) &
(F is directed strong_SG-embedding implies F9 is Disomorphism)
proof
let G1, G2 be _Graph;
let F be PGraphMapping of G1, G2, H being Subgraph of G1;
let F9 be PGraphMapping of H, rng(F | H);
assume A1: F9 = F | H;
hereby
assume F is weak_SG-embedding;
then F9 is total one-to-one by A1, Th112;
hence F9 is weak_SG-embedding;
end;
hereby
assume A2: F is strong_SG-embedding;
then F9 is total by A1, Th112;
then F9 is total one-to-one continuous onto by A1, A2, Th112;
hence F9 is isomorphism;
end;
hereby
assume A3: F is directed strong_SG-embedding;
then F9 is total by A1, Th112;
then F9 is directed total one-to-one continuous onto by A1, A3, Th112;
hence F9 is Disomorphism;
end;
end;
begin :: into GLIB_013
:: or into GLIB_012 (vertex-finite can be replaced by _finite)
theorem
for G1 being vertex-finite Dsimple _Graph, G2 being DGraphComplement of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 holds
v2.inDegree() = G1.order() - (v1.inDegree()+1) &
v2.outDegree() = G1.order() - (v1.outDegree()+1) &
v2.degree() = 2*G1.order() - (v1.degree()+2)
proof
let G1 be vertex-finite Dsimple _Graph, G2 be DGraphComplement of G1;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2;
v1.inNeighbors() c= the_Vertices_of G1;
then v1.inNeighbors() c= the_Vertices_of G2 by GLIB_012:80;
then A2: v1.inNeighbors() \/ {v2} c= the_Vertices_of G2 by XBOOLE_1:8;
v1.outNeighbors() c= the_Vertices_of G1;
then v1.outNeighbors() c= the_Vertices_of G2 by GLIB_012:80;
then A3: v1.outNeighbors() \/ {v2} c= the_Vertices_of G2 by XBOOLE_1:8;
not v1 in v1.allNeighbors() by GLIB_000:112;
then A4: not v2 in v1.inNeighbors() & not v2 in v1.outNeighbors()
by A1, XBOOLE_0:def 3;
thus A5: v2.inDegree() = card v2.inNeighbors() by GLIB_000:109
.= card (the_Vertices_of G2 \ (v1.inNeighbors()\/{v2})) by A1, GLIB_012:95
.= G2.order() - card (v1.inNeighbors()\/{v2}) by A2, CARD_2:44
.= G2.order() - (card v1.inNeighbors() + 1) by A4, CARD_2:41
.= G1.order() - (card v1.inNeighbors() + 1) by GLIB_012:80
.= G1.order() - (v1.inDegree()+1) by GLIB_000:109;
thus v2.outDegree() = card v2.outNeighbors() by GLIB_000:110
.= card (the_Vertices_of G2 \ (v1.outNeighbors()\/{v2})) by A1, GLIB_012:95
.= G2.order() - card (v1.outNeighbors()\/{v2}) by A3, CARD_2:44
.= G2.order() - (card v1.outNeighbors() + 1) by A4, CARD_2:41
.= G1.order() - (card v1.outNeighbors() + 1) by GLIB_012:80
.= G1.order() - (v1.outDegree()+1) by GLIB_000:110;
hence v2.degree() = 2*G1.order() - (v1.degree()+2) by A5;
end;
:: or into GLIB_012 (vertex-finite can be replaced by _finite)
theorem
for G1 being vertex-finite simple _Graph, G2 being GraphComplement of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds v2.degree() = G1.order() - (v1.degree()+1)
proof
let G1 be vertex-finite simple _Graph, G2 be GraphComplement of G1;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2;
v1.allNeighbors() c= the_Vertices_of G1;
then v1.allNeighbors() c= the_Vertices_of G2 by GLIB_012:98;
then A2: v1.allNeighbors() \/ {v2} c= the_Vertices_of G2 by XBOOLE_1:8;
A3: not v2 in v1.allNeighbors() by A1, GLIB_000:112;
thus v2.degree() = card v2.allNeighbors() by GLIB_000:111
.= card (the_Vertices_of G2 \(v1.allNeighbors()\/{v2})) by A1, GLIB_012:118
.= G2.order() - card (v1.allNeighbors()\/{v2}) by A2, CARD_2:44
.= G2.order() - (card v1.allNeighbors() + 1) by A3, CARD_2:41
.= G1.order() - (card v1.allNeighbors() + 1) by GLIB_012:98
.= G1.order() - (v1.degree()+1) by GLIB_000:111;
end;
theorem
for G being vertex-finite Dsimple _Graph, v being Vertex of G
holds v.inDegree() < G.order() & v.outDegree() < G.order()
proof
let G be vertex-finite Dsimple _Graph, v being Vertex of G;
A1: G.order()-1 is Nat by CHORD:1;
not v in v.allNeighbors() by GLIB_000:112;
then A2: not v in v.inNeighbors() & not v in v.outNeighbors()
by XBOOLE_0:def 3;
A3: v.inNeighbors() c= the_Vertices_of G \ {v} &
v.outNeighbors() c= the_Vertices_of G \ {v} by A2, ZFMISC_1:34;
then card v.inNeighbors() <= card(the_Vertices_of G \ {v}) by NAT_1:43;
then v.inDegree() <= card(the_Vertices_of G \ {v}) by GLIB_000:109;
then v.inDegree() <= G.order() - card {v} by CARD_2:44;
then v.inDegree() <= G.order() - 1 by CARD_1:30;
then v.inDegree() < G.order() - 1 + 1 by A1, NAT_1:13;
hence v.inDegree() < G.order();
card v.outNeighbors() <= card(the_Vertices_of G \ {v}) by A3, NAT_1:43;
then v.outDegree() <= card(the_Vertices_of G \ {v}) by GLIB_000:110;
then v.outDegree() <= G.order() - card {v} by CARD_2:44;
then v.outDegree() <= G.order() - 1 by CARD_1:30;
then v.outDegree() < G.order() - 1 + 1 by A1, NAT_1:13;
hence v.outDegree() < G.order();
end;
theorem
for G being vertex-finite simple _Graph, v being Vertex of G
holds v.degree() < G.order()
proof
let G be vertex-finite simple _Graph, v be Vertex of G;
A1: G.order()-1 is Nat by CHORD:1;
not v in v.allNeighbors() by GLIB_000:112;
then card v.allNeighbors() <= card(the_Vertices_of G \ {v})
by NAT_1:43, ZFMISC_1:34;
then v.degree() <= card(the_Vertices_of G \ {v}) by GLIB_000:111;
then v.degree() <= G.order() - card {v} by CARD_2:44;
then v.degree() <= G.order() - 1 by CARD_1:30;
then v.degree() < G.order() - 1 + 1 by A1, NAT_1:13;
hence v.degree() < G.order();
end;
registration
cluster 1-edge -> non-multi for _Graph;
coherence
proof
let G be _Graph;
assume G is 1-edge;
then G.size() = 1 by GLIB_013:def 4;
then consider e being object such that
A1: the_Edges_of G = {e} by CARD_2:42;
now
let e1,e2,v1,v2 be object;
assume e1 Joins v1,v2,G & e2 Joins v1,v2,G;
then e1 in the_Edges_of G & e2 in the_Edges_of G by GLIB_000:def 13;
then e1 = e & e2 = e by A1, TARSKI:def 1;
hence e1 = e2;
end;
hence thesis by GLIB_000:def 20;
end;
end;
begin :: into GLIB_014
registration
let S be \/-tolerating Graph-membered set;
cluster -> \/-tolerating for Subset of S;
coherence
proof
let T be Subset of S;
for G1, G2 being _Graph st G1 in T & G2 in T holds G1 tolerates G2
by GLIB_014:def 23;
hence thesis by GLIB_014:def 23;
end;
end;
theorem
for S1, S2 being Graph-membered set st S1 c= S2 holds
the_Vertices_of S1 c= the_Vertices_of S2 &
the_Edges_of S1 c= the_Edges_of S2 &
the_Source_of S1 c= the_Source_of S2 &
the_Target_of S1 c= the_Target_of S2
proof
let S1, S2 be Graph-membered set;
assume A1: S1 c= S2;
now
let x be object;
assume x in the_Vertices_of S1;
then consider G being _Graph such that
A2: G in S1 & x = the_Vertices_of G by GLIB_014:def 14;
thus x in the_Vertices_of S2 by A1, A2, GLIB_014:def 14;
end;
hence the_Vertices_of S1 c= the_Vertices_of S2 by TARSKI:def 3;
now
let x be object;
assume x in the_Edges_of S1;
then consider G being _Graph such that
A3: G in S1 & x = the_Edges_of G by GLIB_014:def 15;
thus x in the_Edges_of S2 by A1, A3, GLIB_014:def 15;
end;
hence the_Edges_of S1 c= the_Edges_of S2 by TARSKI:def 3;
now
let x be object;
assume x in the_Source_of S1;
then consider G being _Graph such that
A4: G in S1 & x = the_Source_of G by GLIB_014:def 16;
thus x in the_Source_of S2 by A1, A4, GLIB_014:def 16;
end;
hence the_Source_of S1 c= the_Source_of S2 by TARSKI:def 3;
now
let x be object;
assume x in the_Target_of S1;
then consider G being _Graph such that
A5: G in S1 & x = the_Target_of G by GLIB_014:def 17;
thus x in the_Target_of S2 by A1, A5, GLIB_014:def 17;
end;
hence the_Target_of S1 c= the_Target_of S2 by TARSKI:def 3;
thus thesis;
end;
theorem Th119:
for S being GraphUnionSet, G being GraphUnion of S
for e,v,w being object st e DJoins v,w,G
ex H being Element of S st e DJoins v,w,H
proof
let S be GraphUnionSet, G be GraphUnion of S;
let e,v,w be object;
assume e DJoins v,w,G;
then A1: e in the_Edges_of G & (the_Source_of G).e = v &
(the_Target_of G).e = w by GLIB_000:def 14;
e in union the_Edges_of S by A1, GLIB_014:def 25;
then consider E being set such that
A2: e in E & E in the_Edges_of S by TARSKI:def 4;
consider H being _Graph such that
A3: H in S & E = the_Edges_of H by A2, GLIB_014:def 15;
reconsider H as Element of S by A3;
take H;
A4: e in dom the_Source_of H & e in dom the_Target_of H
by A2, A3, FUNCT_2:def 1;
the_Source_of H in the_Source_of S by GLIB_014:def 16;
then A5: (the_Source_of H).e = (union the_Source_of S).e by A4, COMPUT_1:13
.= v by A1, GLIB_014:def 25;
the_Target_of H in the_Target_of S by GLIB_014:def 17;
then (the_Target_of H).e = (union the_Target_of S).e by A4, COMPUT_1:13
.= w by A1, GLIB_014:def 25;
hence e DJoins v,w,H by A2, A3, A5, GLIB_000:def 14;
end;
theorem
for S being GraphUnionSet, G being GraphUnion of S
for e,v,w being object st e Joins v,w,G
ex H being Element of S st e Joins v,w,H
proof
let S be GraphUnionSet, G be GraphUnion of S;
let e,v,w be object;
assume e Joins v,w,G;
then per cases by GLIB_000:16;
suppose e DJoins v,w,G;
then consider H being Element of S such that
A1: e DJoins v,w,H by Th119;
take H;
thus thesis by A1, GLIB_000:16;
end;
suppose e DJoins w,v,G;
then consider H being Element of S such that
A2: e DJoins w,v,H by Th119;
take H;
thus thesis by A2, GLIB_000:16;
end;
end;
theorem Th121:
for S1, S2 being GraphUnionSet
for G1 being (GraphUnion of S1), G2 being GraphUnion of S2
st (for H2 being Element of S2 ex H1 being Element of S1
st H2 is Subgraph of H1)
holds G2 is Subgraph of G1
proof
let S1, S2 be GraphUnionSet;
let G1 be (GraphUnion of S1), G2 be GraphUnion of S2;
assume A1: for H2 being Element of S2 ex H1 being Element of S1
st H2 is Subgraph of H1;
now
now
let x be object;
assume x in the_Vertices_of G2;
then x in union the_Vertices_of S2 by GLIB_014:def 25;
then consider V being set such that
A2: x in V & V in the_Vertices_of S2 by TARSKI:def 4;
consider H2 being _Graph such that
A3: H2 in S2 & V = the_Vertices_of H2 by A2, GLIB_014:def 14;
consider H1 being Element of S1 such that
A4: H2 is Subgraph of H1 by A1, A3;
the_Vertices_of H2 c= the_Vertices_of H1 by A4, GLIB_000:def 32;
then A5: x in the_Vertices_of H1 by A2, A3;
the_Vertices_of H1 in the_Vertices_of S1 by GLIB_014:def 14;
then x in union the_Vertices_of S1 by A5, TARSKI:def 4;
hence x in the_Vertices_of G1 by GLIB_014:def 25;
end;
hence the_Vertices_of G2 c= the_Vertices_of G1 by TARSKI:def 3;
now
let x be object;
assume x in the_Edges_of G2;
then x in union the_Edges_of S2 by GLIB_014:def 25;
then consider E being set such that
A6: x in E & E in the_Edges_of S2 by TARSKI:def 4;
consider H2 being _Graph such that
A7: H2 in S2 & E = the_Edges_of H2 by A6, GLIB_014:def 15;
consider H1 being Element of S1 such that
A8: H2 is Subgraph of H1 by A1, A7;
the_Edges_of H2 c= the_Edges_of H1 by A8, GLIB_000:def 32;
then A9: x in the_Edges_of H1 by A6, A7;
the_Edges_of H1 in the_Edges_of S1 by GLIB_014:def 15;
then x in union the_Edges_of S1 by A9, TARSKI:def 4;
hence x in the_Edges_of G1 by GLIB_014:def 25;
end;
hence the_Edges_of G2 c= the_Edges_of G1 by TARSKI:def 3;
let e be set;
set v = (the_Source_of G2).e, w = (the_Target_of G2).e;
assume e in the_Edges_of G2;
then consider H2 being Element of S2 such that
A10: e DJoins v,w,H2 by Th119, GLIB_000:def 14;
consider H1 being Element of S1 such that
A11: H2 is Subgraph of H1 by A1;
H1 is Subgraph of G1 by GLIB_014:21;
then H2 is Subgraph of G1 by A11, GLIB_000:43;
then e DJoins v,w,G1 by A10, GLIB_000:72;
hence (the_Source_of G2).e = (the_Source_of G1).e &
(the_Target_of G2).e = (the_Target_of G1).e by GLIB_000:def 14;
end;
hence thesis by GLIB_000:def 32;
end;
theorem
for S1, S2 being GraphUnionSet
for G1 being (GraphUnion of S1), G2 being GraphUnion of S2
st S2 c= S1 holds G2 is Subgraph of G1
proof
let S1, S2 be GraphUnionSet;
let G1 be (GraphUnion of S1), G2 be GraphUnion of S2;
assume A1: S2 c= S1;
now
let H2 be Element of S2;
reconsider H1 = H2 as Element of S1 by A1, TARSKI:def 3;
take H1;
thus H2 is Subgraph of H1 by GLIB_000:40;
end;
hence thesis by Th121;
end;
theorem
for G1, G2 being _Graph, G being GraphUnion of G1, G2
st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2
holds G.order() = G1.order() +` G2.order()
proof
let G1, G2 be _Graph, G be GraphUnion of G1, G2;
assume A1: G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2;
then A2: the_Vertices_of G = the_Vertices_of G1 \/ the_Vertices_of G2
by GLIB_014:25;
thus G.order() = G1.order() +` G2.order() by A1, A2, CARD_2:35;
end;
theorem
for G1, G2 being _Graph, G being GraphUnion of G1, G2
st G1 tolerates G2 & the_Edges_of G1 misses the_Edges_of G2
holds G.size() = G1.size() +` G2.size()
proof
let G1, G2 be _Graph, G be GraphUnion of G1, G2;
assume A1: G1 tolerates G2 & the_Edges_of G1 misses the_Edges_of G2;
then A2: the_Edges_of G = the_Edges_of G1 \/ the_Edges_of G2 by GLIB_014:25;
thus G.size() = G1.size() +` G2.size() by A1, A2, CARD_2:35;
end;
theorem
for G1, G2 being connected _Graph, G being GraphUnion of G1, G2
st the_Vertices_of G1 meets the_Vertices_of G2 holds G is connected
proof
let G1, G2 be connected _Graph, G be GraphUnion of G1, G2;
per cases;
suppose A1: G1 tolerates G2;
then A2: G is Supergraph of G2 by GLIB_014:26;
assume the_Vertices_of G1 meets the_Vertices_of G2;
then consider u being object such that
A3: u in the_Vertices_of G1 & u in the_Vertices_of G2 by XBOOLE_0:3;
now
let v,w be Vertex of G;
the_Vertices_of G = the_Vertices_of G1 \/ the_Vertices_of G2
by A1, GLIB_014:25;
then per cases by XBOOLE_0:def 3;
suppose v in the_Vertices_of G1 & w in the_Vertices_of G1;
then consider W being Walk of G1 such that
A4: W is_Walk_from v,w by GLIB_002:def 1;
reconsider W as Walk of G by GLIB_006:75;
take W;
thus W is_Walk_from v,w by A4, GLIB_001:19;
end;
suppose A5: v in the_Vertices_of G1 & w in the_Vertices_of G2;
then consider W1 being Walk of G1 such that
A6: W1 is_Walk_from v, u by A3, GLIB_002:def 1;
reconsider W1 as Walk of G by GLIB_006:75;
consider W2 being Walk of G2 such that
A7: W2 is_Walk_from u, w by A3, A5, GLIB_002:def 1;
reconsider W2 as Walk of G by A2, GLIB_006:75;
reconsider W = W1.append(W2) as Walk of G;
take W;
W1 is_Walk_from v,u & W2 is_Walk_from u,w by A6, A7, GLIB_001:19;
hence W is_Walk_from v, w by GLIB_001:31;
end;
suppose A8: v in the_Vertices_of G2 & w in the_Vertices_of G1;
then consider W1 being Walk of G2 such that
A9: W1 is_Walk_from v, u by A3, GLIB_002:def 1;
reconsider W1 as Walk of G by A2, GLIB_006:75;
consider W2 being Walk of G1 such that
A10: W2 is_Walk_from u, w by A3, A8, GLIB_002:def 1;
reconsider W2 as Walk of G by GLIB_006:75;
reconsider W = W1.append(W2) as Walk of G;
take W;
W1 is_Walk_from v,u & W2 is_Walk_from u,w by A9, A10, GLIB_001:19;
hence W is_Walk_from v, w by GLIB_001:31;
end;
suppose v in the_Vertices_of G2 & w in the_Vertices_of G2;
then consider W being Walk of G2 such that
A11: W is_Walk_from v,w by GLIB_002:def 1;
reconsider W as Walk of G by A2, GLIB_006:75;
take W;
thus W is_Walk_from v,w by A11, GLIB_001:19;
end;
end;
hence thesis by GLIB_002:def 1;
end;
suppose not G1 tolerates G2;
then G1 == G by GLIB_014:def 26;
hence thesis by GLIB_002:8;
end;
end;
Lm4:
for G1, G2 being _Graph, G being GraphUnion of G1, G2
st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2
holds for W being Walk of G holds W is Walk of G1 or W is Walk of G2
proof
let G1, G2 be _Graph, G be GraphUnion of G1, G2;
assume A1: G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2;
then A2: G is Supergraph of G2 by GLIB_014:26;
then A3: G1 is Subgraph of G & G2 is Subgraph of G by GLIB_006:57;
A4: the_Vertices_of G = the_Vertices_of G1 \/ the_Vertices_of G2
by A1, GLIB_014:25;
A5: the_Edges_of G = the_Edges_of G1 \/ the_Edges_of G2 by A1, GLIB_014:25;
defpred P[Walk of G] means $1 is Walk of G1 or $1 is Walk of G2;
A6: for W being trivial Walk of G holds P[W]
proof
let W be trivial Walk of G;
consider v being Vertex of G such that
A7: W = G.walkOf(v) by GLIB_001:128;
per cases by A4, XBOOLE_0:def 3;
suppose v in the_Vertices_of G1;
then W.first() in the_Vertices_of G1 by A7;
hence thesis by A3, GLIB_001:168;
end;
suppose v in the_Vertices_of G2;
then W.first() in the_Vertices_of G2 by A7;
hence thesis by A3, GLIB_001:168;
end;
end;
A8: for W being Walk of G, e being object
st e in W.last().edgesInOut() & P[W] holds P[W.addEdge(e)]
proof
let W be Walk of G, e be object;
assume e in W.last().edgesInOut();
then consider w being Vertex of G such that
A9: e Joins W.last(),w,G by GLIB_000:64;
assume P[W];
then per cases;
suppose W is Walk of G1;
then reconsider W1 = W as Walk of G1;
e in the_Edges_of G1
proof
assume A10: not e in the_Edges_of G1;
e in the_Edges_of G by A9, GLIB_000:def 13;
then e in the_Edges_of G2 by A5, A10, XBOOLE_0:def 3;
then e Joins W.last(),w,G2 by A2, A9, GLIB_006:72;
then W.last() in the_Vertices_of G2 by GLIB_000:13;
then W1.last() in the_Vertices_of G2;
hence contradiction by A1, XBOOLE_0:3;
end;
then e Joins W.last(),w,G1 by A9, GLIB_006:72;
then e Joins W1.last(),w,G1;
then e in W1.last().edgesInOut() by GLIB_000:62;
then W1.addEdge(e) = W.addEdge(e) by A3, GLIB_001:174;
hence thesis;
end;
suppose W is Walk of G2;
then reconsider W2 = W as Walk of G2;
e in the_Edges_of G2
proof
assume A11: not e in the_Edges_of G2;
e in the_Edges_of G by A9, GLIB_000:def 13;
then e in the_Edges_of G1 by A5, A11, XBOOLE_0:def 3;
then e Joins W.last(),w,G1 by A9, GLIB_006:72;
then W.last() in the_Vertices_of G1 by GLIB_000:13;
then W2.last() in the_Vertices_of G1;
hence contradiction by A1, XBOOLE_0:3;
end;
then e Joins W.last(),w,G2 by A2, A9, GLIB_006:72;
then e Joins W2.last(),w,G2;
then e in W2.last().edgesInOut() by GLIB_000:62;
then W2.addEdge(e) = W.addEdge(e) by A3, GLIB_001:174;
hence thesis;
end;
end;
for W being Walk of G holds P[W] from GLIB_009:sch 1(A6, A8);
hence thesis;
end;
theorem Th126:
for G1, G2 being _Graph, G being GraphUnion of G1, G2, W being Walk of G
st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2
holds W is Walk of G1 or W is Walk of G2 by Lm4;
theorem Th127:
for G1, G2 being _Graph, G being GraphUnion of G1, G2
for v1 being Vertex of G1, v being Vertex of G
st the_Vertices_of G1 misses the_Vertices_of G2
holds v = v1 implies G.reachableFrom(v) = G1.reachableFrom(v1)
proof
let G1, G2 be _Graph, G be GraphUnion of G1, G2;
let v1 be Vertex of G1, v be Vertex of G;
per cases;
suppose A1: G1 tolerates G2;
assume A2: the_Vertices_of G1 misses the_Vertices_of G2 & v = v1;
G1 is Subgraph of G by GLIB_006:57;
then A3: G1.reachableFrom(v1) c= G.reachableFrom(v) by A2, GLIB_002:14;
now
let y be object;
assume y in G.reachableFrom(v);
then consider W being Walk of G such that
A4: W is_Walk_from v,y by GLIB_002:def 5;
now
assume W is Walk of G2;
then reconsider W2 = W as Walk of G2;
W.first() = v1 by A2, A4, GLIB_001:def 23;
then v1 in W.vertices() by GLIB_001:88;
then v1 in W2.vertices() by GLIB_001:98;
hence contradiction by A2, XBOOLE_0:3;
end;
then reconsider W1 = W as Walk of G1 by A1, A2, Th126;
W1 is_Walk_from v1,y by A2, A4, GLIB_001:19;
hence y in G1.reachableFrom(v1) by GLIB_002:def 5;
end;
then G.reachableFrom(v) c= G1.reachableFrom(v1) by TARSKI:def 3;
hence thesis by A3, XBOOLE_0:def 10;
end;
suppose not G1 tolerates G2;
then G1 == G by GLIB_014:def 26;
hence thesis by GLIB_002:17;
end;
end;
theorem Th128:
for G1, G2 being _Graph, G being GraphUnion of G1, G2
for v2 being Vertex of G2, v being Vertex of G
st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2
holds v = v2 implies G.reachableFrom(v) = G2.reachableFrom(v2)
proof
let G1, G2 be _Graph, G be GraphUnion of G1, G2;
let v2 be Vertex of G2, v be Vertex of G;
assume that A1: G1 tolerates G2 and
A2: the_Vertices_of G1 misses the_Vertices_of G2 & v = v2;
G is Supergraph of G2 by A1, GLIB_014:26;
then G2 is Subgraph of G by GLIB_006:57;
then A3: G2.reachableFrom(v2) c= G.reachableFrom(v) by A2, GLIB_002:14;
now
let y be object;
assume y in G.reachableFrom(v);
then consider W being Walk of G such that
A4: W is_Walk_from v,y by GLIB_002:def 5;
now
assume W is Walk of G1;
then reconsider W1 = W as Walk of G1;
W.first() = v2 by A2, A4, GLIB_001:def 23;
then v2 in W.vertices() by GLIB_001:88;
then v2 in W1.vertices() by GLIB_001:98;
hence contradiction by A2, XBOOLE_0:3;
end;
then reconsider W2 = W as Walk of G2 by A1, A2, Th126;
W2 is_Walk_from v2,y by A2, A4, GLIB_001:19;
hence y in G2.reachableFrom(v2) by GLIB_002:def 5;
end;
then G.reachableFrom(v) c= G2.reachableFrom(v2) by TARSKI:def 3;
hence thesis by A3, XBOOLE_0:def 10;
end;
:: this is probably somewhere in a more set-theoretic form
Lm5:
for G1, G2 being _Graph st the_Vertices_of G1 misses the_Vertices_of G2
holds G1.componentSet() misses G2.componentSet()
proof
let G1, G2 be _Graph;
assume A1: the_Vertices_of G1 misses the_Vertices_of G2;
assume G1.componentSet() meets G2.componentSet();
then consider x being object such that
A2: x in G1.componentSet() & x in G2.componentSet() by XBOOLE_0:3;
consider v1 being Vertex of G1 such that
A3: x = G1.reachableFrom(v1) by A2, GLIB_002:def 8;
consider v2 being Vertex of G2 such that
A4: x = G2.reachableFrom(v2) by A2, GLIB_002:def 8;
v1 in G2.reachableFrom(v2) by A3, A4, GLIB_002:9;
hence contradiction by A1, XBOOLE_0:3;
end;
theorem
for G1, G2 being _Graph, G being GraphUnion of G1, G2
st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2
holds G.componentSet() = G1.componentSet() \/ G2.componentSet() &
G.numComponents() = G1.numComponents() +` G2.numComponents()
proof
let G1, G2 be _Graph, G be GraphUnion of G1, G2;
assume A1: G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2;
then A2: the_Vertices_of G = the_Vertices_of G1 \/ the_Vertices_of G2 &
G is Supergraph of G2 by GLIB_014:25, GLIB_014:26;
now
let x be object;
hereby
assume x in G.componentSet();
then consider v being Vertex of G such that
A3: x = G.reachableFrom(v) by GLIB_002:def 8;
per cases by A2, XBOOLE_0:def 3;
suppose v in the_Vertices_of G1;
then reconsider v1 = v as Vertex of G1;
x = G1.reachableFrom(v1) by A1, A3, Th127;
hence x in G1.componentSet() or x in G2.componentSet()
by GLIB_002:def 8;
end;
suppose v in the_Vertices_of G2;
then reconsider v2 = v as Vertex of G2;
x = G2.reachableFrom(v2) by A1, A3, Th128;
hence x in G1.componentSet() or x in G2.componentSet()
by GLIB_002:def 8;
end;
end;
assume x in G1.componentSet() or x in G2.componentSet();
then per cases;
suppose x in G1.componentSet();
then consider v1 being Vertex of G1 such that
A4: x = G1.reachableFrom(v1) by GLIB_002:def 8;
reconsider v = v1 as Vertex of G by GLIB_006:68;
x = G.reachableFrom(v) by A1, A4, Th127;
hence x in G.componentSet() by GLIB_002:def 8;
end;
suppose x in G2.componentSet();
then consider v2 being Vertex of G2 such that
A5: x = G2.reachableFrom(v2) by GLIB_002:def 8;
reconsider v = v2 as Vertex of G by A2, GLIB_006:68;
x = G.reachableFrom(v) by A1, A5, Th128;
hence x in G.componentSet() by GLIB_002:def 8;
end;
end;
hence G.componentSet() = G1.componentSet() \/ G2.componentSet()
by XBOOLE_0:def 3;
hence G.numComponents()
= card(G1.componentSet() \/ G2.componentSet()) by GLIB_002:def 9
.= card G1.componentSet() +` card G2.componentSet() by A1, Lm5, CARD_2:35
.= card G1.componentSet() +` G2.numComponents() by GLIB_002:def 9
.= G1.numComponents() +` G2.numComponents() by GLIB_002:def 9;
end;
begin :: into GLUNIR00
theorem Th130:
for V being non empty set, E being Relation of V
holds createGraph(V,E).loops() = E /\ id V
proof
let V be non empty set, E be Relation of V;
set G = createGraph(V,E);
now
let x be object;
hereby
assume x in G.loops();
then consider v being object such that
A1: x DJoins v,v,G by GLIB_009:45;
x Joins v,v,G by A1, GLIB_000:16;
then v in the_Vertices_of G by GLIB_000:13;
then A2: v in V;
x = [v,v] by A1, GLUNIR00:64;
hence x in E & x in id V by A1, A2, GLUNIR00:63, RELAT_1:def 10;
end;
assume A3: x in E & x in id V;
then consider y,z being object such that
A4: x = [y,z] by RELAT_1:def 1;
x = [y,y] by A3, A4, RELAT_1:def 10;
hence x in G.loops() by A3, GLUNIR00:63, GLIB_009:45;
end;
hence thesis by XBOOLE_0:def 4;
end;
theorem
for V being non empty set, E being Relation of V
holds createGraph(V, E \ id V) is removeLoops of createGraph(V,E)
proof
let V be non empty set, E be Relation of V;
set G = createGraph(V,E), H = createGraph(V,E\id V);
V c= V;
then A1: H is inducedSubgraph of G,V,E\id V by XBOOLE_1:36, GLUNIR00:85;
the_Edges_of G \ G.loops() = E \ G.loops()
.= E \ (E /\ id V) by Th130
.= E \ id V by XBOOLE_1:47;
hence thesis by A1;
end;
:: added by SK, 8.12.2024
:: holds more generally for any T not being a 1-cycle instead of G loopless
theorem
for G being loopless _Graph, T being closed Trail of G
st T is non trivial holds
T.2 <> T.(len T - 1) & {T.2,T.(len T - 1)} c= T.first().edgesInOut() &
2 c= T.first().degree()
proof
let G be loopless _Graph, T be closed Trail of G;
assume T is non trivial;
then A1: 3 <= len T by GLIB_001:125;
then 1 < len T by XXREAL_0:2;
then T.(1+1) Joins T.1,T.(1+2),G by POLYFORM:4, GLIB_001:def 3;
then A2: T.2 Joins T.first(),T.3,G;
3-2 <= len T - 2 by A1, XREAL_1:9;
then reconsider m = len T - 2 as Element of NAT by INT_1:3;
m < len T - 0 & m is odd by XREAL_1:15, POLYFORM:5;
then T.(m+1) Joins T.m,T.(m+2),G by GLIB_001:def 3;
then T.(len T-1) Joins T.last(),T.m,G by GLIB_000:14;
then A4: T.(len T-1) Joins T.first(),T.m,G by GLIB_001:def 24;
thus A5: T.2 <> T.(len T - 1)
proof
assume A6: T.2 = T.(len T - 1);
A7: 3-1 <= len T - 1 by A1, XREAL_1:9;
then reconsider k = len T-1 as Element of NAT by INT_1:3;
k <= len T - 0 by XREAL_1:13;
then 2 >= k by A6, POLYFORM:5, GLIB_001:138;
then len T - 1 + 1 = 2+1 by A7, XXREAL_0:1;
then consider e being object such that
A9: e Joins T.first(),T.last(),G and
T = G.walkOf(T.first(),e,T.last()) by Th28;
e Joins T.first(),T.first(),G by A9, GLIB_001:def 24;
hence contradiction by GLIB_000:18;
end;
set v = T.first();
T.2 in v.edgesInOut() & T.(len T - 1) in v.edgesInOut()
by A2, A4, GLIB_000:62;
hence {T.2,T.(len T - 1)} c= v.edgesInOut() by ZFMISC_1:32;
then card{T.2,T.(len T - 1)} c= card(v.edgesInOut()) by CARD_1:11;
then A10: 2 c= card(v.edgesInOut()) by A5, CARD_2:57;
card(v.edgesInOut()) c= v.inDegree() +` v.outDegree() by CARD_2:34;
hence 2 c= v.degree() by A10, XBOOLE_1:1;
end;
theorem
for G being _Graph, C being Walk of G, u,v,w being object
st C is Cycle-like & u in C.vertices() & v in C.vertices() & u <> w & v <> w
ex W being Path of G st W is_Walk_from u,v & not w in W.vertices()
proof
let G be _Graph, C be Walk of G, u,v,w be object;
assume that A1: C is Cycle-like & u in C.vertices() & v in C.vertices() and
A2: u <> w & v <> w;
consider n being odd Element of NAT such that
A3: n <= len C & C.n = u by A1, GLIB_001:87;
consider m being odd Element of NAT such that
A4: m <= len C & C.m = v by A1, GLIB_001:87;
per cases by A3, A4, XXREAL_0:1;
suppose A5: u = v;
reconsider u9 = u as Vertex of G by A1;
reconsider W = G.walkOf(u9) as Path of G;
take W;
thus W is_Walk_from u,v by A5, GLIB_001:13;
W.vertices() = {u} by GLIB_001:90;
hence thesis by A2, TARSKI:def 1;
end;
suppose A6: u <> v & n < m;
per cases;
suppose A7: not w in C.cut(n,m).vertices();
reconsider W = C.cut(n,m) as Path of G by A1;
take W;
thus thesis by A3, A4, A6, A7, GLIB_001:37;
end;
suppose w in C.cut(n,m).vertices();
then consider k being odd Element of NAT such that
A8: k <= len C.cut(n,m) & C.cut(n,m).k = w by GLIB_001:87;
reconsider k3=k-1 as even Nat by CHORD:2;
reconsider k3 as Element of NAT by ORDINAL1:def 12;
k < len C.cut(n,m) + 1 by A8, NAT_1:13;
then A9: k3 < len C.cut(n,m) + 1 - 1 by XREAL_1:14;
A10: C.cut(n,m).(k3+1) = C.(n+k3) by A4, A6, A9, GLIB_001:36;
reconsider W1 = C.cut(1,n), W2 = C.cut(m,len C) as Path of G by A1;
A11: 1 is odd & len C is odd by POLYFORM:4;
A12: 1 <= n by CHORD:2;
len C.cut(n,m) + n = m + 1 by A4, A6, GLIB_001:36;
then A13: n+k3 < m + 1 by A9, XREAL_1:8;
A14: w in W1.vertices() implies n+k3 = len C
proof
assume w in W1.vertices();
then consider k2 being odd Element of NAT such that
A15: k2 <= len W1 & W1.k2 = w by GLIB_001:87;
reconsider k4=k2-1 as Nat by CHORD:2;
reconsider k4 as Element of NAT by ORDINAL1:def 12;
k2 < len W1 + 1 by A15, NAT_1:13;
then k4 < len W1 + 1 - 1 by XREAL_1:14;
then A16: W1.(k4+1) = C.(1+k4) by A3, A11, A12, GLIB_001:36;
then A17: C.(n+k3) = C.(1+k4) by A8, A10, A15;
len W1 + 1 = n + 1 by A3, A11, A12, GLIB_001:36;
then 1+k4 <= n by A15;
then 1+k4 < n by A2, A3, A15, A16, XXREAL_0:1;
then A19: 1+k4+0 < n+k3 by XREAL_1:8;
n+k3 <= m by A13, NAT_1:13;
then n+k3 <= len C by A4, XXREAL_0:2;
hence n+k3 = len C by A1, A17, A19, GLIB_001:def 28;
end;
A20: w in W2.vertices() implies n+k3 = 1
proof
assume w in W2.vertices();
then consider k2 being odd Element of NAT such that
A21: k2 <= len W2 & W2.k2 = w by GLIB_001:87;
reconsider k4=k2-1 as Nat by CHORD:2;
reconsider k4 as Element of NAT by ORDINAL1:def 12;
k2 < len W2 + 1 by A21, NAT_1:13;
then A22: k4 < len W2 + 1 - 1 by XREAL_1:14;
then A23: W2.(k4+1) = C.(m+k4) by A4, GLIB_001:36;
then A24: C.(n+k3) = C.(m+k4) by A8, A10, A21;
1 < k4
proof
assume k4 <= 1;
then k4 = 0 by A11, NAT_1:25;
hence contradiction by A2, A4, A21, A23;
end;
then m+1 < m+k4 by XREAL_1:8;
then A25: n+k3 < m+k4 by A13, XXREAL_0:2;
m+k4 < len W2 + m by A22, XREAL_1:8;
then m+k4 < len C + 1 by A4, GLIB_001:36;
then m+k4 <= len C by NAT_1:13;
hence n+k3 = 1 by A1, A24, A25, GLIB_001:def 28;
end;
per cases;
suppose n <> 1 & m <> len C;
then A26: 1 < n & m < len C by A4, A12, XXREAL_0:1;
then A27: m <> 1 by A6;
A28: W2.last() = C.last() by A4, GLIB_001:37
.= C.first() by A1, GLIB_001:def 24
.= W1.first() by A3, A11, A12, GLIB_001:37;
A29: W1 is open by A1, A3, A6, A11, A26, Th30;
A30: W2 is open by A1, A26, A27, Th30;
now
let x be object;
hereby
assume x in W2.vertices() /\ W1.vertices();
then A31: x in W2.vertices() & x in W1.vertices()
by XBOOLE_0:def 4;
then consider n0 being odd Element of NAT such that
A32: n0 <= len W1 & W1.n0 = x by GLIB_001:87;
consider m0 being odd Element of NAT such that
A33: m0 <= len W2 & W2.m0 = x by A31, GLIB_001:87;
1 <= n0 & 1 <= m0 by CHORD:2;
then A34: n0 in dom W1 & m0 in dom W2 by A32, A33, FINSEQ_3:25;
A35: m0-1 >= 1-1 by CHORD:2, XREAL_1:9;
then 0+m <= m0-1+m by XREAL_1:6;
then A36: n < m+m0-1 by A6, XXREAL_0:2;
len W1 + 1 = n + 1 by A3, A11, A12, GLIB_001:36;
then A37: n0 < m+m0-1 by A32, A36, XXREAL_0:2;
reconsider m1 = m0-1 as Element of NAT by A35, INT_1:3;
m1+1 <= len W2 by A33;
then m1 < len W2 by NAT_1:13;
then m+m1 in dom C by A4, GLIB_001:36;
then A38: m+m0-1 <= len C by FINSEQ_3:25;
A39: m+m1 is odd;
C.n0 = C.(1+n0-1)
.= W2.m0 by A3, A11, A12, A32, A33, A34, GLIB_001:47
.= C.(m+m0-1) by A4, A34, GLIB_001:47;
then n0 = 1 by A1, A37, A38, A39, GLIB_001:def 28;
hence x = W2.last() by A28, A32;
end;
assume x = W2.last();
then x in W2.vertices() & x in W1.vertices() by A28, GLIB_001:88;
hence x in W2.vertices() /\ W1.vertices() by XBOOLE_0:def 4;
end;
then W2.vertices() /\ W1.vertices() = {W2.last()} by TARSKI:def 1;
then W2.append(W1) is Path of G by A28, A29, A30, HELLY:19;
then reconsider W = W2.append(W1).reverse() as Path of G;
take W;
W1 is_Walk_from C.first(),C.n by A3, A11, A12, GLIB_001:37;
then A40: W1 is_Walk_from C.last(),C.n by A1, GLIB_001:def 24;
A41: W2 is_Walk_from C.m,C.last() by A4, GLIB_001:37;
W2.append(W1) is_Walk_from C.m,C.n by A40, A41, GLIB_001:31;
hence W is_Walk_from u,v by A3, A4, GLIB_001:23;
thus not w in W.vertices()
proof
A42: W1.first() = C.last() by A40, GLIB_001:def 23
.= W2.last() by A41, GLIB_001:def 23;
assume w in W.vertices();
then w in W2.append(W1).vertices() by GLIB_001:92;
then w in W2.vertices() \/ W1.vertices() by A42, GLIB_001:93;
then per cases by XBOOLE_0:def 3;
suppose w in W2.vertices();
hence contradiction by A26, A20, XREAL_1:31;
end;
suppose w in W1.vertices();
hence contradiction by A13, A14, A26, NAT_1:13;
end;
end;
end;
suppose A43: n = 1;
take W2.reverse();
W2 is_Walk_from C.m,C.last() by A4, GLIB_001:37;
then W2 is_Walk_from C.m,C.first() by A1, GLIB_001:def 24;
hence W2.reverse() is_Walk_from u,v by A3, A4, A43, GLIB_001:23;
thus not w in W2.reverse().vertices()
by A2, A3, A20, A8, A10, A43, GLIB_001:92;
end;
suppose A44: m = len C;
take W1.reverse();
W1 is_Walk_from C.1,C.n by A3, A11, A12, GLIB_001:37;
then W1 is_Walk_from C.m,C.n by A1, A44, GLIB_001:118;
hence W1.reverse() is_Walk_from u,v by A3, A4, GLIB_001:23;
thus not w in W1.reverse().vertices()
by A2, A4, A14, A8, A10, A44, GLIB_001:92;
end;
end;
end;
:: symmetric case
suppose A45: u <> v & m < n;
per cases;
suppose A46: not w in C.cut(m,n).vertices();
reconsider W = C.cut(m,n) as Path of G by A1;
take W.reverse();
thus thesis by A3, A4, A45, A46, GLIB_001:23, 37, 92;
end;
suppose w in C.cut(m,n).vertices();
then consider k being odd Element of NAT such that
A47: k <= len C.cut(m,n) & C.cut(m,n).k = w by GLIB_001:87;
reconsider k3=k-1 as even Nat by CHORD:2;
reconsider k3 as Element of NAT by ORDINAL1:def 12;
k < len C.cut(m,n) + 1 by A47, NAT_1:13;
then A48: k3 < len C.cut(m,n) + 1 - 1 by XREAL_1:14;
A49: C.cut(m,n).(k3+1) = C.(m+k3) by A3, A45, A48, GLIB_001:36;
reconsider W1 = C.cut(1,m), W2 = C.cut(n,len C) as Path of G by A1;
A50: 1 is odd & len C is odd by POLYFORM:4;
A51: 1 <= m by CHORD:2;
len C.cut(m,n) + m = n + 1 by A3, A45, GLIB_001:36;
then A52: m+k3 < n + 1 by A48, XREAL_1:8;
A53: w in W1.vertices() implies m+k3 = len C
proof
assume w in W1.vertices();
then consider k2 being odd Element of NAT such that
A54: k2 <= len W1 & W1.k2 = w by GLIB_001:87;
reconsider k4=k2-1 as Nat by CHORD:2;
reconsider k4 as Element of NAT by ORDINAL1:def 12;
k2 < len W1 + 1 by A54, NAT_1:13;
then k4 < len W1 + 1 - 1 by XREAL_1:14;
then A55: W1.(k4+1) = C.(1+k4) by A4, A50, A51, GLIB_001:36;
then A56: C.(m+k3) = C.(1+k4) by A47, A49, A54;
len W1 + 1 = m + 1 by A4, A50, A51, GLIB_001:36;
then 1+k4 < m by A2, A4, A54, A55, XXREAL_0:1;
then A58: 1+k4+0 < m+k3 by XREAL_1:8;
m+k3 <= n by A52, NAT_1:13;
then m+k3 <= len C by A3, XXREAL_0:2;
hence m+k3 = len C by A1, A56, A58, GLIB_001:def 28;
end;
A59: w in W2.vertices() implies m+k3 = 1
proof
assume w in W2.vertices();
then consider k2 being odd Element of NAT such that
A60: k2 <= len W2 & W2.k2 = w by GLIB_001:87;
reconsider k4=k2-1 as Nat by CHORD:2;
reconsider k4 as Element of NAT by ORDINAL1:def 12;
k2 < len W2 + 1 by A60, NAT_1:13;
then A61: k4 < len W2 + 1 - 1 by XREAL_1:14;
then A62: W2.(k4+1) = C.(n+k4) by A3, GLIB_001:36;
then A63: C.(m+k3) = C.(n+k4) by A47, A49, A60;
1 < k4
proof
assume k4 <= 1;
then k4 = 0 by A50, NAT_1:25;
hence contradiction by A2, A3, A60, A62;
end;
then n+1 < n+k4 by XREAL_1:8;
then A64: m+k3 < n+k4 by A52, XXREAL_0:2;
n+k4 < len W2 + n by A61, XREAL_1:8;
then n+k4 < len C + 1 by A3, GLIB_001:36;
then n+k4 <= len C by NAT_1:13;
hence m+k3 = 1 by A1, A63, A64, GLIB_001:def 28;
end;
per cases;
suppose m <> 1 & n <> len C;
then A65: 1 < m & n < len C by A3, A51, XXREAL_0:1;
then A66: n <> 1 by A45;
A67: W2.last() = C.last() by A3, GLIB_001:37
.= C.first() by A1, GLIB_001:def 24
.= W1.first() by A4, A50, A51, GLIB_001:37;
A68: W1 is open by A1, A4, A45, A50, A65, Th30;
A69: W2 is open by A1, A65, A66, Th30;
now
let x be object;
hereby
assume x in W2.vertices() /\ W1.vertices();
then A70: x in W2.vertices() & x in W1.vertices()
by XBOOLE_0:def 4;
then consider n0 being odd Element of NAT such that
A71: n0 <= len W1 & W1.n0 = x by GLIB_001:87;
consider m0 being odd Element of NAT such that
A72: m0 <= len W2 & W2.m0 = x by A70, GLIB_001:87;
1 <= n0 & 1 <= m0 by CHORD:2;
then A73: n0 in dom W1 & m0 in dom W2 by A71, A72, FINSEQ_3:25;
A74: m0-1 >= 1-1 by CHORD:2, XREAL_1:9;
then 0+n <= m0-1+n by XREAL_1:6;
then A75: m < n+m0-1 by A45, XXREAL_0:2;
len W1 + 1 = m + 1 by A4, A50, A51, GLIB_001:36;
then A76: n0 < n+m0-1 by A71, A75, XXREAL_0:2;
reconsider m1 = m0-1 as Element of NAT by A74, INT_1:3;
m1+1 <= len W2 by A72;
then m1 < len W2 by NAT_1:13;
then n+m1 in dom C by A3, GLIB_001:36;
then A77: n+m0-1 <= len C by FINSEQ_3:25;
A78: n+m1 is odd;
C.n0 = C.(1+n0-1)
.= W2.m0 by A4, A50, A51, A71, A72, A73, GLIB_001:47
.= C.(n+m0-1) by A3, A73, GLIB_001:47;
then n0 = 1 by A1, A76, A77, A78, GLIB_001:def 28;
hence x = W2.last() by A67, A71;
end;
assume x = W2.last();
then x in W2.vertices() & x in W1.vertices() by A67, GLIB_001:88;
hence x in W2.vertices() /\ W1.vertices() by XBOOLE_0:def 4;
end;
then W2.vertices() /\ W1.vertices() = {W2.last()} by TARSKI:def 1;
then reconsider W = W2.append(W1) as Path of G
by A67, A68, A69, HELLY:19;
take W;
W1 is_Walk_from C.first(),C.m by A4, A50, A51, GLIB_001:37;
then A79: W1 is_Walk_from C.last(),C.m by A1, GLIB_001:def 24;
A80: W2 is_Walk_from C.n,C.last() by A3, GLIB_001:37;
W2.append(W1) is_Walk_from C.n,C.m by A79, A80, GLIB_001:31;
hence W is_Walk_from u,v by A3, A4;
thus not w in W.vertices()
proof
A81: W1.first() = C.last() by A79, GLIB_001:def 23
.= W2.last() by A80, GLIB_001:def 23;
assume w in W.vertices();
then w in W2.vertices() \/ W1.vertices() by A81, GLIB_001:93;
then per cases by XBOOLE_0:def 3;
suppose w in W2.vertices();
hence contradiction by A65, A59, XREAL_1:31;
end;
suppose w in W1.vertices();
hence contradiction by A52, A53, A65, NAT_1:13;
end;
end;
end;
suppose A82: m = 1;
take W2;
W2 is_Walk_from C.n,C.last() by A3, GLIB_001:37;
then W2 is_Walk_from C.n,C.first() by A1, GLIB_001:def 24;
hence W2 is_Walk_from u,v by A3, A4, A82;
thus not w in W2.vertices()
by A2, A4, A59, A47, A49, A82;
end;
suppose A83: n = len C;
take W1;
W1 is_Walk_from C.1,C.m by A4, A50, A51, GLIB_001:37;
hence W1 is_Walk_from u,v by A1, A3, A4, A83, GLIB_001:118;
thus not w in W1.vertices() by A2, A3, A53, A47, A49, A83;
end;
end;
end;
end;