:: Miscellaneous Graph Preliminaries
:: by Sebastian Koch
::
:: Received December 30, 2019
:: Copyright (c) 2019-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FINSEQ_1, SUBSET_1, RELAT_1, FUNCT_1, TARSKI, ARYTM_3,
CARD_1, XBOOLE_0, GLIB_000, PARTFUN1, FINSET_1, ZFMISC_1, RELAT_2,
FUNCT_2, GLIB_009, MOD_4, WAYBEL_0, GLIB_006, GLIB_007, FUNCT_4,
ORDINAL2, CARD_2, SCMYCIEL, SGRAPH1, GLIB_010, MATRIX11, BSPACE,
SETFAM_1, ORDINAL1, FUNCT_7, YELLOW_1, WELLORD2, CHORD, NAT_1, GLIB_002,
XXREAL_0, CARD_3, FUNCOP_1, PBOOLE, EQREL_1, RFINSEQ, FINSEQ_8, GRAPH_2,
ORDINAL4, RING_3, GLIB_011, ARYTM_1, GLIB_001;
notations TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1,
ENUMSET1, FUNCT_1, RELAT_2, ORDINAL1, RELSET_1, PARTFUN1, WELLORD2,
FUNCT_2, DOMAIN_1, FUNCOP_1, FUNCT_4, FINSET_1, CARD_1, PBOOLE, CHORD,
PARTFUN2, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, VALUED_0, NAT_D,
CARD_2, FINSEQ_1, EQREL_1, FINSEQ_2, FINSEQ_4, NEWTON, FUNCT_7, RFINSEQ,
FINSEQ_6, FINSEQ_8, ORDERS_1, CARD_3, ABIAN, GLIB_000, GLIB_001,
STRUCT_0, ORDERS_2, GROUP_1, GROUP_2, GROUP_6, YELLOW_1, SGRAPH1,
MATRIX11, GLIB_002, GLIB_003, BSPACE, ORDERS_5, GLIB_006, GLIB_007,
GLIB_008, GLIB_009, GLIB_010, GLIB_011;
constructors DOMAIN_1, FUNCT_4, XXREAL_0, NAT_1, NAT_D, BINOP_2, CARD_2,
FINSEQ_4, PBOOLE, ORDINAL3, WELLORD2, PARTFUN1, RELSET_1, GLIB_000,
STRUCT_0, RELAT_1, FUNCT_1, FUNCT_2, ALGSTR_0, GROUP_1, GLIB_001, ABIAN,
CARD_3, FINSEQ_1, GLIB_002, GLIB_003, SETFAM_1, EQREL_1, GROUP_2,
GROUP_6, GLIB_006, GLIB_007, PARTFUN2, BSPACE, SETWISEO, CHORD, RAT_1,
MATRIX11, GLIB_008, FUNCT_7, GLIB_009, GLIB_010, SQUARE_1, NEWTON,
VALUED_0, CLASSES1, FINSEQ_2, SGRAPH1, ORDERS_2, YELLOW_1, RFINSEQ,
GRAPH_2, FINSEQ_8, GLIB_011, FINSEQ_6, ENUMSET1, ORDERS_5;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1,
XREAL_0, NAT_1, FINSEQ_1, GLIB_000, CARD_1, FUNCT_2, RELSET_1, XTUPLE_0,
CARD_3, GLIB_006, GLIB_008, GLIB_009, GLIB_010, MSAFREE5, GRFUNC_1,
RELAT_2, SUBSET_1, GLIB_011;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
equalities ORDINAL1, GLIB_000, GLIB_010, BSPACE, SGRAPH1, YELLOW_1;
theorems TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XBOOLE_1, CARD_1, CARD_2,
RELAT_1, RELSET_1, FUNCT_1, FUNCT_2, FUNCOP_1, PARTFUN1, FINSEQ_1,
FINSEQ_3, XXREAL_0, GLIB_000, GLIB_001, GLIB_002, GLIB_006, GLIB_007,
WELLORD2, XTUPLE_0, FUNCT_4, ORDINAL1, CHORD, GLIB_008, GLIB_009,
GLIB_010, SETFAM_1, NAT_1, ORDINAL3, GRFUNC_1, SUBSET_1, MATRIX13,
RELAT_2, WELLSET1, FRIENDS1, EQREL_1, ORDERS_5, FINSEQ_5, RFINSEQ,
FINSEQ_6, FINSEQ_8, PENCIL_1, ORDERS_1, CARD_3, GLIB_011;
schemes FUNCT_1, ORDINAL1;
begin :: Preliminaries not directly related to graphs
:: generalization of XBOOLE_1:45
:: into XBOOLE_1 ?
theorem
for X,Y,Z being set st Z c= X holds X \/ (Y \ Z) = X \/ Y
proof
let X,Y,Z be set;
assume A1: Z c= X;
A2: X \/ (Y \ Z) c= X \/ Y by XBOOLE_1:9;
now
let x be object;
assume x in X \/ Y;
then per cases by XBOOLE_0:def 3;
suppose x in X;
hence x in X \/ (Y \ Z) by XBOOLE_0:def 3;
end;
suppose x in Y & not x in Z;
then x in Y \ Z by XBOOLE_0:def 5;
hence x in X \/ (Y \ Z) by XBOOLE_0:def 3;
end;
suppose x in Y & x in Z;
hence x in X \/ (Y \ Z) by A1, XBOOLE_0:def 3;
end;
end;
then X \/ Y c= X \/ (Y \ Z) by TARSKI:def 3;
hence thesis by A2, XBOOLE_0:def 10;
end;
:: generalization of XBOOLE_1:89
:: into XBOOLE_1 ?
theorem Th2:
for X, Y, Z being set holds X /\ Z misses Y \ Z
proof
let X, Y, Z be set;
(X /\ Z) /\ (Y \ Z) = X /\ (Z /\ (Y \ Z)) by XBOOLE_1:16
.= X /\ ((Z /\ Y) \ (Z /\ Z)) by XBOOLE_1:50
.= X /\ {} by XBOOLE_1:17, XBOOLE_1:37
.= {};
hence thesis by XBOOLE_0:def 7;
end;
:: into ZFMISC_1 ?
theorem
for x,y being object holds {x,y}\{the Element of {x,y}} = {} iff x = y
proof
let x,y be object;
set z = the Element of {x,y};
hereby
assume {x,y}\{z} = {};
then {x,y} c= {z} by XBOOLE_1:37;
then x = z & y = z by ZFMISC_1:20;
hence x = y;
end;
assume x = y;
then {x,y} = {x} by ENUMSET1:29;
then {z} = {x,y} by TARSKI:def 1;
hence thesis by XBOOLE_1:37;
end;
:: into ZFMISC_1 ?
theorem
for a,b,x,y being object st a <> b & x = the Element of {a,b} &
y = the Element of ({a,b}\{the Element of {a,b}})
holds x = a & y = b or x = b & y = a
proof
let a,b,x,y be object;
assume A1: a <> b & x = the Element of {a,b} &
y = the Element of ({a,b}\{the Element of {a,b}});
then per cases by TARSKI:def 2;
suppose A2: x = a;
{a,b}\{a} = {b} by A1, ZFMISC_1:17;
hence thesis by A1, A2, TARSKI:def 1;
end;
suppose A3: x = b;
{a,b}\{b} = {a} by A1, ZFMISC_1:17;
hence thesis by A1, A3, TARSKI:def 1;
end;
end;
:: into ZFMISC_1 ?
theorem
for a,b,x,y being object holds {a,b} = {x,y} iff
x = a & y = b or x = b & y = a by ZFMISC_1:22;
:: into SUBSET_1 ?
theorem
for X being set, Y being non empty set
holds X c< Y iff X is proper Subset of Y by SUBSET_1:def 6, XBOOLE_0:def 8;
registration
let X be non empty set;
cluster id X -> non irreflexive;
coherence
proof
ex x being object st x in field id X & [x,x] in id X
proof
consider x being object such that
A1: x in X by XBOOLE_0:def 1;
take x;
A2: field id X = dom id X \/ rng id X by RELAT_1:def 6;
thus x in field id X by A1, A2;
thus [x,x] in id X by A1, RELAT_1:def 10;
end;
hence id X is non irreflexive by RELAT_2:def 2, RELAT_2:def 10;
end;
cluster [: X, X :] -> non irreflexive non asymmetric;
coherence
proof
ex x being object st x in field [: X,X :] & [x,x] in [: X,X :]
proof
consider x being object such that
A3: x in X by XBOOLE_0:def 1;
take x;
field [: X,X :] = X \/ X by WELLSET1:2;
hence x in field [: X,X :] by A3;
thus [x,x] in [: X,X :] by A3, ZFMISC_1:def 2;
end;
hence thesis by RELAT_2:def 2, RELAT_2:def 10;
end;
cluster non irreflexive non asymmetric for Relation of X;
existence
proof
take R = [: X, X :];
R c= R;
hence thesis;
end;
cluster symmetric irreflexive non total for Relation of X;
existence
proof
take the empty Relation of X;
thus thesis;
end;
cluster symmetric non irreflexive non empty for Relation of X;
existence
proof
take id X;
thus thesis;
end;
end;
registration
let X be non trivial set;
cluster id X -> non connected;
coherence
proof
set x = the Element of X;
set y = the Element of X \ {x};
[x,x] in id X & [y,y] in id X by RELAT_1:def 10;
then A1: x in field id X & y in field id X by RELAT_1:15;
not y in {x} by XBOOLE_0:def 5;
then A2: y <> x by TARSKI:def 1;
then not [x,y] in id X & not [y,x] in id X by RELAT_1:def 10;
hence thesis by A1, A2, RELAT_2:def 6, RELAT_2:def 14;
end;
cluster symmetric non connected for Relation of X;
existence
proof
take id X;
thus thesis;
end;
cluster [: X, X :] -> non antisymmetric;
coherence
proof
set x = the Element of X;
set y = the Element of X \ {x};
A3: [x,y] in [: X,X :] & [y,x] in [: X,X :] by ZFMISC_1:87;
then A4: x in field [: X,X :] & y in field [: X,X :] by RELAT_1:15;
not y in {x} by XBOOLE_0:def 5;
then x <> y by TARSKI:def 1;
hence thesis by A3, A4, RELAT_2:def 4, RELAT_2:def 12;
end;
cluster non antisymmetric for Relation of X;
existence
proof
take [: X, X :];
[: X, X :] c= [: X, X :];
hence thesis;
end;
end;
:: into RELAT_1 ?
theorem
for R,S being Relation, X being set holds (R\/S).:X = R.:X \/ S.:X
proof
let R, S be Relation, X be set;
now
let y be object;
hereby
assume y in (R \/ S).:X;
then consider x being object such that
A1: [x,y] in R \/ S & x in X by RELAT_1:def 13;
per cases by A1, XBOOLE_0:def 3;
suppose [x,y] in R;
then y in R.:X by A1, RELAT_1:def 13;
hence y in R.:X \/ S.:X by XBOOLE_0:def 3;
end;
suppose [x,y] in S;
then y in S.:X by A1, RELAT_1:def 13;
hence y in R.:X \/ S.:X by XBOOLE_0:def 3;
end;
end;
assume y in R.:X \/ S.:X;
then per cases by XBOOLE_0:def 3;
suppose y in R.:X;
then consider x being object such that
A2: [x,y] in R & x in X by RELAT_1:def 13;
[x,y] in R \/ S by A2, XBOOLE_0:def 3;
hence y in (R \/ S).:X by A2, RELAT_1:def 13;
end;
suppose y in S.:X;
then consider x being object such that
A3: [x,y] in S & x in X by RELAT_1:def 13;
[x,y] in R \/ S by A3, XBOOLE_0:def 3;
hence y in (R \/ S).:X by A3, RELAT_1:def 13;
end;
end;
hence thesis by TARSKI:2;
end;
:: into RELAT_1 ?
theorem
for R,S being Relation, Y being set holds (R\/S)"Y = R"Y \/ S"Y
proof
let R, S be Relation, Y be set;
now
let x be object;
hereby
assume x in (R \/ S)"Y;
then consider y being object such that
A1: [x,y] in R \/ S & y in Y by RELAT_1:def 14;
per cases by A1, XBOOLE_0:def 3;
suppose [x,y] in R;
then x in R"Y by A1, RELAT_1:def 14;
hence x in R"Y \/ S"Y by XBOOLE_0:def 3;
end;
suppose [x,y] in S;
then x in S"Y by A1, RELAT_1:def 14;
hence x in R"Y \/ S"Y by XBOOLE_0:def 3;
end;
end;
assume x in R"Y \/ S"Y;
then per cases by XBOOLE_0:def 3;
suppose x in R"Y;
then consider y being object such that
A2: [x,y] in R & y in Y by RELAT_1:def 14;
[x,y] in R \/ S by A2, XBOOLE_0:def 3;
hence x in (R \/ S)"Y by A2, RELAT_1:def 14;
end;
suppose x in S"Y;
then consider y being object such that
A3: [x,y] in S & y in Y by RELAT_1:def 14;
[x,y] in R \/ S by A3, XBOOLE_0:def 3;
hence x in (R \/ S)"Y by A3, RELAT_1:def 14;
end;
end;
hence thesis by TARSKI:2;
end;
:: into RELAT_1 ?
theorem
for R being Relation, X,Y being set holds Y|`R|X = Y|`R /\ R|X
proof
let R be Relation, X,Y be set;
now
let z be object;
hereby
assume A1: z in Y|`R|X;
then consider x,y being object such that
A2: z = [x,y] by RELAT_1:def 1;
A3: z in Y|`R & x in X by A1, A2, RELAT_1:def 11;
then z in R by A2, RELAT_1:def 12;
then z in R|X by A2, A3, RELAT_1:def 11;
hence z in Y|`R /\ R|X by A3, XBOOLE_0:def 4;
end;
assume z in Y|`R /\ R|X;
then A4: z in Y|`R & z in R|X by XBOOLE_0:def 4;
then consider x,y being object such that
A5: z = [x,y] by RELAT_1:def 1;
x in X by A4, A5, RELAT_1:def 11;
hence z in Y|`R|X by A4, A5, RELAT_1:def 11;
end;
hence thesis by TARSKI:2;
end;
:: into RELAT_2 ?
theorem
for R being symmetric Relation, x being object holds Im(R,x) = Coim(R,x)
proof
let R be symmetric Relation, x be object;
thus Im(R,x) = R.:{x} by RELAT_1:def 16
.= R"{x} by FRIENDS1:2
.= Coim(R,x) by RELAT_1:def 17;
end;
:: into RELSET_1 ?
theorem
for X being set, R being Relation of X
holds R is irreflexive iff id X misses R
proof
let X be set, R be Relation of X;
hereby
assume A1: R is irreflexive;
assume id X meets R;
then (id X) /\ R <> {} by XBOOLE_0:def 7;
then consider z being object such that
A2: z in (id X) /\ R by XBOOLE_0:def 1;
consider x,y being object such that
A3: z = [x,y] by A2, RELAT_1:def 1;
A4: [x,y] in id X & [x,y] in R by A2, A3, XBOOLE_0:def 4;
then x = y & x in field R by RELAT_1:def 10, RELAT_1:15;
hence contradiction by A1, A4, RELAT_2:def 2, RELAT_2:def 10;
end;
assume A5: id X misses R;
field R c= X \/ X
by RELSET_1:8;
then id field R misses R by A5, FUNCT_4:3, XBOOLE_1:63;
hence thesis by RELAT_2:2;
end;
:: into ZFMISC_1 or SYSREL ? (in both cases the qua can be omitted)
theorem
for x,y being object holds ({[x,y]} qua Relation)~ = {[y,x]}
proof
let x,y be object;
set Z = ({[x,y]} qua Relation)~;
now
let a,b be object;
hereby
assume [a,b] in Z;
then [b,a] in {[x,y]} by RELAT_1:def 7;
then [b,a] = [x,y] by TARSKI:def 1;
then b = x & a = y by XTUPLE_0:1;
hence [a,b] in {[y,x]} by TARSKI:def 1;
end;
assume [a,b] in {[y,x]};
then [a,b] = [y,x] by TARSKI:def 1;
then a = y & b = x by XTUPLE_0:1;
then [b,a] in {[x,y]} by TARSKI:def 1;
hence [a,b] in Z by RELAT_1:def 7;
end;
hence thesis by RELAT_1:def 2;
end;
:: generalization of EQREL_1:6 (total is unneeded assumption)
:: into EQREL_1 ?
theorem
for X being set, x,y being object, R being symmetric Relation of X
holds [x,y] in R implies [y,x] in R
proof
let X be set, x,y be object, R be symmetric Relation of X;
assume A1: [x,y] in R;
then x in field R & y in field R by RELAT_1:15;
hence thesis by A1, RELAT_2:def 3, RELAT_2:def 11;
end;
:: into CARD_1 ?
registration
let a, b be Cardinal;
cluster a /\ b -> cardinal;
coherence by ORDINAL3:13;
cluster a \/ b -> cardinal;
coherence by ORDINAL3:12;
end;
:: into ORDINAL1 or WELLORD2 ?
registration
let X be c=-linear set;
cluster RelIncl X -> connected;
coherence
proof
now
let x, y be object;
assume x in field RelIncl X & y in field RelIncl X & x <> y;
then A1: x in X & y in X by WELLORD2:def 1;
reconsider A = x, B = y as set by TARSKI:1;
per cases by A1, ORDINAL1:def 8, XBOOLE_0:def 9;
suppose A c= B;
hence [x,y] in RelIncl X or [y,x] in RelIncl X by A1, WELLORD2:def 1;
end;
suppose B c= A;
hence [x,y] in RelIncl X or [y,x] in RelIncl X by A1, WELLORD2:def 1;
end;
end;
hence thesis by RELAT_2:def 6, RELAT_2:def 14;
end;
end;
:: into YELLOW_1 or ORDERS_5 ?
registration
let X be c=-linear set;
cluster InclPoset X -> connected;
coherence
proof
field RelIncl X = X by ORDERS_1:12;
hence thesis by RELAT_2:def 14, ORDERS_5:def 1;
end;
end;
:: into CARD_1 ?
theorem Th15:
for X being non empty set
st for a being set st a in X holds a is cardinal number
ex A being Cardinal st A in X & A = meet X
proof
let X be non empty set;
assume A1: for a being set st a in X holds a is cardinal number;
defpred P[Ordinal] means $1 in X & $1 is cardinal number;
A2: ex A being Ordinal st P[A]
proof
consider A being object such that
A3: A in X by XBOOLE_0:def 1;
reconsider A as Ordinal by A1, A3;
take A;
thus thesis by A1, A3;
end;
consider A being Ordinal such that
A4: P[A] & for B being Ordinal st P[B] holds A c= B
from ORDINAL1:sch 1(A2);
reconsider A as Cardinal by A4;
take A;
thus A in X by A4;
A5: meet X c= A by A4, SETFAM_1:3;
now
let x be object;
assume A6: x in A;
now
let Y be set;
assume A7: Y in X;
then reconsider B = Y as Ordinal by A1;
B in X & B is cardinal number by A1, A7;
then A c= B by A4;
hence x in Y by A6;
end;
hence x in meet X by SETFAM_1:def 1;
end;
then A c= meet X by TARSKI:def 3;
hence A = meet X by A5, XBOOLE_0:def 10;
end;
:: analogous to TOPGEN_2:3
:: into CARD_1 ?
theorem
for X being set st for a being set st a in X holds a is cardinal number
holds meet X is cardinal number
proof
let X be set;
assume A1: for a being set st a in X holds a is cardinal number;
per cases;
suppose X = {};
hence thesis by SETFAM_1:def 1;
end;
suppose X <> {};
then consider A being Cardinal such that
A2: A in X & A = meet X by A1, Th15;
thus thesis by A2;
end;
end;
:: into CARD_3 ?
registration
let f be Cardinal-yielding Function, x be object;
cluster f.x -> cardinal;
coherence
proof
per cases;
suppose x in dom f;
hence thesis by CARD_3:def 1;
end;
suppose not x in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
Th19:
for X being functional set holds meet X is Function
proof
let X be functional set;
per cases;
suppose A1: X <> {};
consider Z being object such that
A2: Z in X by A1, XBOOLE_0:def 1;
reconsider Z as set by TARSKI:1;
A3: now
let x be object;
assume x in meet X;
then x in Z by A2, SETFAM_1:def 1;
then consider y,z being object such that
A4: x = [y,z] by A2, RELAT_1:def 1;
take y,z;
thus x = [y,z] by A4;
end;
now
let x,y1,y2 be object;
assume [x,y1] in meet X & [x,y2] in meet X;
then [x,y1] in Z & [x,y2] in Z by A2, SETFAM_1:def 1;
hence y1 = y2 by A2, FUNCT_1:def 1;
end;
hence thesis by A3, RELAT_1:def 1, FUNCT_1:def 1;
end;
suppose X = {};
hence thesis by SETFAM_1:def 1;
end;
end;
registration
let X be functional set;
cluster meet X -> Function-like Relation-like;
coherence by Th19;
end;
:: into PENCIL_1 ?
:: mostly copied from there
theorem Th20:
for X being set holds 4 c= card X iff
ex w,x,y,z being object st w in X & x in X & y in X & z in X &
w<>x & w<>y & w<>z & x<>y & x<>z & y<>z
proof
let X be set;
thus 4 c= card X implies
ex w,x,y,z being object st w in X & x in X & y in X & z in X &
w<>x & w<>y & w <> z & x<>y & x<>z & y<>z
proof
assume 4 c= card X;
then card 4 c= card X;
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = 4 and
A3: rng f c= X by CARD_1:10;
take w=f.0;
take x=f.1;
take y=f.2;
take z=f.3;
A4: 0 in dom f by A2,ENUMSET1:def 2,CARD_1:52;
then f.0 in rng f by FUNCT_1:def 3;
hence w in X by A3;
A5: 1 in dom f by A2,ENUMSET1:def 2,CARD_1:52;
then f.1 in rng f by FUNCT_1:def 3;
hence x in X by A3;
A6: 2 in dom f by A2,ENUMSET1:def 2,CARD_1:52;
then f.2 in rng f by FUNCT_1:def 3;
hence y in X by A3;
A7: 3 in dom f by A2,ENUMSET1:def 2,CARD_1:52;
then f.3 in rng f by FUNCT_1:def 3;
hence z in X by A3;
thus w <> x by A1,A4,A5,FUNCT_1:def 4;
thus w <> y by A1,A4,A6,FUNCT_1:def 4;
thus w <> z by A1,A4,A7,FUNCT_1:def 4;
thus x <> y by A1,A5,A6,FUNCT_1:def 4;
thus x <> z by A1,A5,A7,FUNCT_1:def 4;
thus thesis by A1,A6,A7,FUNCT_1:def 4;
end;
given w,x,y,z being object such that
A8: w in X & x in X & y in X & z in X and
A9: w<>x & w<>y & w<>z & x<>y & x<>z & y<>z;
for a being object st a in {w,x,y,z} holds a in X by A8,ENUMSET1:def 2;
then card {w,x,y,z} c= card X by TARSKI:def 3, CARD_1:11;
hence thesis by A9, CARD_2:59;
end;
:: into PENCIL_1 ?
theorem Th21:
for X being set st 4 c= card X for w,x,y being object ex z being object
st z in X & w<>z & x<>z & y<>z
proof
let X be set;
assume 4 c= card X;
then consider a,b,c,d being object such that
A1: a in X and
A2: b in X and
A3: c in X and
A4: d in X and
A5: a<>b & a<>c & a<>d & b<>c & b<>d & d<>c by Th20;
let w,x,y be object;
per cases;
suppose
w <> a & x <> a & y <> a;
hence thesis by A1;
end;
suppose
w <> a & x <> a & y = a & w <> b & x <> b;
hence thesis by A2,A5;
end;
suppose
w <> a & x <> a & y = a & w <> b & x = b & w <> c;
hence thesis by A3,A5;
end;
suppose
w <> a & x <> a & y = a & w <> b & x = b & w = c;
hence thesis by A4,A5;
end;
suppose
w <> a & x <> a & y = a & w = b & x <> c;
hence thesis by A3,A5;
end;
suppose
w <> a & x <> a & y = a & w = b & x = c;
hence thesis by A4,A5;
end;
suppose
w <> a & x = a & w <> b & y <> b;
hence thesis by A2,A5;
end;
suppose
w <> a & x = a & w <> b & y = b & w <> c;
hence thesis by A3,A5;
end;
suppose
w <> a & x = a & w <> b & y = b & w = c;
hence thesis by A4,A5;
end;
suppose
w <> a & x = a & w = b & y <> c;
hence thesis by A3,A5;
end;
suppose
w <> a & x = a & w = b & y = c;
hence thesis by A4,A5;
end;
suppose
w = a & x <> b & y <> b;
hence thesis by A2,A5;
end;
suppose
w = a & x <> b & y = b & x <> c;
hence thesis by A3,A5;
end;
suppose
w = a & x <> b & y = b & x = c;
hence thesis by A4,A5;
end;
suppose
w = a & x = b & y <> c;
hence thesis by A3,A5;
end;
suppose
w = a & x = b & y = c;
hence thesis by A4,A5;
end;
end;
:: into BSPACE or SGRAPH1 ?
theorem
for X being set holds singletons X misses 2Set X
proof
let X be set;
assume singletons X meets 2Set X;
then consider x being object such that
A1: x in (singletons X) /\ 2Set X by XBOOLE_0:4;
A2: x in singletons X & x in 2Set X by A1, XBOOLE_0:def 4;
then consider Y being Subset of X such that
A3: x = Y & Y is 1-element;
consider Z being Subset of X such that
A4: x = Z & card Z = 2 by A2;
thus contradiction by A3, A4, CARD_1:def 7;
end;
:: into SGRAPH1 or MATRIX11 ?
theorem Th23:
for X, Y being set st card X = card Y holds card 2Set X = card 2Set Y
proof
let X, Y be set;
:: the basic idea is to build a canonical bijection between the 2Sets
:: from the bijection of the sets
assume card X = card Y;
then consider g being Function such that
A1: g is one-to-one & dom g = X & rng g = Y by CARD_1:5, WELLORD2:def 4;
deffunc E1(set) = the Element of $1;
deffunc E2(set) = the Element of ($1\{E1($1)});
deffunc F(object) = {g.E1(In($1,bool X)),g.E2(In($1,bool X))};
:: basically f.{x,y} = {g.x,g.y}
consider f being Function such that
A2: dom f = 2Set X & for x being object st x in 2Set X holds f.x = F(x)
from FUNCT_1:sch 3;
:: show that range equals 2Set Y
now
let y be object;
hereby
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;
consider X9 being Subset of X such that
A4: x = X9 & card X9 = 2 by A2, A3;
A5: y = {g.E1(In(X9,bool X)),g.E2(In(X9,bool X))} by A2, A3, A4
.= {g.E1(X9),g.E2(X9)};
X9 is non trivial
proof
assume A6: X9 is trivial;
per cases;
suppose X9 is empty;
hence contradiction by A4;
end;
suppose X9 is non empty;
then card X9 = 1 by A6, CARD_1:def 7;
hence contradiction by A4;
end;
end;
then X9 <> {} & X9\{E1(X9)} <> {} by ZFMISC_1:139;
then A7: E1(X9) in X9 & E2(X9) in X9\{E1(X9)};
then E2(X9) in X9 & not E2(X9) in {E1(X9)} by XBOOLE_0:def 5;
then E2(X9) in X9 & E1(X9) <> E2(X9) by TARSKI:def 1;
then A8: g.E1(X9) <> g.E2(X9) by A1, A7, FUNCT_1:def 4;
g.E1(X9) in Y & g.E2(X9) in Y by A1, A7, FUNCT_1:3;
then A9: {g.E1(X9),g.E2(X9)} c= Y by ZFMISC_1:32;
card {g.E1(X9),g.E2(X9)} = 2 by A8, CARD_2:57;
hence y in 2Set Y by A5, A9;
end;
assume y in 2Set Y;
then consider Y9 being Subset of Y such that
A10: y = Y9 & card Y9 = 2;
consider y1,y2 being object such that
A11: y1 <> y2 & Y9 = {y1,y2} by A10, CARD_2:60;
y1 in Y9 & y2 in Y9 by A11, TARSKI:def 2;
then A12: y1 in rng g & y2 in rng g by A1;
then consider x1 being object such that
A13: x1 in dom g & g.x1 = y1 by FUNCT_1:def 3;
consider x2 being object such that
A14: x2 in dom g & g.x2 = y2 by A12, FUNCT_1:def 3;
A15: x1 <> x2 by A11, A13, A14;
reconsider X9 = {x1,x2} as Subset of X by A1, A13, A14, ZFMISC_1:32;
card X9 = 2 by A15, CARD_2:57;
then A16: X9 in 2Set X;
per cases by TARSKI:def 2;
suppose A17: E1(X9) = x1;
then X9\{E1(X9)} = {x2} by A15, ZFMISC_1:17;
then A18: E2(X9) = x2 by TARSKI:def 1;
f.X9 = {g.E1(In(X9,bool X)),g.E2(In(X9,bool X))} by A2, A16
.= y by A10, A11, A13, A14, A17, A18;
hence y in rng f by A2, A16, FUNCT_1:3;
end;
suppose A19: E1(X9) = x2;
then X9\{E1(X9)} = {x1} by A15, ZFMISC_1:17;
then A20: E2(X9) = x1 by TARSKI:def 1;
f.X9 = {g.E1(In(X9,bool X)),g.E2(In(X9,bool X))} by A2, A16
.= y by A10, A11, A13, A14, A19, A20;
hence y in rng f by A2, A16, FUNCT_1:3;
end;
end;
then A21: rng f = 2Set Y by TARSKI:2;
:: show one-to-one property
now
let x1,x2 be object;
assume A22: x1 in dom f & x2 in dom f & f.x1 = f.x2;
then consider X1 being Subset of X such that
A23: x1 = X1 & card X1 = 2 by A2;
consider X2 being Subset of X such that
A24: x2 = X2 & card X2 = 2 by A2, A22;
A25: f.x1 = {g.E1(In(X1,bool X)),g.E2(In(X1,bool X))} by A2, A22, A23
.= {g.E1(X1),g.E2(X1)};
A26: f.x2 = {g.E1(In(X2,bool X)),g.E2(In(X2,bool X))} by A2, A22, A24
.= {g.E1(X2),g.E2(X2)};
X1 is non trivial
proof
assume A27: X1 is trivial;
per cases;
suppose X1 is empty;
hence contradiction by A23;
end;
suppose X1 is non empty;
then card X1 = 1 by A27, CARD_1:def 7;
hence contradiction by A23;
end;
end;
then X1 <> {} & X1\{E1(X1)} <> {} by ZFMISC_1:139;
then A28: E1(X1) in X1 & E2(X1) in X1\{E1(X1)};
then E2(X1) in X1 & not E2(X1) in {E1(X1)} by XBOOLE_0:def 5;
then A29: E2(X1) in X1 & E2(X1) <> E1(X1) by TARSKI:def 1;
A30: E1(X1) in X & E2(X1) in X by A28;
X2 is non trivial
proof
assume A31: X2 is trivial;
per cases;
suppose X2 is empty;
hence contradiction by A24;
end;
suppose X2 is non empty;
then card X2 = 1 by A31, CARD_1:def 7;
hence contradiction by A24;
end;
end;
then X2 <> {} & X2\{E1(X2)} <> {} by ZFMISC_1:139;
then A32: E1(X2) in X2 & E2(X2) in X2\{E1(X2)};
then E2(X2) in X2 & not E2(X2) in {E1(X2)} by XBOOLE_0:def 5;
then A33: E2(X2) in X2 & E2(X2) <> E1(X2) by TARSKI:def 1;
A34: E1(X2) in X & E2(X2) in X by A32;
A35: X1 is finite & X2 is finite by A23, A24;
{E1(X1),E2(X1)} c= X1 & card {E1(X1),E2(X1)} = 2
by A29, ZFMISC_1:32, CARD_2:57;
then A36: {E1(X1),E2(X1)} = X1 by A23, A35, CARD_2:102;
{E1(X2),E2(X2)} c= X2 & card {E1(X2),E2(X2)} = 2
by A33, ZFMISC_1:32, CARD_2:57;
then A37: {E1(X2),E2(X2)} = X2 by A24, A35, CARD_2:102;
A38: f.x1 in rng f & f.x2 in rng f by A22, FUNCT_1:3;
then consider Y1 being Subset of Y such that
A39: f.x1 = Y1 & card Y1 = 2 by A21;
consider Y2 being Subset of Y such that
A40: f.x2 = Y2 & card Y2 = 2 by A21, A38;
A41: g.E1(X1) <> g.E2(X1)
proof
assume g.E1(X1) = g.E2(X1);
then f.x1 = {g.E1(X1)} by A25, ENUMSET1:29;
hence contradiction by A39, CARD_1:30;
end;
A42: g.E1(X2) <> g.E2(X2)
proof
assume g.E1(X2) = g.E2(X2);
then f.x2 = {g.E1(X2)} by A26, ENUMSET1:29;
hence contradiction by A40, CARD_1:30;
end;
A43: {g.E1(X1),g.E2(X1)} = {g.E1(X2),g.E2(X2)} by A22, A25, A26;
then per cases by ZFMISC_1:6;
suppose A44: g.E1(X1) = g.E1(X2);
then A45: E1(X1) = E1(X2) by A1, A30, A34, FUNCT_1:def 4;
{g.E1(X1),g.E2(X1)} \ {g.E1(X1)} = {g.E2(X1)} by A41, ZFMISC_1:17;
then {g.E2(X1)} = {g.E2(X2)} by A42, A43, A44, ZFMISC_1:17;
then E2(X1) = E2(X2) by A1, A28, A32, FUNCT_1:def 4, ZFMISC_1:3;
hence x1 = x2 by A23, A24, A36, A37, A45;
end;
suppose A46: g.E1(X1) = g.E2(X2);
then A47: E1(X1) = E2(X2) by A1, A28, A32, FUNCT_1:def 4;
{g.E1(X1),g.E2(X1)} \ {g.E1(X1)} = {g.E2(X1)} by A41, ZFMISC_1:17;
then {g.E2(X1)} = {g.E1(X2)} by A42, A43, A46, ZFMISC_1:17;
then E2(X1) = E1(X2) by A1, A28, A32, FUNCT_1:def 4, ZFMISC_1:3;
hence x1 = x2 by A23, A24, A36, A37, A47;
end;
end;
hence thesis by A2, A21, FUNCT_1:def 4, CARD_1:70;
end;
:: into MATRIX13 ?
theorem
for X being finite set holds card 2Set X = (card X) choose 2
proof
let X be finite set;
card card X = card Seg card X by FINSEQ_1:55;
then card 2Set X = card 2Set Seg card X by Th23;
hence thesis by MATRIX13:10;
end;
begin :: into GLIB_000
::$CT 23
begin :: into GLIB_002
theorem
for G being _Graph, C being Component of G
for v1 being Vertex of G, v2 being Vertex of C st v1 = v2 holds
v1.edgesIn() = v2.edgesIn() & v1.inDegree() = v2.inDegree() &
v1.edgesOut() = v2.edgesOut() & v1.outDegree() = v2.outDegree() &
v1.edgesInOut() = v2.edgesInOut() & v1.degree() = v2.degree()
proof
let G be _Graph, C be Component of G;
let v1 be Vertex of G, v2 be Vertex of C;
assume A1: v1 = v2;
then A2: v2.edgesIn() c= v1.edgesIn() & v2.edgesOut() c= v1.edgesOut()
by GLIB_000:78;
now
let e be object;
assume e in v1.edgesIn();
then consider x being set such that
A3: e DJoins x,v1,G by GLIB_000:57;
set W = G.walkOf(v1,e,x);
A4: e Joins v1,x,G by A3, GLIB_000:16;
then W is_Walk_from v1,x by GLIB_001:15;
then A5: x in G.reachableFrom(v1) by GLIB_002:def 5;
A6: e Joins v2,x,G & e DJoins x,v2,G by A1, A3, A4;
the_Vertices_of C = G.reachableFrom(v1) by A1, GLIB_002:33;
then e in G.edgesBetween(the_Vertices_of C) by A5, A6, GLIB_000:32;
then e in the_Edges_of C by GLIB_002:31;
then e DJoins x,v2,C & e is set by A6, GLIB_000:73;
hence e in v2.edgesIn() by GLIB_000:57;
end;
then v1.edgesIn() c= v2.edgesIn() by TARSKI:def 3;
hence A7: v1.edgesIn() = v2.edgesIn() by A2, XBOOLE_0:def 10;
hence A8: v1.inDegree() = v2.inDegree();
now
let e be object;
assume e in v1.edgesOut();
then consider x being set such that
A9: e DJoins v1,x,G by GLIB_000:59;
set W = G.walkOf(v1,e,x);
A10: e Joins v1,x,G by A9, GLIB_000:16;
then W is_Walk_from v1,x by GLIB_001:15;
then A11: x in G.reachableFrom(v1) by GLIB_002:def 5;
A12: e Joins v2,x,G & e DJoins v2,x,G by A1, A9, A10;
the_Vertices_of C = G.reachableFrom(v1) by A1, GLIB_002:33;
then e in G.edgesBetween(the_Vertices_of C) by A11, A12, GLIB_000:32;
then e in the_Edges_of C by GLIB_002:31;
then e DJoins v2,x,C & e is set by A12, GLIB_000:73;
hence e in v2.edgesOut() by GLIB_000:59;
end;
then v1.edgesOut() c= v2.edgesOut() by TARSKI:def 3;
hence A13: v1.edgesOut() = v2.edgesOut() by A2, XBOOLE_0:def 10;
hence A14: v1.outDegree() = v2.outDegree();
thus v1.edgesInOut() = v2.edgesInOut() by A7, A13;
thus v1.degree() = v2.degree() by A8, A14;
end;
begin :: into GLIB_006
theorem
for G2 being _Graph, V being set, G1 being addVertices of G2, V
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds
v1.edgesIn() = v2.edgesIn() & v1.inDegree() = v2.inDegree() &
v1.edgesOut() = v2.edgesOut() & v1.outDegree() = v2.outDegree() &
v1.edgesInOut() = v2.edgesInOut() & v1.degree() = v2.degree()
proof
let G2 be _Graph, V be set, G1 be addVertices of G2, V;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2;
A2: G2 is Subgraph of G1 by GLIB_006:57;
then A3: v2.edgesIn() c= v1.edgesIn() by A1, GLIB_000:78;
now
let e be object;
assume e in v1.edgesIn();
then consider x being set such that
A4: e DJoins x,v1,G1 by GLIB_000:57;
e DJoins x,v2,G2 & e is set by A1, A4, GLIB_006:85, TARSKI:1;
hence e in v2.edgesIn() by GLIB_000:57;
end;
then v1.edgesIn() c= v2.edgesIn() by TARSKI:def 3;
hence A5: v1.edgesIn() = v2.edgesIn() by A3, XBOOLE_0:def 10;
hence A6: v1.inDegree() = v2.inDegree();
A7: v2.edgesOut() c= v1.edgesOut() by A1, A2, GLIB_000:78;
now
let e be object;
assume e in v1.edgesOut();
then consider x being set such that
A8: e DJoins v1,x,G1 by GLIB_000:59;
e DJoins v2,x,G2 & e is set by A1, A8, GLIB_006:85, TARSKI:1;
hence e in v2.edgesOut() by GLIB_000:59;
end;
then v1.edgesOut() c= v2.edgesOut() by TARSKI:def 3;
hence A9: v1.edgesOut() = v2.edgesOut() by A7, XBOOLE_0:def 10;
hence A10: v1.outDegree() = v2.outDegree();
thus v1.edgesInOut() = v2.edgesInOut() by A5, A9;
thus v1.degree() = v2.degree() by A6, A10;
end;
theorem
for G2 being _Graph, v,w,e being object, G1 being addEdge of G2,v,e,w
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & v2 <> v & v2 <> w holds
v1.edgesIn() = v2.edgesIn() & v1.inDegree() = v2.inDegree() &
v1.edgesOut() = v2.edgesOut() & v1.outDegree() = v2.outDegree() &
v1.edgesInOut() = v2.edgesInOut() & v1.degree() = v2.degree()
proof
let G2 be _Graph, v,w,e be object, G1 be addEdge of G2,v,e,w;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2 & v2 <> v & v2 <> w;
per cases;
suppose A2: v in the_Vertices_of G2 & w in the_Vertices_of G2 &
not e in the_Edges_of G2;
A3: G2 is Subgraph of G1 by GLIB_006:57;
A4: v2.edgesIn() c= v1.edgesIn() by A1, A3, GLIB_000:78;
now
let f be object;
assume f in v1.edgesIn();
then consider x being set such that
A5: f DJoins x,v1,G1 by GLIB_000:57;
f in the_Edges_of G2
proof
assume A7: not f in the_Edges_of G2;
f Joins x,v1,G1 by A5, GLIB_000:16;
hence contradiction by A1, A2, A7, GLIB_006:107;
end;
hence f in v2.edgesIn() by A1, A5, GLIB_006:71, GLIB_000:57;
end;
then v1.edgesIn() c= v2.edgesIn() by TARSKI:def 3;
hence A8: v1.edgesIn() = v2.edgesIn() by A4, XBOOLE_0:def 10;
hence v1.inDegree() = v2.inDegree();
A9: v2.edgesOut() c= v1.edgesOut() by A1, A3, GLIB_000:78;
now
let f be object;
assume f in v1.edgesOut();
then consider x being set such that
A10: f DJoins v1,x,G1 by GLIB_000:59;
f in the_Edges_of G2
proof
assume A12: not f in the_Edges_of G2;
f Joins x,v1,G1 by A10, GLIB_000:16;
hence contradiction by A1, A2, A12, GLIB_006:107;
end;
hence f in v2.edgesOut() by A1, A10, GLIB_006:71, GLIB_000:59;
end;
then v1.edgesOut() c= v2.edgesOut() by TARSKI:def 3;
hence A13: v1.edgesOut() = v2.edgesOut() by A9, XBOOLE_0:def 10;
hence v1.outDegree() = v2.outDegree();
thus thesis by A8, A13;
end;
suppose 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 11;
hence thesis by A1, GLIB_000:96;
end;
end;
theorem
for G2 being _Graph, v,w being Vertex of G2, e being object
for G1 being addEdge of G2,v,e,w for v1 being Vertex of G1
st not e in the_Edges_of G2 & v1 = v & v <> w holds
v1.edgesIn() = v.edgesIn() & v1.inDegree() = v.inDegree() &
v1.edgesOut() = v.edgesOut() \/ {e} & v1.outDegree() = v.outDegree() +` 1 &
v1.edgesInOut() = v.edgesInOut() \/ {e} & v1.degree() = v.degree() +` 1
proof
let G2 be _Graph, v,w be Vertex of G2, e be object;
let G1 be addEdge of G2,v,e,w, v1 be Vertex of G1;
assume A1: not e in the_Edges_of G2 & v1 = v & v <> w;
A2: G2 is Subgraph of G1 by GLIB_006:57;
A3: v.edgesIn() c= v1.edgesIn() by A1, A2, GLIB_000:78;
now
let f be object;
assume f in v1.edgesIn();
then consider x being set such that
A4: f DJoins x,v1,G1 by GLIB_000:57;
f in the_Edges_of G2
proof
assume A6: not f in the_Edges_of G2;
f Joins x,v1,G1 by A4, GLIB_000:16;
then f = e by A1, A6, GLIB_006:106;
then f DJoins v,w,G1 by A1, GLIB_006:105;
hence contradiction by A1, A4, GLIB_000:125;
end;
hence f in v.edgesIn() by A1, A4, GLIB_006:71, GLIB_000:57;
end;
then v1.edgesIn() c= v.edgesIn() by TARSKI:def 3;
hence A7: v1.edgesIn() = v.edgesIn() by A3, XBOOLE_0:def 10;
hence A8: v1.inDegree() = v.inDegree();
now
let f be object;
thus f in v1.edgesOut() implies f in v.edgesOut() \/ {e}
proof
assume f in v1.edgesOut();
then consider x being set such that
A9: f DJoins v1,x,G1 by GLIB_000:59;
per cases by A9, GLIB_006:71;
suppose A10: f DJoins v1,x,G2;
f is set by TARSKI:1;
then f in v.edgesOut() by A1, A10, GLIB_000:59;
hence thesis by XBOOLE_0:def 3;
end;
suppose A11: not f in the_Edges_of G2;
f Joins x,v1,G1 by A9, GLIB_000:16;
then f = e by A1, A11, GLIB_006:106;
then f in {e} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
end;
assume f in v.edgesOut() \/ {e};
then per cases by XBOOLE_0:def 3;
suppose f in v.edgesOut();
hence f in v1.edgesOut() by A1, A2, GLIB_000:78, TARSKI:def 3;
end;
suppose f in {e};
then f = e & f is set by TARSKI:def 1;
hence f in v1.edgesOut() by A1, GLIB_000:59, GLIB_006:105;
end;
end;
hence A12: v1.edgesOut() = v.edgesOut() \/ {e} by TARSKI:2;
not e in v.edgesOut() by A1;
then A13: v.edgesOut() misses {e} by ZFMISC_1:50;
thus A14: v1.outDegree() = card v.edgesOut() +` card {e} by A12, A13
, CARD_2:35
.= v.outDegree() +` 1 by CARD_1:30;
thus v1.edgesInOut() = v.edgesInOut() \/ {e} by A7, A12, XBOOLE_1:4;
thus v1.degree() = v.degree() +` 1 by A8, A14, CARD_2:19;
end;
theorem
for G2 being _Graph, v,w being Vertex of G2, e being object
for G1 being addEdge of G2,v,e,w for w1 being Vertex of G1
st not e in the_Edges_of G2 & w1 = w & v <> w holds
w1.edgesIn() = w.edgesIn() \/ {e} & w1.inDegree() = w.inDegree() +` 1 &
w1.edgesOut() = w.edgesOut() & w1.outDegree() = w.outDegree() &
w1.edgesInOut() = w.edgesInOut() \/ {e} & w1.degree() = w.degree() +` 1
proof
let G2 be _Graph, v,w be Vertex of G2, e be object;
let G1 be addEdge of G2,v,e,w, w1 be Vertex of G1;
assume A1: not e in the_Edges_of G2 & w1 = w & v <> w;
A2: G2 is Subgraph of G1 by GLIB_006:57;
now
let f be object;
thus f in w1.edgesIn() implies f in w.edgesIn() \/ {e}
proof
assume f in w1.edgesIn();
then consider x being set such that
A3: f DJoins x,w1,G1 by GLIB_000:57;
per cases by A3, GLIB_006:71;
suppose A4: f DJoins x,w1,G2;
f is set by TARSKI:1;
then f in w.edgesIn() by A1, A4, GLIB_000:57;
hence thesis by XBOOLE_0:def 3;
end;
suppose A5: not f in the_Edges_of G2;
f Joins x,w1,G1 by A3, GLIB_000:16;
then f = e by A1, A5, GLIB_006:106;
then f in {e} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
end;
assume f in w.edgesIn() \/ {e};
then per cases by XBOOLE_0:def 3;
suppose f in w.edgesIn();
hence f in w1.edgesIn() by A1, A2, GLIB_000:78, TARSKI:def 3;
end;
suppose f in {e};
then f = e by TARSKI:def 1;
then A6: f DJoins v,w,G1 by A1, GLIB_006:105;
f is set by TARSKI:1;
hence f in w1.edgesIn() by A1, A6, GLIB_000:57;
end;
end;
hence A7: w1.edgesIn() = w.edgesIn() \/ {e} by TARSKI:2;
not e in w.edgesIn() by A1;
then A8: w.edgesIn() misses {e} by ZFMISC_1:50;
thus A9: w1.inDegree() = card w.edgesIn() +` card {e} by A7, A8, CARD_2:35
.= w.inDegree() +` 1 by CARD_1:30;
A10: w.edgesOut() c= w1.edgesOut() by A1, A2, GLIB_000:78;
now
let f be object;
assume f in w1.edgesOut();
then consider x being set such that
A11: f DJoins w1,x,G1 by GLIB_000:59;
f in the_Edges_of G2
proof
assume A13: not f in the_Edges_of G2;
f Joins x,w1,G1 by A11, GLIB_000:16;
then f = e by A1, A13, GLIB_006:106;
then f DJoins v,w,G1 by A1, GLIB_006:105;
hence contradiction by A1, A11, GLIB_000:125;
end;
hence f in w.edgesOut() by A1, A11, GLIB_000:59, GLIB_006:71;
end;
then w1.edgesOut() c= w.edgesOut() by TARSKI:def 3;
hence A14: w1.edgesOut() = w.edgesOut() by A10, XBOOLE_0:def 10;
hence A15: w1.outDegree() = w.outDegree();
thus w1.edgesInOut() = w.edgesInOut() \/ {e} by A7, A14, XBOOLE_1:4;
thus w1.degree() = w.degree() +` 1 by A9, A15, CARD_2:19;
end;
theorem
for G2 being _Graph, v being Vertex of G2, e being object
for G1 being addEdge of G2,v,e,v for v1 being Vertex of G1
st not e in the_Edges_of G2 & v1 = v holds
v1.edgesIn() = v.edgesIn() \/ {e} & v1.inDegree() = v.inDegree() +` 1 &
v1.edgesOut() = v.edgesOut() \/ {e} & v1.outDegree() = v.outDegree() +` 1 &
v1.edgesInOut() = v.edgesInOut() \/ {e} & v1.degree() = v.degree() +` 2
proof
let G2 be _Graph, v be Vertex of G2, e be object;
let G1 be addEdge of G2,v,e,v, v1 be Vertex of G1;
assume A1: not e in the_Edges_of G2 & v1 = v;
A2: G2 is Subgraph of G1 by GLIB_006:57;
now
let f be object;
thus f in v1.edgesIn() implies f in v.edgesIn() \/ {e}
proof
assume f in v1.edgesIn();
then consider x being set such that
A3: f DJoins x,v1,G1 by GLIB_000:57;
per cases by A3, GLIB_006:71;
suppose A4: f DJoins x,v1,G2;
f is set by TARSKI:1;
then f in v.edgesIn() by A1, A4, GLIB_000:57;
hence thesis by XBOOLE_0:def 3;
end;
suppose A5: not f in the_Edges_of G2;
f Joins x,v1,G1 by A3, GLIB_000:16;
then f = e by A1, A5, GLIB_006:106;
then f in {e} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
end;
assume f in v.edgesIn() \/ {e};
then per cases by XBOOLE_0:def 3;
suppose f in v.edgesIn();
hence f in v1.edgesIn() by A1, A2, GLIB_000:78, TARSKI:def 3;
end;
suppose f in {e};
then f = e & f is set by TARSKI:def 1;
hence f in v1.edgesIn() by A1, GLIB_000:57, GLIB_006:105;
end;
end;
hence A6: v1.edgesIn() = v.edgesIn() \/ {e} by TARSKI:2;
not e in v.edgesIn() by A1;
then A7: v.edgesIn() misses {e} by ZFMISC_1:50;
thus A8: v1.inDegree() = card v.edgesIn() +` card {e} by A6, A7, CARD_2:35
.= v.inDegree() +` 1 by CARD_1:30;
now
let f be object;
thus f in v1.edgesOut() implies f in v.edgesOut() \/ {e}
proof
assume f in v1.edgesOut();
then consider x being set such that
A9: f DJoins v1,x,G1 by GLIB_000:59;
per cases by A9, GLIB_006:71;
suppose A10: f DJoins v1,x,G2;
f is set by TARSKI:1;
then f in v.edgesOut() by A1, A10, GLIB_000:59;
hence thesis by XBOOLE_0:def 3;
end;
suppose A11: not f in the_Edges_of G2;
f Joins x,v1,G1 by A9, GLIB_000:16;
then f = e by A1, A11, GLIB_006:106;
then f in {e} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
end;
assume f in v.edgesOut() \/ {e};
then per cases by XBOOLE_0:def 3;
suppose f in v.edgesOut();
hence f in v1.edgesOut() by A1, A2, GLIB_000:78, TARSKI:def 3;
end;
suppose f in {e};
then f = e & f is set by TARSKI:def 1;
hence f in v1.edgesOut() by A1, GLIB_000:59, GLIB_006:105;
end;
end;
hence A12: v1.edgesOut() = v.edgesOut() \/ {e} by TARSKI:2;
not e in v.edgesOut() by A1;
then A13: v.edgesOut() misses {e} by ZFMISC_1:50;
thus A14: v1.outDegree() = card v.edgesOut() +` card {e} by A12, A13
, CARD_2:35
.= v.outDegree() +` 1 by CARD_1:30;
thus v1.edgesInOut() = v.edgesInOut() \/ {e} by A6, A12, XBOOLE_1:5;
thus v1.degree()
= ((v.inDegree() +` 1) +` v.outDegree() +` 1) by A8, A14, CARD_2:19
.= (v.inDegree() +` v.outDegree()) +` 1 +` 1 by CARD_2:19
.= v.degree() +` (1 +` 1) by CARD_2:19
.= v.degree() +` 2;
end;
begin :: into GLIB_007
theorem
for G3 being _Graph, E being set, G4 being reverseEdgeDirections of G3, E
for G1 being Supergraph of G3, G2 being reverseEdgeDirections of G1, E
st E c= the_Edges_of G3 holds G2 is Supergraph of G4
proof
let G3 be _Graph, E be set, G4 be reverseEdgeDirections of G3, E;
let G1 be Supergraph of G3, G2 be reverseEdgeDirections of G1, E;
assume A1: E c= the_Edges_of G3;
the_Edges_of G3 c= the_Edges_of G1 by GLIB_006:def 9;
then A2: E c= the_Edges_of G1 by A1, XBOOLE_1:1;
now
the_Vertices_of G2 = the_Vertices_of G1 &
the_Vertices_of G3 = the_Vertices_of G4 by GLIB_007:4;
hence the_Vertices_of G4 c= the_Vertices_of G2 by GLIB_006:def 9;
the_Edges_of G4 = the_Edges_of G3 & the_Edges_of G2 = the_Edges_of G1
by GLIB_007:4;
hence the_Edges_of G4 c= the_Edges_of G2 by GLIB_006:def 9;
let e be set;
assume A3: e in the_Edges_of G4;
set v4 = (the_Source_of G4).e, w4 = (the_Target_of G4).e;
per cases;
suppose A4: e in E;
e DJoins v4,w4,G4 by A3, GLIB_000:def 14;
then e DJoins w4,v4,G3 by A1, A4, GLIB_007:7;
then e DJoins w4,v4,G1 by GLIB_006:70;
then e DJoins v4,w4,G2 by A2, A4, GLIB_007:7;
hence (the_Source_of G4).e = (the_Source_of G2).e &
(the_Target_of G4).e = (the_Target_of G2).e by GLIB_000:def 14;
end;
suppose A5: not e in E;
e DJoins v4,w4,G4 by A3, GLIB_000:def 14;
then e DJoins v4,w4,G3 by A1, A5, GLIB_007:8;
then e DJoins v4,w4,G1 by GLIB_006:70;
then e DJoins v4,w4,G2 by A2, A5, GLIB_007:8;
hence (the_Source_of G4).e = (the_Source_of G2).e &
(the_Target_of G4).e = (the_Target_of G2).e by GLIB_000:def 14;
end;
end;
hence G2 is Supergraph of G4 by GLIB_006:def 9;
end;
:: counterpart of GLIB_007:55
theorem
for G2 being _Graph, v being object, G1 being addVertex of G2, v
holds G1 is addAdjVertexAll of G2,v,{}
proof
let G2 be _Graph, v be object, G1 be addVertex of G2, v;
per cases;
suppose A1: not v in the_Vertices_of G2;
A2: {} c= the_Vertices_of G2 by XBOOLE_1:2;
now
thus the_Vertices_of G1 = the_Vertices_of G2 \/ {v} by GLIB_006:def 10;
hereby
let e be object;
not e Joins v,v,G2 by A1, GLIB_000:13;
hence not e Joins v,v,G1 by GLIB_006:87;
let v1 be object;
hereby
assume not v1 in {};
not e Joins v1,v,G2 by A1, GLIB_000:13;
hence not e Joins v1,v,G1 by GLIB_006:87;
end;
let v2 be object;
assume v1 <> v & v2 <> v & e DJoins v1,v2,G1;
hence e DJoins v1,v2,G2 by GLIB_006:85;
end;
take E = {};
thus card {} = card E;
thus E misses the_Edges_of G2 by XBOOLE_1:65;
thus the_Edges_of G1 = the_Edges_of G2 \/ E by GLIB_006:def 10;
let v1 be object;
assume v1 in {};
hence ex e1 being object st e1 in E & e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2;
end;
hence thesis by A1, A2, GLIB_007:def 4;
end;
suppose A3: v in the_Vertices_of G2;
then G1 == G2 by ZFMISC_1:31, GLIB_006:78;
hence thesis by A3, GLIB_007:def 4;
end;
end;
theorem Th58:
for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & E c= the_Edges_of G1 holds
v2.edgesIn() = (v1.edgesIn() \ E) \/ (v1.edgesOut() /\ E) &
v2.edgesOut() = (v1.edgesOut() \ E) \/ (v1.edgesIn() /\ E)
proof
let G1 be _Graph, E be set, G2 be reverseEdgeDirections of G1, E;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2 & E c= the_Edges_of G1;
now
let e be object;
A2: e is set by TARSKI:1;
hereby
assume e in v2.edgesIn();
then consider x being set such that
A3: e DJoins x,v2,G2 by GLIB_000:57;
per cases;
suppose A4: e in E;
then e DJoins v2,x,G1 by A1, A3, GLIB_007:7;
then e in v1.edgesOut() by A1, A2, GLIB_000:59;
then e in v1.edgesOut() /\ E by A4, XBOOLE_0:def 4;
hence e in (v1.edgesIn() \ E)\/(v1.edgesOut() /\ E) by XBOOLE_0:def 3;
end;
suppose A5: not e in E;
then e DJoins x,v2,G1 by A1, A3, GLIB_007:8;
then e in v1.edgesIn() by A1, A2, GLIB_000:57;
then e in v1.edgesIn() \ E by A5, XBOOLE_0:def 5;
hence e in (v1.edgesIn() \ E)\/(v1.edgesOut() /\ E) by XBOOLE_0:def 3;
end;
end;
assume e in (v1.edgesIn() \ E)\/(v1.edgesOut() /\ E);
then per cases by XBOOLE_0:def 3;
suppose e in v1.edgesIn() \ E;
then A6: e in v1.edgesIn() & not e in E by XBOOLE_0:def 5;
then consider x being set such that
A7: e DJoins x,v1,G1 by GLIB_000:57;
e DJoins x,v1,G2 by A1, A6, A7, GLIB_007:8;
hence e in v2.edgesIn() by A1, A2, GLIB_000:57;
end;
suppose e in v1.edgesOut() /\ E;
then A8: e in v1.edgesOut() & e in E by XBOOLE_0:def 4;
then consider x being set such that
A9: e DJoins v1,x,G1 by GLIB_000:59;
e DJoins x,v1,G2 by A1, A8, A9, GLIB_007:7;
hence e in v2.edgesIn() by A1, A2, GLIB_000:57;
end;
end;
hence v2.edgesIn() = (v1.edgesIn() \ E) \/ (v1.edgesOut() /\ E) by TARSKI:2;
now
let e be object;
A10: e is set by TARSKI:1;
hereby
assume e in v2.edgesOut();
then consider x being set such that
A11: e DJoins v2,x,G2 by GLIB_000:59;
per cases;
suppose A12: e in E;
then e DJoins x,v2,G1 by A1, A11, GLIB_007:7;
then e in v1.edgesIn() by A1, A10, GLIB_000:57;
then e in v1.edgesIn() /\ E by A12, XBOOLE_0:def 4;
hence e in (v1.edgesOut() \ E)\/(v1.edgesIn() /\ E) by XBOOLE_0:def 3;
end;
suppose A13: not e in E;
then e DJoins v2,x,G1 by A1, A11, GLIB_007:8;
then e in v1.edgesOut() by A1, A10, GLIB_000:59;
then e in v1.edgesOut() \ E by A13, XBOOLE_0:def 5;
hence e in (v1.edgesOut() \ E)\/(v1.edgesIn() /\ E) by XBOOLE_0:def 3;
end;
end;
assume e in (v1.edgesOut() \ E)\/(v1.edgesIn() /\ E);
then per cases by XBOOLE_0:def 3;
suppose e in v1.edgesOut() \ E;
then A14: e in v1.edgesOut() & not e in E by XBOOLE_0:def 5;
then consider x being set such that
A15: e DJoins v1,x,G1 by GLIB_000:59;
e DJoins v1,x,G2 by A1, A14, A15, GLIB_007:8;
hence e in v2.edgesOut() by A1, A10, GLIB_000:59;
end;
suppose e in v1.edgesIn() /\ E;
then A16: e in v1.edgesIn() & e in E by XBOOLE_0:def 4;
then consider x being set such that
A17: e DJoins x,v1,G1 by GLIB_000:57;
e DJoins v1,x,G2 by A1, A16, A17, GLIB_007:7;
hence e in v2.edgesOut() by A1, A10, GLIB_000:59;
end;
end;
hence v2.edgesOut() = (v1.edgesOut() \ E) \/ (v1.edgesIn() /\ E) by TARSKI:2;
end;
theorem
for G1 being _Graph, G2 being reverseEdgeDirections of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds
v2.edgesIn() = v1.edgesOut() & v2.inDegree() = v1.outDegree() &
v2.edgesOut() = v1.edgesIn() & v2.outDegree() = v1.inDegree()
proof
let G1 be _Graph, G2 be reverseEdgeDirections of G1;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2;
now
let e be object;
hereby
assume A2: e in v2.edgesIn();
A3: e is set by TARSKI:1;
consider x being set such that
A4: e DJoins x,v2,G2 by A2, GLIB_000:57;
e in the_Edges_of G2 by A4, GLIB_000:def 14;
then e in the_Edges_of G1 by GLIB_007:4;
then e DJoins v1,x,G1 by A1, A4, GLIB_007:7;
hence e in v1.edgesOut() by A3, GLIB_000:59;
end;
assume A5: e in v1.edgesOut();
A6: e is set by TARSKI:1;
consider x being set such that
A7: e DJoins v1,x,G1 by A5, GLIB_000:59;
e in the_Edges_of G1 by A7, GLIB_000:def 14;
then e DJoins x,v2,G2 by A1, A7, GLIB_007:7;
hence e in v2.edgesIn() by A6, GLIB_000:57;
end;
hence v2.edgesIn() = v1.edgesOut() by TARSKI:2;
hence v2.inDegree() = v1.outDegree();
now
let e be object;
hereby
assume A8: e in v2.edgesOut();
A9: e is set by TARSKI:1;
consider x being set such that
A10: e DJoins v2,x,G2 by A8, GLIB_000:59;
e in the_Edges_of G2 by A10, GLIB_000:def 14;
then e in the_Edges_of G1 by GLIB_007:4;
then e DJoins x,v1,G1 by A1, A10, GLIB_007:7;
hence e in v1.edgesIn() by A9, GLIB_000:57;
end;
assume A11: e in v1.edgesIn();
A12: e is set by TARSKI:1;
consider x being set such that
A13: e DJoins x,v1,G1 by A11, GLIB_000:57;
e in the_Edges_of G1 by A13, GLIB_000:def 14;
then e DJoins v2,x,G2 by A1, A13, GLIB_007:7;
hence e in v2.edgesOut() by A12, GLIB_000:59;
end;
hence v2.edgesOut() = v1.edgesIn() by TARSKI:2;
hence v2.outDegree() = v1.inDegree();
end;
theorem Th60:
for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds v2.edgesInOut() = v1.edgesInOut() & v2.degree() = v1.degree()
proof
let G1 be _Graph, E be set, G2 be reverseEdgeDirections of G1, E;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2;
per cases;
suppose E c= the_Edges_of G1;
then A2: v2.edgesIn() = (v1.edgesIn() \ E) \/ (v1.edgesOut() /\ E) &
v2.edgesOut() = (v1.edgesOut() \ E) \/ (v1.edgesIn() /\ E) by A1, Th58;
:: just sorting the unions
thus v2.edgesInOut()
= (v1.edgesIn() \ E) \/ (v1.edgesOut() /\ E) \/
(v1.edgesIn() /\ E) \/ (v1.edgesOut() \ E) by A2, XBOOLE_1:4
.= (v1.edgesIn() \ E) \/ (v1.edgesIn() /\ E) \/
(v1.edgesOut() /\ E) \/ (v1.edgesOut() \ E) by XBOOLE_1:4
.= v1.edgesIn() \/ (v1.edgesOut() /\ E) \/ (v1.edgesOut() \ E)
by XBOOLE_1:51
.= v1.edgesIn() \/ ((v1.edgesOut() /\ E) \/ (v1.edgesOut() \ E))
by XBOOLE_1:4
.= v1.edgesInOut() by XBOOLE_1:51;
:: sorting the summands in a similar fashion
thus v2.degree()
= card(v1.edgesIn()\E) +` card(v1.edgesOut()/\E) +`
card((v1.edgesOut() \ E) \/ (v1.edgesIn() /\ E)) by A2, Th2, CARD_2:35
.= card(v1.edgesIn()\E) +` card(v1.edgesOut()/\E) +`
(card(v1.edgesOut()\E) +` card(v1.edgesIn()/\E)) by Th2, CARD_2:35
.= card(v1.edgesIn()\E) +` card(v1.edgesOut()/\E) +`
card(v1.edgesIn()/\E) +` card(v1.edgesOut()\E) by CARD_2:19
.= card(v1.edgesIn()\E) +` card(v1.edgesIn()/\E) +`
card(v1.edgesOut()/\E) +` card(v1.edgesOut()\E) by CARD_2:19
.= card((v1.edgesIn()\E) \/ (v1.edgesIn()/\E)) +`
card(v1.edgesOut()/\E) +` card(v1.edgesOut()\E) by Th2, CARD_2:35
.= v1.inDegree() +` card(v1.edgesOut()/\E) +` card(v1.edgesOut()\E)
by XBOOLE_1:51
.= v1.inDegree() +` (card(v1.edgesOut()/\E) +` card(v1.edgesOut()\E))
by CARD_2:19
.= v1.inDegree() +` card((v1.edgesOut()/\E) \/ (v1.edgesOut()\E))
by Th2, CARD_2:35
.= v1.degree() by XBOOLE_1:51;
end;
suppose not E c= the_Edges_of G1;
then G1 == G2 by GLIB_007:def 1;
hence thesis by A1, GLIB_000:96;
end;
end;
theorem
for G2 being _Graph, v being object, V being set
for G1 being addAdjVertexAll of G2, v, V, w being Vertex of G1
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v = w
holds w.allNeighbors() = V & w.degree() = card V
proof
let G2 be _Graph, v be object, V be set;
let G1 be addAdjVertexAll of G2,v,V, w be Vertex of G1;
assume A1: V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v = w;
then consider E being set such that
A2: card V = card E & E misses the_Edges_of G2 and
A3: the_Edges_of G1 = the_Edges_of G2 \/ E and
A4: for v1 being object st v1 in V ex e1 being object st e1 in E &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2 by GLIB_007:def 4;
now
let x be object;
hereby
assume x in w.allNeighbors();
then consider e being object such that
A5: e Joins w,x,G1 by GLIB_000:71;
not e in the_Edges_of G2
proof
assume e in the_Edges_of G2;
then e Joins w,x,G2 by A5, GLIB_006:72;
hence contradiction by A1, GLIB_000:13;
end;
then w = v & x in V or x = v & w in V by A1, A2, A3, A5, GLIB_007:51;
hence x in V by A1;
end;
assume x in V;
then consider e1 being object such that
A6: e1 in E & e1 Joins x,v,G1 and
for e2 being object st e2 Joins x,v,G1 holds e1 = e2 by A4;
x is set by TARSKI:1;
hence x in w.allNeighbors() by A1, A6, GLIB_000:14, GLIB_000:71;
end;
hence w.allNeighbors() = V by TARSKI:2;
per cases;
suppose A7: V <> {};
V c= V;
then consider f being Function of V, G1.edgesBetween(V,{v}) such that
A8: f is one-to-one onto and
A9: for u being object st u in V holds f.u Joins u,v,G1
by A1, GLIB_007:57;
A10: rng f = G1.edgesBetween(V,{w}) by A1, A8, FUNCT_2:def 3;
the_Vertices_of G2 c= the_Vertices_of G1 by GLIB_006:def 9;
then V c= the_Vertices_of G1 by A1, XBOOLE_1:1;
then A11: G1.edgesBetween(V,{w})c= G1.edgesBetween(the_Vertices_of G1,{w})
by GLIB_000:37;
now
let e be object;
assume e in G1.edgesBetween(the_Vertices_of G1,{w});
then A12: e SJoins the_Vertices_of G1,{w},G1 by GLIB_000:def 30;
ex u being object st e Joins u,w,G1
proof
per cases by A12, GLIB_000:def 15;
suppose A13: (the_Source_of G1).e in the_Vertices_of G1 &
(the_Target_of G1).e in {w};
take (the_Source_of G1).e;
A14: (the_Target_of G1).e = w by A13, TARSKI:def 1;
e in the_Edges_of G1 by A12, GLIB_000:def 15;
hence e Joins (the_Source_of G1).e,w,G1 by A14, GLIB_000:def 13;
end;
suppose A15: (the_Target_of G1).e in the_Vertices_of G1 &
(the_Source_of G1).e in {w};
take (the_Target_of G1).e;
A16: (the_Source_of G1).e = w by A15, TARSKI:def 1;
e in the_Edges_of G1 by A12, GLIB_000:def 15;
hence e Joins (the_Target_of G1).e,w,G1 by A16, GLIB_000:def 13;
end;
end;
then consider u being object such that
A17: e Joins u,w,G1;
u in V & w in {w} by A1, A17, GLIB_007:def 4, TARSKI:def 1;
then e SJoins V,{w},G1 by A17, GLIB_000:17;
hence e in G1.edgesBetween(V,{w}) by GLIB_000:def 30;
end;
then G1.edgesBetween(the_Vertices_of G1,{w}) c= G1.edgesBetween(V,{w})
by TARSKI:def 3;
then G1.edgesBetween(V,{w}) = G1.edgesBetween(the_Vertices_of G1,{w})
by A11, XBOOLE_0:def 10;
then A18: rng f = w.edgesInOut() by A10, GLIB_000:151;
set u = the Element of V;
A19: u in V & v in {v} by A7, TARSKI:def 1;
then f.u Joins u,v,G1 by A9;
then f.u SJoins V,{v},G1 by A19, GLIB_000:17;
then f.u in G1.edgesBetween(V,{v}) by GLIB_000:def 30;
then dom f = V by FUNCT_2:def 1;
then A20: card V = card w.edgesInOut() by A8, A18, CARD_1:70;
for e being object holds not e Joins w,w,G1 by A1, GLIB_007:def 4;
hence w.degree() = card V by A20, GLIB_000:154;
end;
suppose A21: V = {};
then A22: G1 is addVertex of G2, v by GLIB_007:55;
{w} \ the_Vertices_of G2 = {w} by A1, ZFMISC_1:59;
then w in {v} \ the_Vertices_of G2 by A1, TARSKI:def 1;
hence w.degree() = card V by A21, A22, GLIB_000:157, GLIB_006:88;
end;
end;
theorem Th62:
for G2 being _Graph, v being object, V being set
for G1 being addAdjVertexAll of G2, v, V
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & not v2 in V holds
v1.edgesIn() = v2.edgesIn() & v1.inDegree() = v2.inDegree() &
v1.edgesOut() = v2.edgesOut() & v1.outDegree() = v2.outDegree() &
v1.edgesInOut() = v2.edgesInOut() & v1.degree() = v2.degree()
proof
let G2 be _Graph, v be object, V be set;
let G1 be addAdjVertexAll of G2,v,V;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2 & not v2 in V;
per cases;
suppose A2: V c= the_Vertices_of G2 & not v in the_Vertices_of G2;
A3: G2 is Subgraph of G1 by GLIB_006:57;
then A4: v2.edgesIn() c= v1.edgesIn() by A1, GLIB_000:78;
now
let e be object;
A5: e is set by TARSKI:1;
assume e in v1.edgesIn();
then consider x being set such that
A6: e DJoins x,v1,G1 by GLIB_000:57;
A7: x <> v
proof
assume x = v;
then e Joins v1,v,G1 by A6, GLIB_000:16;
hence contradiction by A1, A2, GLIB_007:def 4;
end;
v1 <> v by A1, A2;
then e DJoins x,v1,G2 by A2, A6, A7, GLIB_007:def 4;
hence e in v2.edgesIn() by A1, A5, GLIB_000:57;
end;
then v1.edgesIn() c= v2.edgesIn() by TARSKI:def 3;
hence A8: v1.edgesIn() = v2.edgesIn() by A4, XBOOLE_0:def 10;
hence v1.inDegree() = v2.inDegree();
A9: v2.edgesOut() c= v1.edgesOut() by A1, A3, GLIB_000:78;
now
let e be object;
A10: e is set by TARSKI:1;
assume e in v1.edgesOut();
then consider x being set such that
A11: e DJoins v1,x,G1 by GLIB_000:59;
A12: x <> v
proof
assume x = v;
then e Joins v1,v,G1 by A11, GLIB_000:16;
hence contradiction by A1, A2, GLIB_007:def 4;
end;
v1 <> v by A1, A2;
then e DJoins v1,x,G2 by A2, A11, A12, GLIB_007:def 4;
hence e in v2.edgesOut() by A1, A10, GLIB_000:59;
end;
then v1.edgesOut() c= v2.edgesOut() by TARSKI:def 3;
hence A13: v1.edgesOut() = v2.edgesOut() by A9, XBOOLE_0:def 10;
hence v1.outDegree() = v2.outDegree();
thus thesis by A8, A13;
end;
suppose not(V c= the_Vertices_of G2 & not v in the_Vertices_of G2);
then G1 == G2 by GLIB_007:def 4;
hence thesis by A1, GLIB_000:96;
end;
end;
theorem
for G2 being _Graph, v being object, V being Subset of the_Vertices_of G2
for G1 being addAdjVertexAll of G2, v, V
for v1 being Vertex of G1, v2 being Vertex of G2
st not v in the_Vertices_of G2 & v1 = v2 & v2 in V holds
v1.allNeighbors() = v2.allNeighbors() \/ {v} &
v1.degree() = v2.degree() +` 1
proof
let G2 be _Graph, v be object, V be Subset of the_Vertices_of G2;
let G1 be addAdjVertexAll of G2, v, V;
let v1 be Vertex of G1, v2 be Vertex of G2;
A1: v is set by TARSKI:1;
assume A2: not v in the_Vertices_of G2 & v1 = v2 & v2 in V;
:: first we get the edge that connects v1 and v
A3: G2 is Subgraph of G1 by GLIB_006:57;
then A4: v2.allNeighbors() c= v1.allNeighbors() by A2, GLIB_000:82;
consider E being set such that
A5: card V = card E & E misses the_Edges_of G2 and
the_Edges_of G1 = the_Edges_of G2 \/ E and
A6: for w1 being object st w1 in V ex e1 being object st e1 in E &
e1 Joins w1,v,G1 & for e2 being object
st e2 Joins w1,v,G1 holds e1 = e2 by A2, GLIB_007:def 4;
consider e1 being object such that
A7: e1 in E & e1 Joins v2,v,G1 and
A8: for e2 being object st e2 Joins v2,v,G1 holds e1 = e2 by A2, A6;
e1 Joins v1,v,G1 & v is set by A2, A7, TARSKI:1;
:: we conclude that v is the only new neighbor
then {v} c= v1.allNeighbors() by GLIB_000:71, ZFMISC_1:31;
then A9: v2.allNeighbors() \/ {v} c= v1.allNeighbors() by A4, XBOOLE_1:8;
now
let x be object;
assume x in v1.allNeighbors();
then consider e2 being object such that
A10: e2 Joins v1,x,G1 by GLIB_000:71;
per cases;
suppose x <> v;
then v1 <> v & x <> v by A2;
then e2 Joins v2,x,G2 & x is set by A2, A10, GLIB_007:49, TARSKI:1;
then x in v2.allNeighbors() by GLIB_000:71;
hence x in v2.allNeighbors() \/ {v} by XBOOLE_0:def 3;
end;
suppose x = v;
then x in {v} by TARSKI:def 1;
hence x in v2.allNeighbors() \/ {v} by XBOOLE_0:def 3;
end;
end;
then v1.allNeighbors() c= v2.allNeighbors() \/ {v} by TARSKI:def 3;
hence v1.allNeighbors() = v2.allNeighbors() \/ {v} by A9, XBOOLE_0:def 10;
:: and since e1 is the only new edge, the degree can only increase by 1
A11: v2.edgesOut() c= v1.edgesOut() & v2.edgesIn() c= v1.edgesIn()
by A2, A3, GLIB_000:78;
A12: e1 is set by TARSKI:1;
per cases by A7, GLIB_000:16;
suppose A13: e1 DJoins v2,v,G1;
then {e1} c= v1.edgesOut() by A1, A2, A12, GLIB_000:59, ZFMISC_1:31;
then A14: v2.edgesOut() \/ {e1} c= v1.edgesOut() by A11, XBOOLE_1:8;
now
let e2 be object;
assume e2 in v1.edgesOut();
then consider x being set such that
A15: e2 DJoins v1,x,G1 by GLIB_000:59;
per cases;
suppose x <> v;
then A16: x <> v & v1 <> v & e2 is set by A2, TARSKI:1;
then e2 DJoins v1,x,G2 by A2, A15, GLIB_007:def 4;
then e2 in v2.edgesOut() by A2, A16, GLIB_000:59;
hence e2 in v2.edgesOut() \/ {e1} by XBOOLE_0:def 3;
end;
suppose x = v;
then e2 Joins v2,v,G1 by A2, A15, GLIB_000:16;
then e1 = e2 by A8;
then e2 in {e1} by TARSKI:def 1;
hence e2 in v2.edgesOut() \/ {e1} by XBOOLE_0:def 3;
end;
end;
then v1.edgesOut() c= v2.edgesOut() \/ {e1} by TARSKI:def 3;
then A17: v1.edgesOut() = v2.edgesOut() \/ {e1} by A14, XBOOLE_0:def 10;
now
let e2 be object;
assume e2 in v1.edgesIn();
then consider x being set such that
A18: e2 DJoins x,v1,G1 by GLIB_000:57;
A19: e2 is set & v1 <> v by A2, TARSKI:1;
x <> v
proof
assume A20: x = v;
then e2 Joins v2,v,G1 by A2, A18, GLIB_000:16;
then e1 = e2 by A8;
then x = v1 by A2, A13, A18, GLIB_000:125;
hence contradiction by A2, A20;
end;
then e2 DJoins x,v1,G2 by A2, A18, A19, GLIB_007:def 4;
hence e2 in v2.edgesIn() by A2, A19, GLIB_000:57;
end;
then v1.edgesIn() c= v2.edgesIn() by TARSKI:def 3;
then A21: v1.edgesIn() = v2.edgesIn() by A11, XBOOLE_0:def 10;
not e1 in the_Edges_of G2
proof
assume e1 in the_Edges_of G2;
then e1 in E /\ the_Edges_of G2 by A7, XBOOLE_0:def 4;
hence contradiction by A5, XBOOLE_0:4;
end;
then not e1 in v2.edgesOut();
then A22: {e1} misses v2.edgesOut() by ZFMISC_1:50;
thus v1.degree()
= v2.inDegree() +` (card(v2.edgesOut()) +` card {e1})
by A17, A21, A22, CARD_2:35
.= v2.inDegree() +` (v2.outDegree() +` 1) by CARD_1:30
.= v2.degree() +` 1 by CARD_2:19;
end;
suppose A23: e1 DJoins v,v2,G1;
then {e1} c= v1.edgesIn() by A1, A2, A12, GLIB_000:57, ZFMISC_1:31;
then A24: v2.edgesIn() \/ {e1} c= v1.edgesIn() by A11, XBOOLE_1:8;
now
let e2 be object;
assume e2 in v1.edgesIn();
then consider x being set such that
A25: e2 DJoins x,v1,G1 by GLIB_000:57;
per cases;
suppose x <> v;
then A26: x <> v & v1 <> v & e2 is set by A2, TARSKI:1;
then e2 DJoins x,v1,G2 by A2, A25, GLIB_007:def 4;
then e2 in v2.edgesIn() by A2, A26, GLIB_000:57;
hence e2 in v2.edgesIn() \/ {e1} by XBOOLE_0:def 3;
end;
suppose x = v;
then e2 Joins v2,v,G1 by A2, A25, GLIB_000:16;
then e1 = e2 by A8;
then e2 in {e1} by TARSKI:def 1;
hence e2 in v2.edgesIn() \/ {e1} by XBOOLE_0:def 3;
end;
end;
then v1.edgesIn() c= v2.edgesIn() \/ {e1} by TARSKI:def 3;
then A27: v1.edgesIn() = v2.edgesIn() \/ {e1} by A24, XBOOLE_0:def 10;
now
let e2 be object;
assume e2 in v1.edgesOut();
then consider x being set such that
A28: e2 DJoins v1,x,G1 by GLIB_000:59;
A29: e2 is set & v1 <> v by A2, TARSKI:1;
x <> v
proof
assume A30: x = v;
then e2 Joins v2,v,G1 by A2, A28, GLIB_000:16;
then e1 = e2 by A8;
then x = v1 by A2, A23, A28, GLIB_000:125;
hence contradiction by A2, A30;
end;
then e2 DJoins v1,x,G2 by A2, A28, A29, GLIB_007:def 4;
hence e2 in v2.edgesOut() by A2, A29, GLIB_000:59;
end;
then v1.edgesOut() c= v2.edgesOut() by TARSKI:def 3;
then A31: v1.edgesOut() = v2.edgesOut() by A11, XBOOLE_0:def 10;
not e1 in the_Edges_of G2
proof
assume e1 in the_Edges_of G2;
then e1 in E /\ the_Edges_of G2 by A7, XBOOLE_0:def 4;
hence contradiction by A5, XBOOLE_0:4;
end;
then not e1 in v2.edgesIn();
then A32: {e1} misses v2.edgesIn() by ZFMISC_1:50;
thus v1.degree()
= v2.outDegree() +` (card(v2.edgesIn()) +` card {e1})
by A27, A31, A32, CARD_2:35
.= v2.outDegree() +` (v2.inDegree() +` 1) by CARD_1:30
.= v2.degree() +` 1 by CARD_2:19;
end;
end;
theorem
for G2 being _Graph, v being object, V being set
for G1 being addAdjVertexAll of G2, v, V
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds
v1.degree() c= v2.degree() +` 1 &
v1.inDegree() c= v2.inDegree() +` 1 &
v1.outDegree() c= v2.outDegree() +` 1
proof
let G2 be _Graph, v be object, V be set;
let G1 be addAdjVertexAll of G2, v, V;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2;
per cases;
suppose A2: V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v2 in V;
:: first get the edge connecting v1 and v
then consider E being set such that
A3: card V = card E & E misses the_Edges_of G2 and
the_Edges_of G1 = the_Edges_of G2 \/ E and
A4: for v3 being object st v3 in V ex e1 being object st e1 in E &
e1 Joins v3,v,G1 &
for e2 being object st e2 Joins v3,v,G1 holds e1 = e2
by GLIB_007:def 4;
consider e1 being object such that
A5: e1 in E & e1 Joins v2,v,G1 and
A6: for e2 being object st e2 Joins v2,v,G1 holds e1 = e2 by A2, A4;
A7: v2 <> v by A2;
:: we show that e1 is the only new edge incident with v1
now
let e2 be object;
assume e2 in v1.edgesIn();
then consider x being set such that
A8: e2 DJoins x,v1,G1 by GLIB_000:57;
per cases;
suppose x = v;
then e2 Joins v1,v,G1 by A8, GLIB_000:16;
then e2 = e1 by A1, A6;
then e2 in {e1} by TARSKI:def 1;
hence e2 in v2.edgesIn() \/ {e1} by XBOOLE_0:def 3;
end;
suppose x <> v;
then A9: e2 DJoins x,v1,G2 by A1, A2, A7, A8, GLIB_007:def 4;
e2 is set by TARSKI:1;
then e2 in v2.edgesIn() by A1, A9, GLIB_000:57;
hence e2 in v2.edgesIn() \/ {e1} by XBOOLE_0:def 3;
end;
end;
then A10: v1.edgesIn() c= v2.edgesIn() \/ {e1} by TARSKI:def 3;
now
let e2 be object;
assume e2 in v1.edgesOut();
then consider x being set such that
A11: e2 DJoins v1,x,G1 by GLIB_000:59;
per cases;
suppose x = v;
then e2 Joins v1,v,G1 by A11, GLIB_000:16;
then e2 = e1 by A1, A6;
then e2 in {e1} by TARSKI:def 1;
hence e2 in v2.edgesOut() \/ {e1} by XBOOLE_0:def 3;
end;
suppose x <> v;
then A12: e2 DJoins v1,x,G2 by A1, A2, A7, A11, GLIB_007:def 4;
e2 is set by TARSKI:1;
then e2 in v2.edgesOut() by A1, A12, GLIB_000:59;
hence e2 in v2.edgesOut() \/ {e1} by XBOOLE_0:def 3;
end;
end;
then A13: v1.edgesOut() c= v2.edgesOut() \/ {e1} by TARSKI:def 3;
:: e1 can only be an in edge or an out edge of v1
A14: v1.edgesIn() = v2.edgesIn() or v1.edgesOut() = v2.edgesOut()
proof
assume A15
: v1.edgesIn() <> v2.edgesIn() & v1.edgesOut() <> v2.edgesOut();
G2 is Subgraph of G1 by GLIB_006:57;
then v2.edgesIn() c= v1.edgesIn() & v2.edgesOut() c= v1.edgesOut()
by A1, GLIB_000:78;
then not v1.edgesIn() c= v2.edgesIn() & not v1.edgesOut()c= v2.edgesOut()
by A15, XBOOLE_0:def 10;
then A16: v1.edgesIn()\v2.edgesIn()<>{} & v1.edgesOut()\v2.edgesOut()<>{}
by XBOOLE_1:37;
then consider i being object such that
A17: i in v1.edgesIn()\v2.edgesIn() by XBOOLE_0:def 1;
consider o being object such that
A18: o in v1.edgesOut()\v2.edgesOut() by A16, XBOOLE_0:def 1;
A19: i in v1.edgesIn() & not i in v2.edgesIn() &
o in v1.edgesOut() & not o in v2.edgesOut() by A17, A18
, XBOOLE_0:def 5;
then i in {e1} & o in {e1} by A10, A13, XBOOLE_0:def 3;
then A20: i = e1 & o = e1 by TARSKI:def 1;
then consider j being set such that
A21: e1 DJoins j,v1,G1 by A19, GLIB_000:57;
consider p being set such that
A22: e1 DJoins v1,p,G1 by A19, A20, GLIB_000:59;
j = v1 & v1 = p by A21, A22, GLIB_000:125;
then e1 Joins v1,v1,G1 by A21, GLIB_000:16;
hence contradiction by A1, A5, A7, GLIB_000:15;
end;
{e1} misses the_Edges_of G2 by A3, A5, ZFMISC_1:31, XBOOLE_1:63;
then A23: {e1} misses v2.edgesIn() & {e1} misses v2.edgesOut()
by XBOOLE_1:63;
then A24: card(v2.edgesOut() \/ {e1})
= v2.outDegree() +` card {e1} by CARD_2:35
.= v2.outDegree() +` 1 by CARD_1:30;
A25: card(v2.edgesIn() \/ {e1})
= v2.inDegree() +` card {e1} by A23, CARD_2:35
.= v2.inDegree() +` 1 by CARD_1:30;
thus v1.degree() c= v2.degree() +` 1
proof
per cases by A14;
suppose v1.edgesIn() = v2.edgesIn();
then A26: v1.inDegree() = v2.inDegree();
v1.outDegree() c= v2.outDegree() +` 1 by A13, A24, CARD_1:11;
then v1.degree() c= v2.inDegree() +` (v2.outDegree() +` 1)
by A26, CARD_2:84;
hence thesis by CARD_2:19;
end;
suppose v1.edgesOut() = v2.edgesOut();
then A27: v1.outDegree() = v2.outDegree();
v1.inDegree() c= v2.inDegree() +` 1 by A10, A25, CARD_1:11;
then v1.degree() c= v2.outDegree() +` (v2.inDegree() +` 1)
by A27, CARD_2:84;
hence thesis by CARD_2:19;
end;
end;
thus thesis by A10, A13, A24, A25, CARD_1:11;
end;
suppose not v2 in V;
then v1.degree() = v2.degree() & v1.inDegree() = v2.inDegree() &
v1.outDegree() = v2.outDegree() by A1, Th62;
hence thesis by CARD_2:94;
end;
suppose not(V c= the_Vertices_of G2 & not v in the_Vertices_of G2);
then G1 == G2 by GLIB_007:def 4;
then v1.degree() = v2.degree() & v1.inDegree() = v2.inDegree() &
v1.outDegree() = v2.outDegree() by A1, GLIB_000:96;
hence thesis by CARD_2:94;
end;
end;
begin :: into GLIB_008
theorem Th65:
for G being _Graph holds G is edgeless iff
for v,w being Vertex of G holds not v,w are_adjacent
proof
let G be _Graph;
hereby
assume A1: G is edgeless;
let v,w be Vertex of G;
not ex e being object st e Joins v,w,G by A1, GLIB_008:50;
hence not v,w are_adjacent by CHORD:def 3;
end;
assume A2: for v,w being Vertex of G holds not v,w are_adjacent;
assume G is non edgeless;
then consider e being object such that
A3: e in the_Edges_of G by XBOOLE_0:def 1;
set v = (the_Source_of G).e, w = (the_Target_of G).e;
reconsider v,w as Vertex of G by A3, FUNCT_2:5;
e Joins v,w,G by A3, GLIB_000:def 13;
hence contradiction by A2, CHORD:def 3;
end;
theorem
for G being loopless _Graph holds G is edgeless iff
for v,w being Vertex of G st v <> w holds not v,w are_adjacent
proof
let G be loopless _Graph;
thus G is edgeless implies
for v,w being Vertex of G st v <> w holds not v,w are_adjacent by Th65;
assume A1: for v,w being Vertex of G st v <> w holds not v,w are_adjacent;
assume G is non edgeless;
then consider e being object such that
A2: e in the_Edges_of G by XBOOLE_0:def 1;
set v = (the_Source_of G).e, w = (the_Target_of G).e;
reconsider v,w as Vertex of G by A2, FUNCT_2:5;
A3: e Joins v,w,G by A2, GLIB_000:def 13;
then v <> w by GLIB_000:18;
hence contradiction by A1, A3, CHORD:def 3;
end;
begin :: into GLIB_009
theorem Th67:
for G being _Graph
holds G.loops() = dom((the_Source_of G) /\ (the_Target_of G))
proof
let G be _Graph;
now
let e be object;
hereby
assume e in G.loops();
then consider v being object such that
A1: e DJoins v,v,G by GLIB_009:45;
e in the_Edges_of G by A1, GLIB_000:def 14;
then A2: e in dom the_Source_of G & e in dom the_Target_of G
by FUNCT_2:def 1;
(the_Source_of G).e=v & (the_Target_of G).e=v by A1, GLIB_000:def 14;
then [e,v] in the_Source_of G & [e,v] in the_Target_of G
by A2, FUNCT_1:def 2;
then [e,v] in (the_Source_of G) /\ (the_Target_of G) by XBOOLE_0:def 4;
hence e in dom((the_Source_of G) /\ (the_Target_of G)) by FUNCT_1:1;
end;
set v = ((the_Source_of G) /\ (the_Target_of G)).e;
assume e in dom((the_Source_of G) /\ (the_Target_of G));
then [e,v] in (the_Source_of G) /\ (the_Target_of G) by FUNCT_1:def 2;
then A3: [e,v] in the_Source_of G & [e,v] in the_Target_of G
by XBOOLE_0:def 4;
then A4: e in dom the_Source_of G & e in dom the_Target_of G by FUNCT_1:1;
then (the_Source_of G).e=v & (the_Target_of G).e=v by A3, FUNCT_1:def 2;
hence e in G.loops() by A4, GLIB_000:def 14, GLIB_009:45;
end;
hence thesis by TARSKI:2;
end;
Lm1:
for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
holds G2 is reverseEdgeDirections of G1, E \ G1.loops()
proof
let G1 be _Graph, E be set, G2 be reverseEdgeDirections of G1, E;
per cases;
suppose A1: E c= the_Edges_of G1;
then A2: the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 by GLIB_007:def 1;
A3: E \ G1.loops() c= the_Edges_of G1 by A1, XBOOLE_1:1;
set S = the_Source_of G1, T = the_Target_of G1;
dom(T | (E /\ G1.loops())) c= dom T by RELAT_1:60;
then dom(T | (E /\ G1.loops())) c= the_Edges_of G1 by FUNCT_2:def 1;
then A4: dom(T | (E /\ G1.loops())) c= dom S by FUNCT_2:def 1;
now
let x be object;
assume x in dom S /\ dom(T | (E /\ G1.loops()));
then A5: x in dom(T | (E /\ G1.loops())) by A4, XBOOLE_1:28;
then x in G1.loops() by XBOOLE_0:def 4;
then A6: x in dom(S /\ T) by Th67;
thus S.x = (S /\ T).x by A6, GRFUNC_1:11
.= T.x by A6, GRFUNC_1:11
.= (T | (E /\ G1.loops())).x by A5, FUNCT_1:47;
end;
then A7: S tolerates (T | (E /\ G1.loops())) by PARTFUN1:def 4;
A8: the_Source_of G2 = S +* (T | E) by A1, GLIB_007:def 1
.= S +* (T | ((E /\ G1.loops()) \/ (E \ G1.loops()))) by XBOOLE_1:51
.= S +* ((T | (E /\ G1.loops())) +* (T | (E \ G1.loops()))) by FUNCT_4:78
.= S +* (T | (E /\ G1.loops())) +* (T | (E \ G1.loops())) by FUNCT_4:14
.= (T|(E /\ G1.loops())) +* S +* (T | (E \ G1.loops())) by A7, FUNCT_4:34
.= S +* (T | (E \ G1.loops())) by A4, FUNCT_4:19;
dom(S | (E /\ G1.loops())) c= dom S by RELAT_1:60;
then dom(S | (E /\ G1.loops())) c= the_Edges_of G1 by FUNCT_2:def 1;
then A9: dom(S | (E /\ G1.loops())) c= dom T by FUNCT_2:def 1;
now
let x be object;
assume x in dom T /\ dom(S | (E /\ G1.loops()));
then A10: x in dom(S | (E /\ G1.loops())) by A9, XBOOLE_1:28;
then x in G1.loops() by XBOOLE_0:def 4;
then A11: x in dom(S /\ T) by Th67;
thus T.x = (S /\ T).x by A11, GRFUNC_1:11
.= S.x by A11, GRFUNC_1:11
.= (S | (E /\ G1.loops())).x by A10, FUNCT_1:47;
end;
then A12: T tolerates (S | (E /\ G1.loops())) by PARTFUN1:def 4;
the_Target_of G2 = T +* (S | E) by A1, GLIB_007:def 1
.= T +* (S | ((E /\ G1.loops()) \/ (E \ G1.loops()))) by XBOOLE_1:51
.= T +* ((S | (E /\ G1.loops())) +* (S | (E \ G1.loops()))) by FUNCT_4:78
.= T +* (S | (E /\ G1.loops())) +* (S | (E \ G1.loops())) by FUNCT_4:14
.= (S|(E /\ G1.loops())) +* T +* (S | (E \ G1.loops())) by A12
, FUNCT_4:34
.= T +* (S | (E \ G1.loops())) by A9, FUNCT_4:19;
hence thesis by A2, A3, A8, GLIB_007:def 1;
end;
suppose A13: not E c= the_Edges_of G1;
then A14: G1 == G2 by GLIB_007:def 1;
consider e being object such that
A15: e in E & not e in the_Edges_of G1 by A13, TARSKI:def 3;
not e in G1.loops() by A15;
then e in E \ G1.loops() by A15, XBOOLE_0:def 5;
then not E \ G1.loops() c= the_Edges_of G1 by A15;
hence thesis by A14, GLIB_007:def 1;
end;
end;
Lm2:
for G1 being _Graph, E being set
for G2 being reverseEdgeDirections of G1, E \ G1.loops()
holds G2 is reverseEdgeDirections of G1, E
proof
let G1 be _Graph, E be set;
let G2 be reverseEdgeDirections of G1, E \ G1.loops();
per cases;
suppose A1: E \ G1.loops() c= the_Edges_of G1;
then A2: the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 by GLIB_007:def 1;
E c= the_Edges_of G1 \/ G1.loops() by A1, XBOOLE_1:44;
then A3: E c= the_Edges_of G1 by XBOOLE_1:12;
set S = the_Source_of G1, T = the_Target_of G1;
dom(T | (E /\ G1.loops())) c= dom T by RELAT_1:60;
then dom(T | (E /\ G1.loops())) c= the_Edges_of G1 by FUNCT_2:def 1;
then A4: dom(T | (E /\ G1.loops())) c= dom S by FUNCT_2:def 1;
now
let x be object;
assume x in dom S /\ dom(T | (E /\ G1.loops()));
then A5: x in dom(T | (E /\ G1.loops())) by A4, XBOOLE_1:28;
then x in G1.loops() by XBOOLE_0:def 4;
then A6: x in dom(S /\ T) by Th67;
thus S.x = (S /\ T).x by A6, GRFUNC_1:11
.= T.x by A6, GRFUNC_1:11
.= (T | (E /\ G1.loops())).x by A5, FUNCT_1:47;
end;
then A7: S tolerates (T | (E /\ G1.loops())) by PARTFUN1:def 4;
A8: the_Source_of G2
= S +* (T | (E \ G1.loops())) by A1, GLIB_007:def 1
.= (T|(E /\ G1.loops())) +* S +* (T | (E \ G1.loops())) by A4, FUNCT_4:19
.= S +* (T | (E /\ G1.loops())) +* (T | (E\G1.loops())) by A7, FUNCT_4:34
.= S +* ((T | (E /\ G1.loops())) +* (T | (E \ G1.loops()))) by FUNCT_4:14
.= S +* (T | ((E /\ G1.loops()) \/ (E \ G1.loops()))) by FUNCT_4:78
.= S +* (T | E) by XBOOLE_1:51;
dom(S | (E /\ G1.loops())) c= dom S by RELAT_1:60;
then dom(S | (E /\ G1.loops())) c= the_Edges_of G1 by FUNCT_2:def 1;
then A9: dom(S | (E /\ G1.loops())) c= dom T by FUNCT_2:def 1;
now
let x be object;
assume x in dom T /\ dom(S | (E /\ G1.loops()));
then A10: x in dom(S | (E /\ G1.loops())) by A9, XBOOLE_1:28;
then x in G1.loops() by XBOOLE_0:def 4;
then A11: x in dom(S /\ T) by Th67;
thus T.x = (S /\ T).x by A11, GRFUNC_1:11
.= S.x by A11, GRFUNC_1:11
.= (S | (E /\ G1.loops())).x by A10, FUNCT_1:47;
end;
then A12: T tolerates (S | (E /\ G1.loops())) by PARTFUN1:def 4;
the_Target_of G2
= T +* (S | (E \ G1.loops())) by A1, GLIB_007:def 1
.= (S|(E /\ G1.loops())) +* T +* (S | (E \ G1.loops())) by A9, FUNCT_4:19
.= T +* (S | (E /\ G1.loops())) +* (S | (E\G1.loops())) by A12
, FUNCT_4:34
.= T +* ((S | (E /\ G1.loops())) +* (S | (E \ G1.loops()))) by FUNCT_4:14
.= T +* (S | ((E /\ G1.loops()) \/ (E \ G1.loops()))) by FUNCT_4:78
.= T +* (S | E) by XBOOLE_1:51;
hence thesis by A3, A2, A8, GLIB_007:def 1;
end;
suppose A13: not E \ G1.loops() c= the_Edges_of G1;
A14: not E c= the_Edges_of G1 by A13, XBOOLE_1:1;
G1 == G2 by A13, GLIB_007:def 1;
hence thesis by A14, GLIB_007:def 1;
end;
end;
theorem
for G1, G2 being _Graph, E being set
holds G2 is reverseEdgeDirections of G1, E iff
G2 is reverseEdgeDirections of G1, E \ G1.loops() by Lm1, Lm2;
theorem Th69:
for G1 being _Graph, G2 being removeLoops of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds
v2.inNeighbors() = v1.inNeighbors() \ {v1} &
v2.outNeighbors() = v1.outNeighbors() \ {v1} &
v2.allNeighbors() = v1.allNeighbors() \ {v1}
proof
let G1 be _Graph, G2 be removeLoops of G1;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2;
now
let x be object;
hereby
assume A2: x in v2.inNeighbors();
then A3: x in v1.inNeighbors() by A1, GLIB_000:82, TARSKI:def 3;
consider e being object such that
A4: e DJoins x,v2,G2 by A2, GLIB_000:69;
x <> v2 by A4, GLIB_000:136;
then not x in {v1} by A1, TARSKI:def 1;
hence x in v1.inNeighbors() \ {v1} by A3, XBOOLE_0:def 5;
end;
assume x in v1.inNeighbors() \ {v1};
then A5: x in v1.inNeighbors() & not x in {v1} by XBOOLE_0:def 5;
then consider e being object such that
A6: e DJoins x,v1,G1 by GLIB_000:69;
A7: e Joins x,v1,G1 by A6, GLIB_000:16;
x <> v1 by A5, TARSKI:def 1;
then A8: not e in G1.loops() by A7, GLIB_009:46;
e in the_Edges_of G1 by A6, GLIB_000:def 14;
then e in the_Edges_of G1 \ G1.loops() by A8, XBOOLE_0:def 5;
then A9: e in the_Edges_of G2 by GLIB_000:53;
A10: x is set & e is set by TARSKI:1;
then e DJoins x,v1,G2 by A6, A9, GLIB_000:73;
hence x in v2.inNeighbors() by A1, A10, GLIB_000:69;
end;
hence A11: v2.inNeighbors() = v1.inNeighbors() \ {v1} by TARSKI:2;
now
let x be object;
hereby
assume A12: x in v2.outNeighbors();
then A13: x in v1.outNeighbors() by A1, GLIB_000:82, TARSKI:def 3;
consider e being object such that
A14: e DJoins v2,x,G2 by A12, GLIB_000:70;
x <> v2 by A14, GLIB_000:136;
then not x in {v1} by A1, TARSKI:def 1;
hence x in v1.outNeighbors() \ {v1} by A13, XBOOLE_0:def 5;
end;
assume x in v1.outNeighbors() \ {v1};
then A15: x in v1.outNeighbors() & not x in {v1} by XBOOLE_0:def 5;
then consider e being object such that
A16: e DJoins v1,x,G1 by GLIB_000:70;
A17: e Joins v1,x,G1 by A16, GLIB_000:16;
x <> v1 by A15, TARSKI:def 1;
then A18: not e in G1.loops() by A17, GLIB_009:46;
e in the_Edges_of G1 by A16, GLIB_000:def 14;
then e in the_Edges_of G1 \ G1.loops() by A18, XBOOLE_0:def 5;
then A19: e in the_Edges_of G2 by GLIB_000:53;
A20: x is set & e is set by TARSKI:1;
then e DJoins v1,x,G2 by A16, A19, GLIB_000:73;
hence x in v2.outNeighbors() by A1, A20, GLIB_000:70;
end;
hence A21: v2.outNeighbors() = v1.outNeighbors() \ {v1} by TARSKI:2;
thus v2.allNeighbors() = v1.allNeighbors() \ {v1} by A11, A21, XBOOLE_1:42;
end;
theorem Th70:
for G1 being _Graph, G2 being removeParallelEdges of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds v2.allNeighbors() = v1.allNeighbors()
proof
let G1 be _Graph, G2 be removeParallelEdges of G1;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2;
consider E being RepEdgeSelection of G1 such that
A2: G2 is inducedSubgraph of G1, the_Vertices_of G1, E by GLIB_009:def 7;
the_Edges_of G1 = G1.edgesBetween(the_Vertices_of G1) by GLIB_000:34;
then E c= G1.edgesBetween(the_Vertices_of G1) &
the_Vertices_of G1 c= the_Vertices_of G1;
then A3: the_Edges_of G2 = E by A2, GLIB_000:def 37;
A4: v2.allNeighbors() c= v1.allNeighbors() by A1, GLIB_000:82;
now
let x be object;
assume x in v1.allNeighbors();
then consider e0 being object such that
A5: e0 Joins v1,x,G1 by GLIB_000:71;
consider e being object such that
A6: e Joins v1,x,G1 & e in E and
for e9 being object st e9 Joins v1,x,G1 & e9 in E holds e9 = e
by A5, GLIB_009:def 5;
A7: x is set & e is set by TARSKI:1;
then e Joins v1,x,G2 by A3, A6, GLIB_000:73;
hence x in v2.allNeighbors() by A1, A7, GLIB_000:71;
end;
then v1.allNeighbors() c= v2.allNeighbors() by TARSKI:def 3;
hence v2.allNeighbors() = v1.allNeighbors() by A4, XBOOLE_0:def 10;
end;
theorem Th71:
for G1 being _Graph, G2 being removeDParallelEdges of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds
v2.inNeighbors() = v1.inNeighbors() &
v2.outNeighbors() = v1.outNeighbors() &
v2.allNeighbors() = v1.allNeighbors()
proof
let G1 be _Graph, G2 be removeDParallelEdges of G1;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2;
consider E being RepDEdgeSelection of G1 such that
A2: G2 is inducedSubgraph of G1, the_Vertices_of G1, E by GLIB_009:def 8;
the_Edges_of G1 = G1.edgesBetween(the_Vertices_of G1) by GLIB_000:34;
then E c= G1.edgesBetween(the_Vertices_of G1) &
the_Vertices_of G1 c= the_Vertices_of G1;
then A3: the_Edges_of G2 = E by A2, GLIB_000:def 37;
A4: v2.inNeighbors() c= v1.inNeighbors() by A1, GLIB_000:82;
now
let x be object;
assume x in v1.inNeighbors();
then consider e0 being object such that
A5: e0 DJoins x,v1,G1 by GLIB_000:69;
consider e being object such that
A6: e DJoins x,v1,G1 & e in E and
for e9 being object st e9 DJoins x,v1,G1 & e9 in E holds e9 = e
by A5, GLIB_009:def 6;
A7: x is set & e is set by TARSKI:1;
then e DJoins x,v1,G2 by A3, A6, GLIB_000:73;
hence x in v2.inNeighbors() by A1, A7, GLIB_000:69;
end;
then v1.inNeighbors() c= v2.inNeighbors() by TARSKI:def 3;
hence A8: v2.inNeighbors() = v1.inNeighbors() by A4, XBOOLE_0:def 10;
A9: v2.outNeighbors() c= v1.outNeighbors() by A1, GLIB_000:82;
now
let x be object;
assume x in v1.outNeighbors();
then consider e0 being object such that
A10: e0 DJoins v1,x,G1 by GLIB_000:70;
consider e being object such that
A11: e DJoins v1,x,G1 & e in E and
for e9 being object st e9 DJoins v1,x,G1 & e9 in E holds e9 = e
by A10, GLIB_009:def 6;
A12: x is set & e is set by TARSKI:1;
then e DJoins v1,x,G2 by A3, A11, GLIB_000:73;
hence x in v2.outNeighbors() by A1, A12, GLIB_000:70;
end;
then v1.outNeighbors() c= v2.outNeighbors() by TARSKI:def 3;
hence A13: v2.outNeighbors() = v1.outNeighbors() by A9, XBOOLE_0:def 10;
thus v2.allNeighbors() = v1.allNeighbors() by A8, A13;
end;
theorem
for G1 being _Graph, G2 being SimpleGraph of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds v2.allNeighbors() = v1.allNeighbors() \ {v1}
proof
let G1 be _Graph, G2 be SimpleGraph of G1;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2;
consider G9 being removeParallelEdges of G1 such that
A2: G2 is removeLoops of G9 by GLIB_009:119;
reconsider v3 = v2 as Vertex of G9 by A2, GLIB_000:53;
thus v2.allNeighbors() = v3.allNeighbors() \ {v3} by A2, Th69
.= v1.allNeighbors() \ {v1} by A1, Th70;
end;
theorem
for G1 being _Graph, G2 being DSimpleGraph of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds
v2.inNeighbors() = v1.inNeighbors() \ {v1} &
v2.outNeighbors() = v1.outNeighbors() \ {v1} &
v2.allNeighbors() = v1.allNeighbors() \ {v1}
proof
let G1 be _Graph, G2 be DSimpleGraph of G1;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2;
consider G9 being removeDParallelEdges of G1 such that
A2: G2 is removeLoops of G9 by GLIB_009:120;
reconsider v3 = v2 as Vertex of G9 by A2, GLIB_000:53;
thus v2.inNeighbors() = v3.inNeighbors() \ {v3} by A2, Th69
.= v1.inNeighbors() \ {v1} by A1, Th71;
thus v2.outNeighbors() = v3.outNeighbors() \ {v3} by A2, Th69
.= v1.outNeighbors() \ {v1} by A1, Th71;
thus v2.allNeighbors() = v3.allNeighbors() \ {v3} by A2, Th69
.= v1.allNeighbors() \ {v1} by A1, Th71;
end;
registration
let G be non loopless _Graph;
cluster -> non loopless for removeParallelEdges of G;
coherence
proof
let H be removeParallelEdges of G;
consider E being RepEdgeSelection of G such that
A1: H is inducedSubgraph of G, the_Vertices_of G, E by GLIB_009:def 7;
consider v being object such that
A2: ex e being object st e Joins v,v,G by GLIB_000:18;
consider e0 being object such that
A3: e0 Joins v,v,G by A2;
consider e being object such that
A4: e Joins v,v,G & e in E and
for e9 being object st e9 Joins v,v,G & e9 in E holds e9 = e
by A3, GLIB_009:def 5;
A5: the_Edges_of G = G.edgesBetween(the_Vertices_of G) by GLIB_000:34;
the_Vertices_of G c= the_Vertices_of G;
then A6: e in the_Edges_of H by A1, A4, A5, GLIB_000:def 37;
v is set & e is set by TARSKI:1;
then e Joins v,v,H by A4, A6, GLIB_000:73;
hence thesis by GLIB_000:18;
end;
cluster -> non loopless for removeDParallelEdges of G;
coherence
proof
let H be removeDParallelEdges of G;
consider E being RepDEdgeSelection of G such that
A7: H is inducedSubgraph of G, the_Vertices_of G, E by GLIB_009:def 8;
consider v being object such that
A8: ex e being object st e DJoins v,v,G by GLIB_000:136;
consider e0 being object such that
A9: e0 DJoins v,v,G by A8;
consider e being object such that
A10: e DJoins v,v,G & e in E and
for e9 being object st e9 DJoins v,v,G & e9 in E holds e9 = e
by A9, GLIB_009:def 6;
A11: the_Edges_of G = G.edgesBetween(the_Vertices_of G) by GLIB_000:34;
the_Vertices_of G c= the_Vertices_of G;
then A12: e in the_Edges_of H by A7, A10, A11, GLIB_000:def 37;
v is set & e is set by TARSKI:1;
then e DJoins v,v,H by A10, A12, GLIB_000:73;
hence thesis by GLIB_000:136;
end;
end;
registration
let G be non edgeless _Graph;
cluster -> non edgeless for removeParallelEdges of G;
coherence
proof
let H be removeParallelEdges of G;
consider E being RepEdgeSelection of G such that
A1: H is inducedSubgraph of G, the_Vertices_of G, E by GLIB_009:def 7;
A4: the_Edges_of G = G.edgesBetween(the_Vertices_of G) by GLIB_000:34;
the_Vertices_of G c= the_Vertices_of G;
then the_Edges_of H = E by A1, A4, GLIB_000:def 37;
hence thesis;
end;
cluster -> non edgeless for removeDParallelEdges of G;
coherence
proof
let H be removeDParallelEdges of G;
consider E being RepDEdgeSelection of G such that
A5: H is inducedSubgraph of G, the_Vertices_of G, E by GLIB_009:def 8;
A8: the_Edges_of G = G.edgesBetween(the_Vertices_of G) by GLIB_000:34;
the_Vertices_of G c= the_Vertices_of G;
then the_Edges_of H = E by A5, A8, GLIB_000:def 37;
hence thesis;
end;
end;
theorem
for G being _Graph, E being RepEdgeSelection of G
holds card E = card Class EdgeAdjEqRel(G)
proof
let G be _Graph, E be RepEdgeSelection of G;
deffunc F(object) = Class(EdgeAdjEqRel(G),$1);
consider f being Function such that
A1: dom f = E & for x being object st x in E holds f.x = F(x)
from FUNCT_1:sch 3;
now
let y be object;
hereby
assume y in rng f;
then consider x being object such that
A2: x in dom f & f.x = y by FUNCT_1:def 3;
y = Class(EdgeAdjEqRel(G),x) by A1, A2;
hence y in Class EdgeAdjEqRel(G) by A1, A2, EQREL_1:def 3;
end;
assume y in Class EdgeAdjEqRel(G);
then consider x being object such that
A3: x in the_Edges_of G & y = Class(EdgeAdjEqRel(G),x) by EQREL_1:def 3;
set v = (the_Source_of G).x, w = (the_Target_of G).x;
A4: x Joins v,w,G by A3, GLIB_000:def 13;
then consider e being object such that
A5: e Joins v,w,G & e in E and
for e9 being object st e9 Joins v,w,G & e9 in E holds e9 = e
by GLIB_009:def 5;
[x,e] in EdgeAdjEqRel(G) by A4, A5, GLIB_009:def 3;
then e in Class(EdgeAdjEqRel(G),x) by EQREL_1:18;
then y = Class(EdgeAdjEqRel(G),e) by A3, EQREL_1:23
.= f.e by A1, A5;
hence y in rng f by A1, A5, FUNCT_1:3;
end;
then A6: rng f = Class EdgeAdjEqRel(G) by TARSKI:2;
now
let x1,x2 be object;
assume A7: x1 in dom f & x2 in dom f & f.x1 = f.x2;
then f.x1=Class(EdgeAdjEqRel(G),x1) & f.x2=Class(EdgeAdjEqRel(G),x2) by A1;
then x2 in Class(EdgeAdjEqRel(G),x1) by A1, A7, EQREL_1:23;
then [x1,x2] in EdgeAdjEqRel(G) by EQREL_1:18;
then consider v,w being object such that
A8: x1 Joins v,w,G & x2 Joins v,w,G by GLIB_009:def 3;
consider e being object such that
e Joins v,w,G & e in E and
A9: for e9 being object st e9 Joins v,w,G & e9 in E holds e9 = e
by A8, GLIB_009:def 5;
x1 = e & x2 = e by A1, A7, A8, A9;
hence x1 = x2;
end;
hence thesis by A1, A6, FUNCT_1:def 4, CARD_1:70;
end;
theorem
for G being _Graph, E being RepDEdgeSelection of G
holds card E = card Class DEdgeAdjEqRel(G)
proof
let G be _Graph, E be RepDEdgeSelection of G;
deffunc F(object) = Class(DEdgeAdjEqRel(G),$1);
consider f being Function such that
A1: dom f = E & for x being object st x in E holds f.x = F(x)
from FUNCT_1:sch 3;
now
let y be object;
hereby
assume y in rng f;
then consider x being object such that
A2: x in dom f & f.x = y by FUNCT_1:def 3;
y = Class(DEdgeAdjEqRel(G),x) by A1, A2;
hence y in Class DEdgeAdjEqRel(G) by A1, A2, EQREL_1:def 3;
end;
assume y in Class DEdgeAdjEqRel(G);
then consider x being object such that
A3: x in the_Edges_of G & y = Class(DEdgeAdjEqRel(G),x) by EQREL_1:def 3;
set v = (the_Source_of G).x, w = (the_Target_of G).x;
A4: x DJoins v,w,G by A3, GLIB_000:def 14;
then consider e being object such that
A5: e DJoins v,w,G & e in E and
for e9 being object st e9 DJoins v,w,G & e9 in E holds e9 = e
by GLIB_009:def 6;
[x,e] in DEdgeAdjEqRel(G) by A4, A5, GLIB_009:def 4;
then e in Class(DEdgeAdjEqRel(G),x) by EQREL_1:18;
then y = Class(DEdgeAdjEqRel(G),e) by A3, EQREL_1:23
.= f.e by A1, A5;
hence y in rng f by A1, A5, FUNCT_1:3;
end;
then A6: rng f = Class DEdgeAdjEqRel(G) by TARSKI:2;
now
let x1,x2 be object;
assume A7: x1 in dom f & x2 in dom f & f.x1 = f.x2;
then f.x1=Class(DEdgeAdjEqRel(G),x1) & f.x2=Class(DEdgeAdjEqRel(G),x2)
by A1;
then x2 in Class(DEdgeAdjEqRel(G),x1) by A1, A7, EQREL_1:23;
then [x1,x2] in DEdgeAdjEqRel(G) by EQREL_1:18;
then consider v,w being object such that
A8: x1 DJoins v,w,G & x2 DJoins v,w,G by GLIB_009:def 4;
consider e being object such that
e DJoins v,w,G & e in E and
A9: for e9 being object st e9 DJoins v,w,G & e9 in E holds e9 = e
by A8, GLIB_009:def 6;
x1 = e & x2 = e by A1, A7, A8, A9;
hence x1 = x2;
end;
hence thesis by A1, A6, CARD_1:70, FUNCT_1:def 4;
end;
Lm3:
for G being _Graph, X being set, E being Subset of the_Edges_of G
for H being reverseEdgeDirections of G, X
holds E is RepEdgeSelection of G implies E is RepEdgeSelection of H
proof
let G be _Graph, X be set, E be Subset of the_Edges_of G;
let H be reverseEdgeDirections of G, X;
assume A1: E is RepEdgeSelection of G;
A2: E is Subset of the_Edges_of H by GLIB_007:4;
now
let v,w,e0 be object;
assume e0 Joins v,w,H;
then consider e being object such that
A3: e Joins v,w,G & e in E and
A4: for e9 being object st e9 Joins v,w,G & e9 in E holds e9 = e
by A1, GLIB_007:9, GLIB_009:def 5;
take e;
thus e Joins v,w,H & e in E by A3, GLIB_007:9;
let e9 be object;
assume e9 Joins v,w,H & e9 in E;
hence e9 = e by A4, GLIB_007:9;
end;
hence thesis by A2, GLIB_009:def 5;
end;
theorem
for G being _Graph, X being set, E being Subset of the_Edges_of G
for H being reverseEdgeDirections of G, X
holds E is RepEdgeSelection of G iff E is RepEdgeSelection of H
proof
let G be _Graph, X be set, E be Subset of the_Edges_of G;
let H be reverseEdgeDirections of G, X;
thus E is RepEdgeSelection of G implies E is RepEdgeSelection of H by Lm3;
A1: G is reverseEdgeDirections of H, X by GLIB_007:3;
assume E is RepEdgeSelection of H;
hence thesis by A1, Lm3;
end;
theorem
for G being _Graph, V being non empty Subset of the_Vertices_of G
for H being (inducedSubgraph of G, V), E being RepEdgeSelection of G
holds E /\ G.edgesBetween(V) is RepEdgeSelection of H
proof
let G be _Graph, V be non empty Subset of the_Vertices_of G;
let H be (inducedSubgraph of G, V), E be RepEdgeSelection of G;
G.edgesBetween(V) = the_Edges_of H by GLIB_000:def 37;
then reconsider E9 = E /\ G.edgesBetween(V) as Subset of the_Edges_of H
by XBOOLE_1:17;
now
let v,w,e0 be object;
A1: v is set & w is set by TARSKI:1;
assume A2: e0 Joins v,w,H;
then e0 Joins v,w,G by A1, GLIB_000:72;
then consider e being object such that
A3: e Joins v,w,G & e in E and
A4: for e9 being object st e9 Joins v,w,G & e9 in E holds e9 = e
by GLIB_009:def 5;
take e;
v in the_Vertices_of H & w in the_Vertices_of H by A2, GLIB_000:13;
then v in V & w in V by GLIB_000:def 37;
then A5: e in G.edgesBetween(V) by A3, GLIB_000:32;
then e in the_Edges_of H by GLIB_000:def 37;
hence e Joins v,w,H by A1, A3, GLIB_000:73;
thus e in E9 by A3, A5, XBOOLE_0:def 4;
let e9 be object;
assume e9 Joins v,w,H & e9 in E9;
then e9 Joins v,w,G & e9 in E by A1, GLIB_000:72, XBOOLE_0:def 4;
hence e9 = e by A4;
end;
hence thesis by GLIB_009:def 5;
end;
theorem
for G being _Graph, V being non empty Subset of the_Vertices_of G
for H being (inducedSubgraph of G, V), E being RepDEdgeSelection of G
holds E /\ G.edgesBetween(V) is RepDEdgeSelection of H
proof
let G be _Graph, V be non empty Subset of the_Vertices_of G;
let H be (inducedSubgraph of G, V), E be RepDEdgeSelection of G;
G.edgesBetween(V) = the_Edges_of H by GLIB_000:def 37;
then reconsider E9 = E /\ G.edgesBetween(V) as Subset of the_Edges_of H
by XBOOLE_1:17;
now
let v,w,e0 be object;
A1: v is set & w is set by TARSKI:1;
assume A2: e0 DJoins v,w,H;
then e0 DJoins v,w,G by A1, GLIB_000:72;
then consider e being object such that
A3: e DJoins v,w,G & e in E and
A4: for e9 being object st e9 DJoins v,w,G & e9 in E holds e9 = e
by GLIB_009:def 6;
take e;
e0 Joins v,w,H by A2, GLIB_000:16;
then v in the_Vertices_of H & w in the_Vertices_of H by GLIB_000:13;
then A5: v in V & w in V by GLIB_000:def 37;
e Joins v,w,G by A3, GLIB_000:16;
then A6: e in G.edgesBetween(V) by A5, GLIB_000:32;
then e in the_Edges_of H by GLIB_000:def 37;
hence e DJoins v,w,H by A1, A3, GLIB_000:73;
thus e in E9 by A3, A6, XBOOLE_0:def 4;
let e9 be object;
assume e9 DJoins v,w,H & e9 in E9;
then e9 DJoins v,w,G & e9 in E by A1, GLIB_000:72, XBOOLE_0:def 4;
hence e9 = e by A4;
end;
hence thesis by GLIB_009:def 6;
end;
theorem
for G being _Graph, V being set, H being addVertices of G, V
for E being Subset of the_Edges_of G
holds E is RepEdgeSelection of G iff E is RepEdgeSelection of H
proof
let G be _Graph, V be set, H be addVertices of G,V;
let E be Subset of the_Edges_of G;
A1: the_Edges_of G = the_Edges_of H by GLIB_006:def 10;
hereby
assume A2: E is RepEdgeSelection of G;
now
let v,w,e0 be object;
A3: v is set & w is set by TARSKI:1;
assume e0 Joins v,w,H;
then consider e being object such that
A4: e Joins v,w,G & e in E and
A5: for e9 being object st e9 Joins v,w,G & e9 in E holds e9 = e
by A2, A3, GLIB_009:41, GLIB_009:def 5;
take e;
thus e Joins v,w,H & e in E by A3, A4, GLIB_009:41;
let e9 be object;
assume e9 Joins v,w,H & e9 in E;
hence e9 = e by A3, A5, GLIB_009:41;
end;
hence E is RepEdgeSelection of H by A1, GLIB_009:def 5;
end;
assume A6: E is RepEdgeSelection of H;
now
let v,w,e0 be object;
A7: v is set & w is set by TARSKI:1;
assume e0 Joins v,w,G;
then consider e being object such that
A8: e Joins v,w,H & e in E and
A9: for e9 being object st e9 Joins v,w,H & e9 in E holds e9 = e
by A6, A7, GLIB_009:41, GLIB_009:def 5;
take e;
thus e Joins v,w,G & e in E by A7, A8, GLIB_009:41;
let e9 be object;
assume e9 Joins v,w,G & e9 in E;
hence e9 = e by A7, A9, GLIB_009:41;
end;
hence E is RepEdgeSelection of G by GLIB_009:def 5;
end;
theorem
for G being _Graph, V being set, H being addVertices of G, V
for E being Subset of the_Edges_of G
holds E is RepDEdgeSelection of G iff E is RepDEdgeSelection of H
proof
let G be _Graph, V be set, H be addVertices of G,V;
let E be Subset of the_Edges_of G;
A1: the_Edges_of G = the_Edges_of H by GLIB_006:def 10;
hereby
assume A2: E is RepDEdgeSelection of G;
now
let v,w,e0 be object;
A3: v is set & w is set by TARSKI:1;
assume e0 DJoins v,w,H;
then consider e being object such that
A4: e DJoins v,w,G & e in E and
A5: for e9 being object st e9 DJoins v,w,G & e9 in E holds e9 = e
by A2, A3, GLIB_009:41, GLIB_009:def 6;
take e;
thus e DJoins v,w,H & e in E by A3, A4, GLIB_009:41;
let e9 be object;
assume e9 DJoins v,w,H & e9 in E;
hence e9 = e by A3, A5, GLIB_009:41;
end;
hence E is RepDEdgeSelection of H by A1, GLIB_009:def 6;
end;
assume A6: E is RepDEdgeSelection of H;
now
let v,w,e0 be object;
A7: v is set & w is set by TARSKI:1;
assume e0 DJoins v,w,G;
then consider e being object such that
A8: e DJoins v,w,H & e in E and
A9: for e9 being object st e9 DJoins v,w,H & e9 in E holds e9 = e
by A6, A7, GLIB_009:41, GLIB_009:def 6;
take e;
thus e DJoins v,w,G & e in E by A7, A8, GLIB_009:41;
let e9 be object;
assume e9 DJoins v,w,G & e9 in E;
hence e9 = e by A7, A9, GLIB_009:41;
end;
hence E is RepDEdgeSelection of G by GLIB_009:def 6;
end;
registration
cluster non non-multi non-Dmulti for _Graph;
existence
proof
set G0 = the _trivial edgeless _Graph, v = the Vertex of G0;
set w = the_Vertices_of G0, e = the_Edges_of G0;
set G1 = the addAdjVertex of G0,v,e,w;
A1: not e in the_Edges_of G0 & not w in the_Vertices_of G0;
reconsider v1 = v, w1 = w as Vertex of G1
by A1, GLIB_006:68, GLIB_006:129;
set f = the_Edges_of G1, G2 = the addEdge of G1, w1,f,v1;
take G2;
A3: e DJoins v,w,G2 by A1, GLIB_006:70, GLIB_006:131;
A4: not f in the_Edges_of G1;
then A5: f DJoins w1,v1,G2 by GLIB_006:105;
ex e1,e2,v1,v2 being object
st e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2 & e1 <> e2
proof
take e,f,v,w;
thus e Joins v,w,G2 by A3, GLIB_000:16;
thus f Joins v,w,G2 by A5, GLIB_000:16;
thus e <> f;
end;
hence G2 is non non-multi by GLIB_000:def 20;
for e1,e2,v1,v2 being object
st e1 DJoins v1,v2,G2 & e2 DJoins v1,v2,G2 holds e1 = e2
proof
let e1,e2,v1,v2 be object;
assume A6: e1 DJoins v1,v2,G2 & e2 DJoins v1,v2,G2;
then A7: e1 in the_Edges_of G2 & e2 in the_Edges_of G2
by GLIB_000:def 14;
the_Edges_of G2 = the_Edges_of G1 \/ {f} by A4, GLIB_006:def 11
.= the_Edges_of G0 \/ {e} \/ {f} by A1, GLIB_006:def 12
.= {e,f} by ENUMSET1:1;
then per cases by A7, TARSKI:def 2;
suppose e1 = e & e2 = e;
hence thesis;
end;
suppose e1 = e & e2 = f; :: by contradiction
then v1 = v & v2 = w & v1 = w & v2 = v by A3, A5, A6, GLIB_000:125;
then v = w & v in w;
hence thesis;
end;
suppose e1 = f & e2 = e; :: by contradiction
then v1 = v & v2 = w & v1 = w & v2 = v by A3, A5, A6, GLIB_000:125;
then v = w & v in w;
hence thesis;
end;
suppose e1 = f & e2 = f;
hence thesis;
end;
end;
hence thesis by GLIB_000:def 21;
end;
end;
definition
let GF be Graph-yielding Function;
attr GF is plain means
:Def1:
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is plain;
end;
registration
let G be plain _Graph;
cluster <* G *> -> plain;
coherence
proof
let x be object;
assume A1: x in dom <* G *>;
then reconsider n = x as Nat;
1 <= n <= len <* G *> by A1, FINSEQ_3:25;
then 1 <= n <= 1 by FINSEQ_1:40;
then n = 1 by XXREAL_0:1;
hence thesis;
end;
cluster NAT --> G -> plain;
coherence by FUNCOP_1:7;
end;
definition
let GF be non empty Graph-yielding Function;
redefine attr GF is plain means :: redefines plain (GLIBPRE0, definition)
:Def2:
for x being Element of dom GF holds GF.x is plain;
compatibility
proof
hereby
assume A1: GF is plain;
let x be Element of dom GF;
consider G being _Graph such that
A2: GF.x = G & G is plain by A1;
thus GF.x is plain by A2;
end;
assume A3: for x being Element of dom GF holds GF.x is plain;
let x be object;
assume x in dom GF;
then reconsider y = x as Element of dom GF;
take GF.y;
thus thesis by A3;
end;
end;
Lm4: :: copied from GLIB_000
for F being ManySortedSet of NAT, n being object
holds n is Nat iff n in dom F
proof
let F be ManySortedSet of NAT, n being object;
hereby
assume n is Nat;
then n in NAT by ORDINAL1:def 12;
hence n in dom F by PARTFUN1:def 2;
end;
assume n in dom F;
hence n is Nat;
end;
definition
let GSq be GraphSeq;
redefine attr GSq is plain means :: redefines plain (GLIBPRE0, redefinition) → plain (GLIBPRE0, definition)
:Def3:
for n being Nat holds GSq.n is plain;
compatibility
proof
hereby
assume A1: GSq is plain;
let x be Nat;
x in dom GSq by Lm4;
hence GSq.x is plain by A1;
end;
assume A2: for x being Nat holds GSq.x is plain;
let x be Element of dom GSq;
thus thesis by A2;
end;
end;
registration
cluster empty -> plain for Graph-yielding Function;
coherence;
end;
registration
cluster plain for GraphSeq;
existence
proof
take NAT --> the plain _Graph;
thus thesis;
end;
cluster non empty plain for Graph-yielding FinSequence;
existence
proof
take <* the plain _Graph *>;
thus thesis;
end;
end;
registration
let GF be plain non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> plain;
coherence by Def2;
end;
registration
let GSq be plain GraphSeq, x be Nat;
cluster GSq.x -> plain;
coherence by Def3;
end;
registration
let p be plain Graph-yielding FinSequence, n be Nat;
cluster p | n -> plain;
coherence
proof
A1: p|n = p|Seg n by FINSEQ_1:def 16;
now
let x be object;
assume A2: x in dom(p|n);
then x in dom p by A1, RELAT_1:60, TARSKI:def 3;
then consider G being _Graph such that
A3: p.x = G & G is plain by Def1;
take G;
thus (p|n).x = G & G is plain by A1, A3, A2, FUNCT_1:47;
end;
hence thesis;
end;
cluster p /^ n -> plain;
coherence
proof
per cases;
suppose A4: n <= len p;
now
let x be object;
assume A5: x in dom(p /^ n);
then reconsider i = x as Nat;
n+i in dom p by A5, FINSEQ_5:26;
then consider G being _Graph such that
A6: p.(n+i) = G & G is plain by Def1;
take G;
thus (p /^ n).x = G & G is plain by A4, A5, A6, RFINSEQ:def 1;
end;
hence thesis;
end;
suppose not (n <= len p);
hence thesis by RFINSEQ:def 1;
end;
end;
let m be Nat;
cluster smid(p,m,n) -> plain;
coherence
proof
smid(p,m,n) = (p/^(m-'1))|(n+1-'m) by FINSEQ_8:def 1;
hence thesis;
end;
cluster (m,n)-cut p -> plain;
coherence
proof
per cases;
suppose 1 <= m & m <= n & n <= len p;
then 1 <= m & m <= len p & 1 <= n & n <= len p by XXREAL_0:2;
then m in dom p & n in dom p by FINSEQ_3:25;
then smid(p,m,n) = (m,n)-cut p by FINSEQ_8:29;
hence thesis;
end;
suppose not(1 <= m & m <= n & n <= len p);
hence thesis by FINSEQ_6:def 4;
end;
end;
end;
registration
let p, q be plain Graph-yielding FinSequence;
cluster p ^ q -> plain;
coherence
proof
for x being object st x in dom (p^q) ex G being _Graph st
G = (p^q).x & G is plain
proof
let x be object;
assume A1: x in dom (p^q);
then reconsider k = x as Nat;
per cases by A1, FINSEQ_1:25;
suppose k in dom p;
then (p^q).k = p.k & ex G being _Graph st p.k = G & G is plain
by Def1, FINSEQ_1:def 7;
hence ex G being _Graph st (p^q).x = G & G is plain;
end;
suppose ex n being Nat st n in dom q & k = len p + n;
then consider n being Nat such that
A2: n in dom q & k = len p + n;
(p^q).(len p + n) = q.n & ex G being _Graph st q.n = G & G is plain
by A2, Def1, FINSEQ_1:def 7;
hence ex G being _Graph st (p^q).x = G & G is plain by A2;
end;
end;
hence thesis;
end;
cluster p ^' q -> plain;
coherence
proof
p ^' q = p^(2,len q)-cut q by FINSEQ_6:def 5;
hence thesis;
end;
end;
registration
let G1, G2 be plain _Graph;
cluster <* G1, G2 *> -> plain;
coherence
proof
<* G1, G2 *> = <* G1 *> ^ <* G2 *> by FINSEQ_1:def 9;
hence thesis;
end;
let G3 be plain _Graph;
cluster <* G1, G2, G3 *> -> plain;
coherence
proof
<* G1, G2, G3 *> = <* G1 *> ^ <* G2 *> ^ <* G3 *> by FINSEQ_1:def 10;
hence thesis;
end;
end;
begin :: into GLIB_010
theorem Th81:
for G1, G2 being _Graph st G1 == G2
ex F being PGraphMapping of G1, G2 st F = id G1 & F is Disomorphism
proof
let G1, G2 be _Graph;
assume A1: G1 == G2;
then reconsider F = id G1 as PGraphMapping of G1, G2 by GLIB_010:11;
take F;
thus F = id G1;
dom F_V = the_Vertices_of G1 & dom F_E = the_Edges_of G1;
then A2: F is total by GLIB_010:def 11;
rng F_V = the_Vertices_of G2 & rng F_E = the_Edges_of G2
by A1, GLIB_000:def 34;
then A3: F is onto by GLIB_010:def 12;
F_V is one-to-one & F_E is one-to-one;
then A4: F is one-to-one by GLIB_010:def 13;
now
let e,v,w be object;
assume A5: e in dom F_E & v in dom F_V & w in dom F_V;
assume e DJoins v,w,G1;
then (id G1)_E.e DJoins (id G1)_V.v,(id G1)_V.w,G1 by A5, GLIB_010:def 14;
hence F_E.e DJoins F_V.v,F_V.w,G2 by A1, GLIB_000:88;
end;
then F is directed by GLIB_010:def 14;
hence F is Disomorphism by A2, A3, A4;
end;
theorem
for G1, G2 being _Graph st G1 == G2 holds G2 is G1-Disomorphic
proof
let G1, G2 be _Graph;
assume G1 == G2;
then consider F being PGraphMapping of G1, G2 such that
A1: F = id G1 & F is Disomorphism by Th81;
thus thesis by A1, GLIB_010:def 24;
end;
theorem Th83:
for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
ex F being PGraphMapping of G1, G2 st F = id G1 & F is isomorphism
proof
let G1 be _Graph, E be set, G2 be reverseEdgeDirections of G1, E;
reconsider F = id G1 as PGraphMapping of G1, G2 by GLIB_010:12;
take F;
thus F = id G1;
dom F_V = the_Vertices_of G1 & dom F_E = the_Edges_of G1;
then A1: F is total by GLIB_010:def 11;
rng F_V = the_Vertices_of G2 & rng F_E = the_Edges_of G2 by GLIB_007:4;
then A2: F is onto by GLIB_010:def 12;
F_V is one-to-one & F_E is one-to-one;
then F is one-to-one by GLIB_010:def 13;
hence F is isomorphism by A1, A2;
end;
theorem
for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
holds G2 is G1-isomorphic
proof
let G1 be _Graph, E be set, G2 be reverseEdgeDirections of G1, E;
consider F being PGraphMapping of G1, G2 such that
A1: F = id G1 & F is isomorphism by Th83;
thus thesis by A1, GLIB_010:def 23;
end;
:: correction of GLIB_010:90
theorem
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is Dcontinuous isomorphism holds
(G1 is non-Dmulti iff G2 is non-Dmulti) &
(G1 is Dsimple iff G2 is Dsimple)
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: F is Dcontinuous isomorphism;
then reconsider F0 = F as one-to-one PGraphMapping of G1, G2;
F0" is Dcontinuous isomorphism by A1, GLIB_010:74, GLIB_010:75;
hence thesis by A1, GLIB_010:50;
end;
theorem Th86:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st v in dom F_V
holds F_E.:(v.edgesInOut()) c= (F_V/.v).edgesInOut()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
let v be Vertex of G1;
assume A1: v in dom F_V;
now
let e be object;
assume e in F_E.:(v.edgesInOut());
then consider e0 being object such that
A2: e0 in dom F_E & e0 in v.edgesInOut() & e = F_E.e0 by FUNCT_1:def 6;
per cases by A2, GLIB_000:61;
suppose A3: (the_Source_of G1).e0 = v;
set w = (the_Target_of G1).e0;
A4: w in dom F_V by A2, GLIB_010:5;
e0 Joins v,w,G1 by A2, A3, GLIB_000:def 13;
then F_E.e0 Joins F_V.v,F_V.w,G2 by A1, A2, A4, GLIB_010:4;
then F_E.e0 Joins F_V/.v,F_V.w,G2 by A1, PARTFUN1:def 6;
hence e in (F_V/.v).edgesInOut() by A2, GLIB_000:62;
end;
suppose A5: (the_Target_of G1).e0 = v;
set w = (the_Source_of G1).e0;
A6: w in dom F_V by A2, GLIB_010:5;
e0 Joins v,w,G1 by A2, A5, GLIB_000:def 13;
then F_E.e0 Joins F_V.v,F_V.w,G2 by A1, A2, A6, GLIB_010:4;
then F_E.e0 Joins F_V/.v,F_V.w,G2 by A1, PARTFUN1:def 6;
hence e in (F_V/.v).edgesInOut() by A2, GLIB_000:62;
end;
end;
hence thesis by TARSKI:def 3;
end;
theorem Th87:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is directed & v in dom F_V holds
F_E.:(v.edgesIn()) c= (F_V/.v).edgesIn() &
F_E.:(v.edgesOut()) c= (F_V/.v).edgesOut()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
let v be Vertex of G1;
assume A1: F is directed & v in dom F_V;
now
let e be object;
assume e in F_E.:(v.edgesIn());
then consider e0 being object such that
A2: e0 in dom F_E & e0 in v.edgesIn() & e = F_E.e0 by FUNCT_1:def 6;
A3: (the_Target_of G1).e0 = v by A2, GLIB_000:56;
set w = (the_Source_of G1).e0;
A4: w in dom F_V by A2, GLIB_010:5;
e0 DJoins w,v,G1 by A2, A3, GLIB_000:def 14;
then F_E.e0 DJoins F_V.w,F_V.v,G2 by A1, A2, A4, GLIB_010:def 14;
then F_E.e0 DJoins F_V.w,F_V/.v,G2 by A1, PARTFUN1:def 6;
hence e in (F_V/.v).edgesIn() by A2, GLIB_000:57;
end;
hence F_E.:(v.edgesIn()) c= (F_V/.v).edgesIn() by TARSKI:def 3;
now
let e be object;
assume e in F_E.:(v.edgesOut());
then consider e0 being object such that
A5: e0 in dom F_E & e0 in v.edgesOut() & e = F_E.e0 by FUNCT_1:def 6;
A6: (the_Source_of G1).e0 = v by A5, GLIB_000:58;
set w = (the_Target_of G1).e0;
A7: w in dom F_V by A5, GLIB_010:5;
e0 DJoins v,w,G1 by A5, A6, GLIB_000:def 14;
then F_E.e0 DJoins F_V.v,F_V.w,G2 by A1, A5, A7, GLIB_010:def 14;
then F_E.e0 DJoins F_V/.v,F_V.w,G2 by A1, PARTFUN1:def 6;
hence e in (F_V/.v).edgesOut() by A5, GLIB_000:59;
end;
hence F_E.:(v.edgesOut()) c= (F_V/.v).edgesOut() by TARSKI:def 3;
end;
theorem Th88:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is onto semi-continuous & v in dom F_V
holds F_E.:(v.edgesInOut()) = (F_V/.v).edgesInOut()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2, v be Vertex of G1;
assume A1: F is onto semi-continuous & v in dom F_V;
then A2: F_E.:(v.edgesInOut()) c= (F_V/.v).edgesInOut() by Th86;
now
let e9 be object;
assume A3: e9 in (F_V/.v).edgesInOut();
then e9 in the_Edges_of G2;
then e9 in rng F_E by A1, GLIB_010:def 12;
then consider e being object such that
A4: e in dom F_E & F_E.e = e9 by FUNCT_1:def 3;
per cases by A3, GLIB_000:61;
suppose A5: (the_Source_of G2).e9 = F_V/.v;
set w9 = (the_Target_of G2).e9;
A6: F_E.e Joins F_V/.v,w9,G2 by A3, A4, A5, GLIB_000:def 13;
then w9 in the_Vertices_of G2 by GLIB_000:13;
then w9 in rng F_V by A1, GLIB_010:def 12;
then consider w being object such that
A7: w in dom F_V & F_V.w = w9 by FUNCT_1:def 3;
F_E.e Joins F_V.v,F_V.w,G2 by A1, A6, A7, PARTFUN1:def 6;
then e in v.edgesInOut() by A1, A4, A7, GLIB_010:def 15, GLIB_000:62;
hence e9 in F_E.:(v.edgesInOut()) by A4, FUNCT_1:def 6;
end;
suppose A8: (the_Target_of G2).e9 = F_V/.v;
set w9 = (the_Source_of G2).e9;
A9: F_E.e Joins F_V/.v,w9,G2 by A3, A4, A8, GLIB_000:def 13;
then w9 in the_Vertices_of G2 by GLIB_000:13;
then w9 in rng F_V by A1, GLIB_010:def 12;
then consider w being object such that
A10: w in dom F_V & F_V.w = w9 by FUNCT_1:def 3;
F_E.e Joins F_V.v,F_V.w,G2 by A1, A9, A10, PARTFUN1:def 6;
then e in v.edgesInOut() by A1, A4, A10, GLIB_010:def 15, GLIB_000:62;
hence e9 in F_E.:(v.edgesInOut()) by A4, FUNCT_1:def 6;
end;
end;
then (F_V/.v).edgesInOut() c= F_E.:(v.edgesInOut()) by TARSKI:def 3;
hence thesis by A2, XBOOLE_0:def 10;
end;
theorem Th89:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is onto semi-Dcontinuous & v in dom F_V holds
F_E.:(v.edgesIn()) = (F_V/.v).edgesIn() &
F_E.:(v.edgesOut()) = (F_V/.v).edgesOut()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2, v be Vertex of G1;
assume A1: F is onto semi-Dcontinuous & v in dom F_V;
then A2: F_E.:(v.edgesIn()) c= (F_V/.v).edgesIn() &
F_E.:(v.edgesOut()) c= (F_V/.v).edgesOut() by Th87;
now
let e9 be object;
assume A3: e9 in (F_V/.v).edgesIn();
then e9 in the_Edges_of G2;
then e9 in rng F_E by A1, GLIB_010:def 12;
then consider e being object such that
A4: e in dom F_E & F_E.e = e9 by FUNCT_1:def 3;
A5: (the_Target_of G2).e9 = F_V/.v by A3, GLIB_000:56;
set w9 = (the_Source_of G2).e9;
A6: F_E.e DJoins w9,F_V/.v,G2 by A3, A4, A5, GLIB_000:def 14;
then F_E.e Joins w9,F_V/.v,G2 by GLIB_000:16;
then w9 in the_Vertices_of G2 by GLIB_000:13;
then w9 in rng F_V by A1, GLIB_010:def 12;
then consider w being object such that
A7: w in dom F_V & F_V.w = w9 by FUNCT_1:def 3;
F_E.e DJoins F_V.w,F_V.v,G2 by A1, A6, A7, PARTFUN1:def 6;
then A8: e DJoins w,v,G1 by A1, A4, A7, GLIB_010:def 17;
e is set & w is set by TARSKI:1;
then e in v.edgesIn() by A8, GLIB_000:57;
hence e9 in F_E.:(v.edgesIn()) by A4, FUNCT_1:def 6;
end;
then (F_V/.v).edgesIn() c= F_E.:(v.edgesIn()) by TARSKI:def 3;
hence F_E.:(v.edgesIn()) = (F_V/.v).edgesIn() by A2, XBOOLE_0:def 10;
now
let e9 be object;
assume A9: e9 in (F_V/.v).edgesOut();
then e9 in the_Edges_of G2;
then e9 in rng F_E by A1, GLIB_010:def 12;
then consider e being object such that
A10: e in dom F_E & F_E.e = e9 by FUNCT_1:def 3;
A11: (the_Source_of G2).e9 = F_V/.v by A9, GLIB_000:58;
set w9 = (the_Target_of G2).e9;
A12: F_E.e DJoins F_V/.v,w9,G2 by A9, A10, A11, GLIB_000:def 14;
then F_E.e Joins F_V/.v,w9,G2 by GLIB_000:16;
then w9 in the_Vertices_of G2 by GLIB_000:13;
then w9 in rng F_V by A1, GLIB_010:def 12;
then consider w being object such that
A13: w in dom F_V & F_V.w = w9 by FUNCT_1:def 3;
F_E.e DJoins F_V.v,F_V.w,G2 by A1, A12, A13, PARTFUN1:def 6;
then A14: e DJoins v,w,G1 by A1, A10, A13, GLIB_010:def 17;
e is set & w is set by TARSKI:1;
then e in v.edgesOut() by A14, GLIB_000:59;
hence e9 in F_E.:(v.edgesOut()) by A10, FUNCT_1:def 6;
end;
then (F_V/.v).edgesOut() c= F_E.:(v.edgesOut()) by TARSKI:def 3;
hence F_E.:(v.edgesOut()) = (F_V/.v).edgesOut() by A2, XBOOLE_0:def 10;
end;
theorem
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is isomorphism
holds F_E.:(v.edgesInOut()) = (F_V/.v).edgesInOut()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
let v be Vertex of G1;
assume A1: F is isomorphism;
then dom F_V = the_Vertices_of G1 by GLIB_010:def 11;
hence thesis by A1, Th88;
end;
theorem
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is Disomorphism holds
F_E.:(v.edgesIn()) = (F_V/.v).edgesIn() &
F_E.:(v.edgesOut()) = (F_V/.v).edgesOut()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
let v be Vertex of G1;
assume A1: F is Disomorphism;
then dom F_V = the_Vertices_of G1 by GLIB_010:def 11;
hence thesis by A1, Th89;
end;
registration
let G1 be _Graph, G2 be edgeless _Graph;
cluster -> directed for PGraphMapping of G1, G2;
coherence
proof
let F be PGraphMapping of G1, G2;
for e,v,w being object st e in dom F_E & v in dom F_V & w in dom F_V
holds e DJoins v,w,G1 implies F_E.e DJoins F_V.v, F_V.w, G2;
hence thesis by GLIB_010:def 14;
end;
end;
theorem Th92:
for G1, G2 being _Graph, F0 being PGraphMapping of G1, G2
st F0_E is one-to-one
ex E being Subset of the_Edges_of G2 st
for G3 being reverseEdgeDirections of G2, E
ex F being PGraphMapping of G1, G3 st F = F0 & F is directed &
(F0 is non empty implies F is non empty) &
(F0 is total implies F is total) &
(F0 is one-to-one implies F is one-to-one) &
(F0 is onto implies F is onto) &
(F0 is semi-continuous implies F is semi-continuous) &
(F0 is continuous implies F is continuous)
proof
let G1, G2 be _Graph, F0 be PGraphMapping of G1, G2;
assume A1: F0_E is one-to-one;
per cases;
suppose the_Edges_of G2 <> {};
set E = {e9 where e9 is Element of the_Edges_of G2 : e9 in rng F0_E &
for e being object st e in dom F0_E & F0_E.e = e9 holds e9 DJoins
F0_V.((the_Target_of G1).e), F0_V.((the_Source_of G1).e), G2};
now
let x be object;
assume x in E;
then consider e9 being Element of the_Edges_of G2 such that
A2: x = e9 and
A3: e9 in rng F0_E and
for e being object st e in dom F0_E & F0_E.e = e9 holds e9 DJoins
F0_V.((the_Target_of G1).e), F0_V.((the_Source_of G1).e), G2;
e9 in the_Edges_of G2 by A3;
hence x in the_Edges_of G2 by A2;
end;
then reconsider E as Subset of the_Edges_of G2 by TARSKI:def 3;
take E;
let G3 be reverseEdgeDirections of G2, E;
consider F9 being PGraphMapping of G2, G3 such that
A4: F9 = id G2 & F9 is isomorphism by Th83;
take F9*F0;
thus A5: F9 * F0 = (id G2) * F0 by A4 .= F0 by GLIB_010:116;
now
let e,v,w be object;
assume e in dom (F9*F0)_E & v in dom (F9*F0)_V & w in dom (F9*F0)_V;
then A6: e in dom F0_E & v in dom F0_V & w in dom F0_V by A5;
assume A7: e DJoins v,w,G1;
A8: F0_E.e in rng F0_E by A6, FUNCT_1:3;
then reconsider e9 = F0_E.e as Element of the_Edges_of G2;
per cases;
suppose A11: e9 in E;
then consider e8 being Element of the_Edges_of G2 such that
A12: e8 = e9 & e8 in rng F0_E and
A13: for e0 being object st e0 in dom F0_E & F0_E.e0 = e8 holds
e8 DJoins F0_V.((the_Target_of G1).e0),
F0_V.((the_Source_of G1).e0), G2;
A14: e9 DJoins F0_V.((the_Target_of G1).e),
F0_V.((the_Source_of G1).e), G2 by A6, A12, A13;
(the_Source_of G1).e = v & (the_Target_of G1).e = w
by A7, GLIB_000:def 14;
then F0_E.e DJoins F0_V.v,F0_V.w,G3 by A11, A14, GLIB_007:7;
hence (F9*F0)_E.e DJoins (F9*F0)_V.v,(F9*F0)_V.w,G3 by A5;
end;
suppose A15: not e9 in E;
e Joins v,w,G1 by A7, GLIB_000:16;
then A16: F0_E.e Joins F0_V.v,F0_V.w,G2 by A6, GLIB_010:4;
not F0_E.e DJoins F0_V.w,F0_V.v,G2
proof
assume A17: F0_E.e DJoins F0_V.w,F0_V.v,G2;
for e0 being object st e0 in dom F0_E & F0_E.e0 = e9 holds e9 DJoins
F0_V.((the_Target_of G1).e0), F0_V.((the_Source_of G1).e0), G2
proof
let e0 be object;
assume e0 in dom F0_E & F0_E.e0 = e9;
then e = e0 by A1, A6, FUNCT_1:def 4;
then (the_Source_of G1).e0 = v & (the_Target_of G1).e0 = w
by A7, GLIB_000:def 14;
hence thesis by A17;
end;
hence contradiction by A8, A15;
end;
then F0_E.e DJoins F0_V.v,F0_V.w,G2 by A16, GLIB_000:16;
then F0_E.e DJoins F0_V.v,F0_V.w,G3 by A15, GLIB_007:8;
hence (F9*F0)_E.e DJoins (F9*F0)_V.v,(F9*F0)_V.w,G3 by A5;
end;
end;
hence F9*F0 is directed by GLIB_010:def 14;
thus F0 is non empty implies F9*F0 is non empty by A5;
thus thesis by A4, GLIB_010:104, GLIB_010:106;
end;
suppose A18: the_Edges_of G2 = {};
take E = {}the_Edges_of G2;
let G3 be reverseEdgeDirections of G2, E;
consider F9 being PGraphMapping of G2, G3 such that
A19: F9 = id G2 & F9 is isomorphism by Th83;
take F9*F0;
thus A20: F9 * F0 = (id G2) * F0 by A19 .= F0 by GLIB_010:116;
the_Edges_of G3 = {} by A18, GLIB_007:4;
then G3 is edgeless;
hence F9*F0 is directed;
thus F0 is non empty implies F9*F0 is non empty by A20;
thus thesis by A19, GLIB_010:104, GLIB_010:106;
end;
end;
theorem Th93:
for G1, G2 being _Graph, F0 being PGraphMapping of G1, G2
st F0_E is one-to-one
ex E being Subset of the_Edges_of G2 st
for G3 being reverseEdgeDirections of G2, E
ex F being PGraphMapping of G1, G3 st F = F0 & F is directed &
(F0 is weak_SG-embedding implies F is weak_SG-embedding) &
(F0 is strong_SG-embedding implies F is strong_SG-embedding) &
(F0 is isomorphism implies F is isomorphism)
proof
let G1, G2 be _Graph, F0 be PGraphMapping of G1, G2;
assume F0_E is one-to-one;
then consider E being Subset of the_Edges_of G2 such that
A1: for G3 being reverseEdgeDirections of G2, E
ex F being PGraphMapping of G1, G3 st F = F0 & F is directed &
(F0 is non empty implies F is non empty) &
(F0 is total implies F is total) &
(F0 is one-to-one implies F is one-to-one) &
(F0 is onto implies F is onto) &
(F0 is semi-continuous implies F is semi-continuous) &
(F0 is continuous implies F is continuous) by Th92;
take E;
let G3 be reverseEdgeDirections of G2, E;
consider F being PGraphMapping of G1, G3 such that
A2: F = F0 & F is directed and
F0 is non empty implies F is non empty and
A3: F0 is total implies F is total and
A4: F0 is one-to-one implies F is one-to-one and
A5: F0 is onto implies F is onto and
F0 is semi-continuous implies F is semi-continuous and
A6: F0 is continuous implies F is continuous by A1;
take F;
thus F = F0 & F is directed by A2;
thus thesis by A3, A4, A5, A6;
end;
theorem Th94:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is directed weak_SG-embedding holds
v.inDegree() c= (F_V/.v).inDegree() &
v.outDegree() c= (F_V/.v).outDegree()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2, v be Vertex of G1;
assume A1: F is directed weak_SG-embedding;
then A2: dom F_E = the_Edges_of G1 by GLIB_010:def 11;
set f = F_E|(v.edgesIn());
A3: dom f = dom F_E /\ v.edgesIn() by RELAT_1:61
.= v.edgesIn() by A2, XBOOLE_1:28;
A4: rng f = F_E.:(v.edgesIn()) by RELAT_1:115;
dom F_V = the_Vertices_of G1 by A1, GLIB_010:def 11;
then F_E.:(v.edgesIn()) c= (F_V/.v).edgesIn() by A1, Th87;
then A5: card(F_E.:(v.edgesIn())) c= card (F_V/.v).edgesIn() by CARD_1:11;
f is one-to-one by A1, FUNCT_1:52;
hence v.inDegree() c= (F_V/.v).inDegree() by A3, A4, A5, CARD_1:70;
set f = F_E|(v.edgesOut());
A6: dom f = dom F_E /\ v.edgesOut() by RELAT_1:61
.= v.edgesOut() by A2, XBOOLE_1:28;
A7: rng f = F_E.:(v.edgesOut()) by RELAT_1:115;
dom F_V = the_Vertices_of G1 by A1, GLIB_010:def 11;
then F_E.:(v.edgesOut()) c= (F_V/.v).edgesOut() by A1, Th87;
then A8: card(F_E.:(v.edgesOut())) c= card (F_V/.v).edgesOut() by CARD_1:11;
f is one-to-one by A1, FUNCT_1:52;
hence v.outDegree() c= (F_V/.v).outDegree() by A6, A7, A8, CARD_1:70;
end;
Lm5:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is directed weak_SG-embedding
holds v.degree() c= (F_V/.v).degree()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2, v be Vertex of G1;
assume F is directed weak_SG-embedding;
then v.inDegree() c= (F_V/.v).inDegree() &
v.outDegree() c= (F_V/.v).outDegree() by Th94;
hence thesis by CARD_2:83;
end;
theorem
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is weak_SG-embedding
holds v.degree() c= (F_V/.v).degree()
proof
let G1, G2 be _Graph, F0 be PGraphMapping of G1, G2, v be Vertex of G1;
assume A1: F0 is weak_SG-embedding;
then F0_E is one-to-one;
then consider E being Subset of the_Edges_of G2 such that
A2: for G3 being reverseEdgeDirections of G2, E
ex F being PGraphMapping of G1, G3 st F = F0 & F is directed &
(F0 is weak_SG-embedding implies F is weak_SG-embedding) &
(F0 is strong_SG-embedding implies F is strong_SG-embedding) &
(F0 is isomorphism implies F is isomorphism) by Th93;
set G3 = the reverseEdgeDirections of G2, E;
consider F be PGraphMapping of G1, G3 such that
A3: F = F0 & F is directed and
A4: F0 is weak_SG-embedding implies F is weak_SG-embedding and
(F0 is strong_SG-embedding implies F is strong_SG-embedding) &
(F0 is isomorphism implies F is isomorphism) by A2;
A5: v.degree() c= (F_V/.v).degree() by A1, A3, A4, Lm5;
dom F_V = the_Vertices_of G1 by A1, A4, GLIB_010:def 11;
then A6: v in dom F_V & v in dom F0_V by A3;
F0_V/.v = F0_V.v by A6, PARTFUN1:def 6
.= F_V/.v by A3, A6, PARTFUN1:def 6;
hence thesis by A5, Th60;
end;
theorem Th96:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is onto semi-Dcontinuous & v in dom F_V holds
(F_V/.v).inDegree() c= v.inDegree() &
(F_V/.v).outDegree() c= v.outDegree()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2, v being Vertex of G1;
assume F is onto semi-Dcontinuous & v in dom F_V;
then F_E.:(v.edgesIn()) = (F_V/.v).edgesIn() &
F_E.:(v.edgesOut()) = (F_V/.v).edgesOut() by Th89;
hence thesis by CARD_1:67;
end;
:: Can this theorem and all using it be improved to semi-continuous?
theorem
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is onto semi-Dcontinuous & v in dom F_V
holds (F_V/.v).degree() c= v.degree()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2, v be Vertex of G1;
assume F is onto semi-Dcontinuous & v in dom F_V;
then (F_V/.v).inDegree() c= v.inDegree() &
(F_V/.v).outDegree() c= v.outDegree() by Th96;
hence thesis by CARD_2:83;
end;
theorem Th98:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is Disomorphism holds
v.inDegree() = (F_V/.v).inDegree() & v.outDegree() = (F_V/.v).outDegree()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
let v be Vertex of G1;
assume A1: F is Disomorphism;
then dom F_V = the_Vertices_of G1 by GLIB_010:def 11;
then A2: (F_V/.v).inDegree() c= v.inDegree() &
(F_V/.v).outDegree() c= v.outDegree() by A1, Th96;
v.inDegree() c= (F_V/.v).inDegree() & v.outDegree() c= (F_V/.v).outDegree()
by A1, Th94;
hence thesis by A2, XBOOLE_0:def 10;
end;
theorem Th99:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is isomorphism
holds v.degree() = (F_V/.v).degree()
proof
let G1, G2 be _Graph, F0 be PGraphMapping of G1, G2;
let v be Vertex of G1;
assume A1: F0 is isomorphism;
then F0_E is one-to-one;
then consider E being Subset of the_Edges_of G2 such that
A2: for G3 being reverseEdgeDirections of G2, E
ex F being PGraphMapping of G1, G3 st F = F0 & F is directed &
(F0 is weak_SG-embedding implies F is weak_SG-embedding) &
(F0 is strong_SG-embedding implies F is strong_SG-embedding) &
(F0 is isomorphism implies F is isomorphism) by Th93;
set G3 = the reverseEdgeDirections of G2, E;
consider F being PGraphMapping of G1, G3 such that
A3: F = F0 & F is directed and
(F0 is weak_SG-embedding implies F is weak_SG-embedding) &
(F0 is strong_SG-embedding implies F is strong_SG-embedding) and
A4: (F0 is isomorphism implies F is isomorphism) by A2;
v.inDegree()=(F_V/.v).inDegree() & v.outDegree()=(F_V/.v).outDegree()
by A1, A3, A4, Th98;
then A5: (F_V/.v).degree() = v.degree();
F0 is total & dom(F_V) = dom(F0_V) & v in the_Vertices_of G1 by A1, A3;
then A6: v in dom F0_V & v in dom F_V by GLIB_010:def 11;
F0_V/.v = F0_V.v by A6, PARTFUN1:def 6
.= F_V/.v by A3, A6, PARTFUN1:def 6;
hence thesis by A5, Th60;
end;
begin :: into CHORD
theorem Th100:
for G being _Graph, u,v,w being Vertex of G st v is endvertex & u <> w
holds not u,v are_adjacent or not v,w are_adjacent
proof
let G be _Graph, u,v,w being Vertex of G;
assume A1: v is endvertex & u <> w;
assume A2: u,v are_adjacent;
consider e being object such that
A3: v.edgesInOut() = {e} & not e Joins v,v,G by A1, GLIB_000:def 51;
e in v.edgesInOut() by A3, TARSKI:def 1;
then consider v9 being Vertex of G such that
A4: e Joins v,v9,G by GLIB_000:64;
consider e8 being object such that
A5: e8 Joins v,u,G by A2, CHORD:def 3;
e8 is set by TARSKI:1;
then e8 in v.edgesInOut() by A5, GLIB_000:64;
then e8 = e by A3, TARSKI:def 1;
then A6: v = v & v9 = u or v = u & v9 = v by A4, A5, GLIB_000:15;
not ex e9 being object st e9 Joins v,w,G
proof
given e9 being object such that
A7: e9 Joins v,w,G;
e9 is set by TARSKI:1;
then e9 in v.edgesInOut() by A7, GLIB_000:64;
then e9 = e by A3, TARSKI:def 1;
then v = v & w = v9 or v = v9 & w = v by A4, A7, GLIB_000:15;
hence contradiction by A1, A6;
end;
hence not v,w are_adjacent by CHORD:def 3;
end;
theorem Th101:
for G being _Graph, v being Vertex of G st 3 c= G.order() & v is endvertex
ex u,w being Vertex of G
st u <> v & w <> v & u <> w & u,v are_adjacent & not v,w are_adjacent
proof
let G be _Graph, v be Vertex of G;
assume A1: 3 c= G.order() & v is endvertex;
then A2: 3 c= card the_Vertices_of G;
consider e being object such that
A3: v.edgesInOut() = {e} & not e Joins v,v,G by A1, GLIB_000:def 51;
e in v.edgesInOut() by A3, TARSKI:def 1;
then consider u being Vertex of G such that
A4: e Joins v,u,G by GLIB_000:64;
consider w being object such that
A5: w in the_Vertices_of G & w <> v & w <> u by A2, PENCIL_1:6;
reconsider w as Vertex of G by A5;
take u,w;
thus u <> v & w <> v & u <> w by A3, A4, A5;
thus u,v are_adjacent by A4, CHORD:def 3;
hence not v,w are_adjacent by A1, A5, Th100;
end;
theorem
for G being _Graph, v being Vertex of G st 4 c= G.order() & v is endvertex
ex x,y,z being Vertex of G
st v <> x & v <> y & v <> z & x <> y & x <> z & y <> z & v,x are_adjacent &
not v,y are_adjacent & not v,z are_adjacent
proof
let G be _Graph, v be Vertex of G;
assume A1: 4 c= G.order() & v is endvertex;
Segm 3 c= Segm 4 by NAT_1:39;
then consider x,y being Vertex of G such that
A2: x <> v & y <> v & x <> y & x,v are_adjacent & not v,y are_adjacent
by A1, Th101, XBOOLE_1:1;
consider z being object such that
A3: z in the_Vertices_of G & v <> z & x <> z & y <> z by A1, Th21;
reconsider z as Vertex of G by A3;
take x,y,z;
thus v <> x & v <> y & v <> z & x <> y & x <> z & y <> z by A2, A3;
thus v,x are_adjacent by A2;
thus not v,y are_adjacent by A2;
thus not v,z are_adjacent by A1, A2, A3, Th100;
end;
definition
let GF be Graph-yielding Function;
attr GF is chordal means
:Def4:
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is chordal;
end;
registration
let G be chordal _Graph;
cluster <* G *> -> chordal;
coherence
proof
let x be object;
assume A1: x in dom <* G *>;
then reconsider n = x as Nat;
1 <= n <= len <* G *> by A1, FINSEQ_3:25;
then 1 <= n <= 1 by FINSEQ_1:40;
then n = 1 by XXREAL_0:1;
hence thesis;
end;
cluster NAT --> G -> chordal;
coherence by FUNCOP_1:7;
end;
definition
let GF be non empty Graph-yielding Function;
redefine attr GF is chordal means :: redefines chordal (GLIBPRE0, definition)
:Def5:
for x being Element of dom GF holds GF.x is chordal;
compatibility
proof
hereby
assume A1: GF is chordal;
let x be Element of dom GF;
ex G being _Graph st GF.x = G & G is chordal by A1;
hence GF.x is chordal;
end;
assume A3: for x being Element of dom GF holds GF.x is chordal;
let x be object;
assume x in dom GF;
then reconsider y = x as Element of dom GF;
take GF.y;
thus thesis by A3;
end;
end;
definition
let GSq be GraphSeq;
redefine attr GSq is chordal means :: redefines chordal (GLIBPRE0, redefinition) → chordal (GLIBPRE0, definition)
:Def6:
for n being Nat holds GSq.n is chordal;
compatibility
proof
hereby
assume A1: GSq is chordal;
let x be Nat;
x in dom GSq by Lm4;
hence GSq.x is chordal by A1;
end;
assume A2: for x being Nat holds GSq.x is chordal;
let x be Element of dom GSq;
thus thesis by A2;
end;
end;
registration
cluster empty -> chordal for Graph-yielding Function;
coherence;
end;
registration
cluster chordal for GraphSeq;
existence
proof
take NAT --> the chordal _Graph;
thus thesis;
end;
cluster non empty chordal for Graph-yielding FinSequence;
existence
proof
take <* the chordal _Graph *>;
thus thesis;
end;
end;
registration
let GF be chordal non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> chordal;
coherence by Def5;
end;
registration
let GSq be chordal GraphSeq, x be Nat;
cluster GSq.x -> chordal;
coherence by Def6;
end;
registration
let p be chordal Graph-yielding FinSequence, n be Nat;
cluster p | n -> chordal;
coherence
proof
A1: p|n = p|Seg n by FINSEQ_1:def 16;
now
let x be object;
assume A2: x in dom(p|n);
then x in dom p by A1, RELAT_1:60, TARSKI:def 3;
then consider G being _Graph such that
A3: p.x = G & G is chordal by Def4;
take G;
thus (p|n).x = G & G is chordal by A1, A3, A2, FUNCT_1:47;
end;
hence thesis;
end;
cluster p /^ n -> chordal;
coherence
proof
per cases;
suppose A4: n <= len p;
now
let x be object;
assume A5: x in dom(p /^ n);
then reconsider i = x as Nat;
n+i in dom p by A5, FINSEQ_5:26;
then consider G being _Graph such that
A6: p.(n+i) = G & G is chordal by Def4;
take G;
thus (p /^ n).x = G & G is chordal by A4, A5, A6, RFINSEQ:def 1;
end;
hence thesis;
end;
suppose not (n <= len p);
hence thesis by RFINSEQ:def 1;
end;
end;
let m be Nat;
cluster smid(p,m,n) -> chordal;
coherence
proof
smid(p,m,n) = (p/^(m-'1))|(n+1-'m) by FINSEQ_8:def 1;
hence thesis;
end;
cluster (m,n)-cut p -> chordal;
coherence
proof
per cases;
suppose 1 <= m & m <= n & n <= len p;
then 1 <= m & m <= len p & 1 <= n & n <= len p by XXREAL_0:2;
then m in dom p & n in dom p by FINSEQ_3:25;
then smid(p,m,n) = (m,n)-cut p by FINSEQ_8:29;
hence thesis;
end;
suppose not(1 <= m & m <= n & n <= len p);
hence thesis by FINSEQ_6:def 4;
end;
end;
end;
registration
let p, q be chordal Graph-yielding FinSequence;
cluster p ^ q -> chordal;
coherence
proof
for x being object st x in dom (p^q) ex G being _Graph st
G = (p^q).x & G is chordal
proof
let x be object;
assume A1: x in dom (p^q);
then reconsider k = x as Nat;
per cases by A1, FINSEQ_1:25;
suppose k in dom p;
then (p^q).k = p.k & ex G being _Graph st p.k = G & G is chordal
by Def4, FINSEQ_1:def 7;
hence ex G being _Graph st (p^q).x = G & G is chordal;
end;
suppose ex n being Nat st n in dom q & k = len p + n;
then consider n being Nat such that
A2: n in dom q & k = len p + n;
(p^q).(len p + n) = q.n & ex G being _Graph st q.n = G & G is chordal
by A2, Def4, FINSEQ_1:def 7;
hence ex G being _Graph st (p^q).x = G & G is chordal by A2;
end;
end;
hence thesis;
end;
cluster p ^' q -> chordal;
coherence
proof
p ^' q = p^(2,len q)-cut q by FINSEQ_6:def 5;
hence thesis;
end;
end;
registration
let G1, G2 be chordal _Graph;
cluster <* G1, G2 *> -> chordal;
coherence
proof
<* G1, G2 *> = <* G1 *> ^ <* G2 *> by FINSEQ_1:def 9;
hence thesis;
end;
let G3 be chordal _Graph;
cluster <* G1, G2, G3 *> -> chordal;
coherence
proof
<* G1, G2, G3 *> = <* G1 *> ^ <* G2 *> ^ <* G3 *> by FINSEQ_1:def 10;
hence thesis;
end;
end;
begin :: into GLIB_011
theorem
for G1, G2 being non-Dmulti _Graph, f being directed PVertexMapping of G1, G2
for v being Vertex of G1 st f is Disomorphism holds
v.inDegree() = (f/.v).inDegree() & v.outDegree() = (f/.v).outDegree()
proof
let G1, G2 be non-Dmulti _Graph, f be directed PVertexMapping of G1, G2;
let v be Vertex of G1;
assume f is Disomorphism;
then A1: DPVM2PGM(f) is Disomorphism by GLIB_011:48;
thus v.inDegree() = ((DPVM2PGM f)_V/.v).inDegree() by A1, Th98
.= (f/.v).inDegree();
thus v.outDegree() = ((DPVM2PGM f)_V/.v).outDegree() by A1, Th98
.= (f/.v).outDegree();
end;
theorem
for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2
for v being Vertex of G1 st f is isomorphism
holds v.degree() = (f/.v).degree()
proof
let G1, G2 be non-multi _Graph, f be PVertexMapping of G1, G2;
let v be Vertex of G1;
assume f is isomorphism;
hence v.degree() = ((PVM2PGM f)_V/.v).degree() by Th99, GLIB_011:47
.= (f/.v).degree();
end;