:: Alternative Graph Structures
:: by Gilbert Lee and Piotr Rudnicki
::
:: Received February 22, 2005
:: Copyright (c) 2005-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, FINSET_1, RELAT_1, FUNCT_1, XBOOLE_0, TARSKI, SUBSET_1,
FINSEQ_1, NAT_1, FUNCT_4, FUNCOP_1, ZFMISC_1, CARD_1, ARYTM_3, CARD_2,
ORDINAL2, XXREAL_0, PBOOLE, GLIB_000, XCMPLX_0;
notations TARSKI, XBOOLE_0, DOMAIN_1, SUBSET_1, PBOOLE, RELAT_1, CARD_1,
CARD_2, FUNCT_1, RELSET_1, FINSEQ_1, FINSET_1, ORDINAL1, XCMPLX_0, NAT_1,
FUNCT_2, FUNCOP_1, FUNCT_4, ORDINAL2, FINSEQ_4, NUMBERS, XXREAL_0;
constructors DOMAIN_1, FUNCT_4, XXREAL_0, NAT_1, NAT_D, BINOP_2, CARD_2,
FINSEQ_4, PBOOLE, ORDINAL3, WELLORD2, PARTFUN1, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
FINSET_1, XREAL_0, NAT_1, CARD_1, FINSEQ_1, FINSEQ_4, FUNCT_2, PARTFUN1,
RELSET_1;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
definitions TARSKI, RELAT_1;
equalities FUNCOP_1;
expansions TARSKI;
theorems CARD_1, CARD_2, FUNCOP_1, ENUMSET1, FINSEQ_1, FUNCT_1, FUNCT_2,
FUNCT_4, NAT_1, RELAT_1, FINSEQ_4, TARSKI, XBOOLE_0, XBOOLE_1, ZFMISC_1,
XREAL_1, XXREAL_0, ORDINAL1, RELSET_1, PARTFUN1, WELLORD2, SUBSET_1;
schemes NAT_1, SUBSET_1, FUNCT_1;
begin :: Definitions
registration
cluster finite NAT-defined for Function;
existence
proof
take {};
thus {} is finite;
thus dom {} c= NAT;
end;
end;
definition
mode GraphStruct is finite NAT-defined Function;
end;
definition
func VertexSelector -> Element of NAT equals
1;
coherence;
func EdgeSelector -> Element of NAT equals
2;
coherence;
func SourceSelector -> Element of NAT equals
3;
coherence;
func TargetSelector -> Element of NAT equals
4;
coherence;
end;
definition
func _GraphSelectors -> non empty Subset of NAT equals
{VertexSelector,
EdgeSelector, SourceSelector, TargetSelector};
coherence;
end;
definition
let G be GraphStruct;
func the_Vertices_of G -> set equals
G.VertexSelector;
coherence;
func the_Edges_of G -> set equals
G.EdgeSelector;
coherence;
func the_Source_of G -> set equals
G.SourceSelector;
coherence;
func the_Target_of G -> set equals
G.TargetSelector;
coherence;
end;
definition
let G be GraphStruct;
attr G is [Graph-like] means
:Def10:
VertexSelector in dom G & EdgeSelector in dom G &
SourceSelector in dom G & TargetSelector in dom G &
the_Vertices_of G is non empty set &
the_Source_of G is Function of the_Edges_of G, the_Vertices_of G &
the_Target_of G is Function of the_Edges_of G, the_Vertices_of G;
end;
registration
cluster [Graph-like] for GraphStruct;
existence
proof
set V = {1}, E = {};
reconsider S = {} as Function of E,V by RELSET_1:12;
set G = <*V,E,S,S*>;
len G=4 by FINSEQ_4:76;
then
A1: dom G = Seg 4 by FINSEQ_1:def 3;
reconsider G as GraphStruct;
A2: SourceSelector in dom G & TargetSelector in dom G by A1,FINSEQ_1:1;
VertexSelector in dom G & EdgeSelector in dom G by A1,FINSEQ_1:1;
then G is [Graph-like] by A2;
hence thesis;
end;
end;
definition
mode _Graph is [Graph-like] GraphStruct;
end;
registration
let G be _Graph;
cluster the_Vertices_of G -> non empty;
coherence by Def10;
end;
definition
let G be _Graph;
redefine func the_Source_of G -> Function of the_Edges_of G,the_Vertices_of :: redefines the_Source_of (GLIB_000, definition)
G;
coherence by Def10;
redefine func the_Target_of G -> Function of the_Edges_of G,the_Vertices_of :: redefines the_Target_of (GLIB_000, definition)
G;
coherence by Def10;
end;
definition
let V be non empty set,E be set, S,T be Function of E,V;
func createGraph(V,E,S,T) -> _Graph equals
<* V, E, S, T *>;
coherence
proof
set G = <*V,E,S,T*>;
len G = 4 by FINSEQ_4:76;
then
A1: dom G = Seg 4 by FINSEQ_1:def 3;
reconsider G as GraphStruct;
A2: SourceSelector in dom G & TargetSelector in dom G by A1,FINSEQ_1:1;
A3: the_Vertices_of G = V & the_Edges_of G = E;
A4: the_Source_of G = S & the_Target_of G = T;
VertexSelector in dom G & EdgeSelector in dom G by A1,FINSEQ_1:1;
hence thesis by A3,A4,A2,Def10;
end;
end;
definition
let G be GraphStruct, n be Nat, x be set;
func G.set(n,x) -> GraphStruct equals
G +* (n .--> x);
coherence
proof
set IT = G +* (n .--> x);
n in NAT by ORDINAL1:def 12;
then
A2: {n} c= NAT by ZFMISC_1:31;
dom IT = dom G \/ dom (n .--> x) & dom G c= NAT by FUNCT_4:def 1;
then dom IT c= NAT by A2,XBOOLE_1:8;
hence thesis by RELAT_1:def 18;
end;
end;
Lm1: for GS being GraphStruct holds GS is [Graph-like] iff _GraphSelectors c=
dom GS & the_Vertices_of GS is non empty & the_Source_of GS is Function of
the_Edges_of GS,the_Vertices_of GS & the_Target_of GS is Function of
the_Edges_of GS,the_Vertices_of GS
proof
let GS be GraphStruct;
now
thus VertexSelector in dom GS & EdgeSelector in dom GS &
SourceSelector in dom GS & TargetSelector in dom GS
implies _GraphSelectors c= dom GS by ENUMSET1:def 2;
A1: VertexSelector in _GraphSelectors & EdgeSelector in _GraphSelectors
by ENUMSET1:def 2;
A2: SourceSelector in _GraphSelectors & TargetSelector in _GraphSelectors
by ENUMSET1:def 2;
assume _GraphSelectors c= dom GS;
hence VertexSelector in dom GS & EdgeSelector in dom GS &
SourceSelector in dom GS & TargetSelector in dom GS by A1,A2;
end;
hence thesis;
end;
registration
let G be _Graph;
cluster G|(_GraphSelectors) -> [Graph-like];
coherence
proof
now
let x be object;
assume x in _GraphSelectors;
then
x = VertexSelector or x = EdgeSelector or x = SourceSelector or x =
TargetSelector by ENUMSET1:def 2;
hence x in dom G by Def10;
end;
then
A1: _GraphSelectors c= dom G;
set G2 = G|(_GraphSelectors);
VertexSelector in _GraphSelectors by ENUMSET1:def 2;
then
A2: the_Vertices_of G2 = the_Vertices_of G by FUNCT_1:49;
EdgeSelector in _GraphSelectors by ENUMSET1:def 2;
then
A3: the_Edges_of G2 = the_Edges_of G by FUNCT_1:49;
TargetSelector in _GraphSelectors by ENUMSET1:def 2;
then
A4: the_Target_of G2 = the_Target_of G by FUNCT_1:49;
SourceSelector in _GraphSelectors by ENUMSET1:def 2;
then
A5: the_Source_of G2 = the_Source_of G by FUNCT_1:49;
dom G2 = dom G /\ _GraphSelectors by RELAT_1:61
.= _GraphSelectors by A1,XBOOLE_1:28;
hence thesis by A2,A3,A5,A4,Lm1;
end;
end;
definition
let G be _Graph, x,y,e be object;
pred e Joins x,y,G means
e in the_Edges_of G & ( (the_Source_of G).e
= x & (the_Target_of G).e = y or (the_Source_of G).e = y & (the_Target_of G).e
= x );
end;
definition
let G be _Graph, x, y, e be object;
pred e DJoins x,y,G means
:Def14:
e in the_Edges_of G & (the_Source_of G).e = x & (the_Target_of G).e = y;
end;
definition
let G be _Graph, X,Y be set,e be object;
pred e SJoins X,Y,G means
e in the_Edges_of G & ( (the_Source_of G).e in X & (the_Target_of G).e in Y
or (the_Source_of G).e in Y & (the_Target_of G).e in X);
pred e DSJoins X,Y,G means
e in the_Edges_of G & (the_Source_of G).e in X & (the_Target_of G).e in Y;
end;
definition
let G be _Graph;
attr G is _finite means
:Def17:
the_Vertices_of G is finite & the_Edges_of G is finite;
attr G is loopless means
:Def18:
not ex e being object st e in the_Edges_of G &
(the_Source_of G).e = (the_Target_of G).e;
attr G is _trivial means
:Def19:
card the_Vertices_of G = 1;
attr G is non-multi means
:Def20:
for e1,e2,v1,v2 being object holds e1 Joins
v1,v2,G & e2 Joins v1,v2,G implies e1 = e2;
attr G is non-Dmulti means
:Def21:
for e1,e2,v1,v2 being object holds e1 DJoins
v1,v2,G & e2 DJoins v1,v2,G implies e1 = e2;
end;
definition
let G be _Graph;
attr G is simple means
G is loopless & G is non-multi;
attr G is Dsimple means
G is loopless & G is non-Dmulti;
end;
Lm2: for G being _Graph holds the_Edges_of G = {} implies G is simple
proof
let G be _Graph;
assume
A1: the_Edges_of G = {};
then
A2: G is loopless;
for e1,e2,v1,v2 being object holds e1 Joins v1,v2,G & e2 Joins v1,v2,G
implies e1 = e2 by A1;
then G is non-multi;
hence thesis by A2;
end;
registration
cluster non-multi -> non-Dmulti for _Graph;
coherence
proof
let G be _Graph;
assume
A1: G is non-multi;
now
let e1,e2,v1,v2 be object;
assume e1 DJoins v1,v2,G & e2 DJoins v1,v2,G;
then e1 Joins v1,v2,G & e2 Joins v1,v2,G;
hence e1 = e2 by A1;
end;
hence thesis;
end;
cluster simple -> loopless non-multi for _Graph;
coherence;
cluster loopless non-multi -> simple for _Graph;
coherence;
cluster loopless non-Dmulti -> Dsimple for _Graph;
coherence;
cluster Dsimple -> loopless non-Dmulti for _Graph;
coherence;
cluster _trivial loopless -> _finite for _Graph;
coherence
proof
let G be _Graph;
assume that
A2: G is _trivial and
A3: G is loopless;
card the_Vertices_of G = 1 by A2;
then consider v being object such that
A4: the_Vertices_of G = {v} by CARD_2:42;
now
per cases;
suppose
the_Edges_of G is empty;
hence the_Edges_of G is finite;
end;
suppose
the_Edges_of G is non empty;
then consider e being object such that
A5: e in the_Edges_of G by XBOOLE_0:def 1;
(the_Target_of G).e in the_Vertices_of G by A5,FUNCT_2:5;
then
A6: (the_Target_of G).e = v by A4,TARSKI:def 1;
(the_Source_of G).e in the_Vertices_of G by A5,FUNCT_2:5;
then (the_Source_of G).e = v by A4,TARSKI:def 1;
hence the_Edges_of G is finite by A3,A5,A6;
end;
end;
hence thesis by A4;
end;
cluster _trivial non-Dmulti -> _finite for _Graph;
coherence
proof
let G be _Graph;
assume that
A7: G is _trivial and
A8: G is non-Dmulti;
card the_Vertices_of G = 1 by A7;
then consider v being object such that
A9: the_Vertices_of G = {v} by CARD_2:42;
now
set e1 = the Element of the_Edges_of G;
set v1 = (the_Source_of G).e1, v2 = (the_Target_of G).e1;
assume
A10: not the_Edges_of G is finite;
then
A11: the_Edges_of G <> {};
v2 in the_Vertices_of G by A10,FUNCT_2:5;
then
A12: v2 = v by A9,TARSKI:def 1;
v1 in the_Vertices_of G by A10,FUNCT_2:5;
then v1 = v by A9,TARSKI:def 1;
then
A13: e1 DJoins v,v,G by A11,A12;
now
let x be object;
set v1 = (the_Source_of G).x, v2 = (the_Target_of G).x;
hereby
assume x in {e1};
then x = e1 by TARSKI:def 1;
hence x in the_Edges_of G by A11;
end;
assume
A14: x in the_Edges_of G;
then v2 in the_Vertices_of G by FUNCT_2:5;
then
A15: v2 = v by A9,TARSKI:def 1;
v1 in the_Vertices_of G by A14,FUNCT_2:5;
then v1 = v by A9,TARSKI:def 1;
then x DJoins v,v,G by A14,A15;
then x = e1 by A8,A13;
hence x in {e1} by TARSKI:def 1;
end;
hence contradiction by A10,TARSKI:2;
end;
hence thesis by A9;
end;
end;
registration
cluster _trivial simple for _Graph;
existence
proof
set V = {1}, E = {};
reconsider S = {} as Function of E,V by RELSET_1:12;
set G = createGraph(V,E,S,S);
take G;
card the_Vertices_of G = 1 by CARD_1:30;
hence G is _trivial;
for e1,e2,v1,v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G holds
e1 = e2;
then
A1: G is non-multi;
G is loopless;
hence thesis by A1;
end;
cluster _finite non _trivial simple for _Graph;
existence
proof
set V = {1,2}, E = {};
reconsider S = {} as Function of E,V by RELSET_1:12;
set G = createGraph(V,E,S,S);
take G;
thus G is _finite;
card the_Vertices_of G <> 1 by CARD_2:57;
hence G is non _trivial;
A4: G is loopless;
for e1,e2,v1,v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G
holds e1 = e2;
then G is non-multi;
hence thesis by A4;
end;
end;
registration
let G be _finite _Graph;
cluster the_Vertices_of G -> finite;
coherence by Def17;
cluster the_Edges_of G -> finite;
coherence by Def17;
end;
registration
let G be _trivial _Graph;
cluster the_Vertices_of G -> finite;
coherence
proof
card the_Vertices_of G = 1 by Def19;
hence thesis;
end;
end;
registration
let V be non empty finite set, E be finite set, S,T be Function of E,V;
cluster createGraph(V,E,S,T) -> _finite;
coherence;
end;
registration
let V be non empty set, E be empty set,S,T be Function of E,V;
cluster createGraph(V,E,S,T) -> simple;
coherence
proof
set G = createGraph(V,E,S,T);
for e1,e2,v1,v2 be object st e1 Joins v1,v2,G & e2 Joins v1,v2,G
holds e1 = e2;
then
A1: G is non-multi;
G is loopless;
hence thesis by A1;
end;
end;
registration
let v be set, E be set, S,T be Function of E,{v};
cluster createGraph({v},E,S,T) -> _trivial;
coherence
proof
set G = createGraph({v},E,S,T);
card the_Vertices_of G = 1 by CARD_1:30;
hence thesis;
end;
end;
definition
let G be _Graph;
func G.order() -> Cardinal equals
card the_Vertices_of G;
coherence;
end;
definition
let G be _finite _Graph;
redefine func G.order() -> non zero Element of NAT; :: redefines .order() (GLIB_000, definition)
coherence
proof
G.order() = card the_Vertices_of G;
hence thesis;
end;
end;
definition
let G be _Graph;
func G.size() -> Cardinal equals
card the_Edges_of G;
coherence;
end;
definition
let G be _finite _Graph;
redefine func G.size() -> Element of NAT; :: redefines .size() (GLIB_000, definition)
coherence
proof
G.size() = card the_Edges_of G;
hence thesis;
end;
end;
definition
let G be _Graph, X be set;
func G.edgesInto(X) -> Subset of the_Edges_of G means
:Def26:
for e being
set holds e in it iff e in the_Edges_of G & (the_Target_of G).e in X;
existence
proof
defpred P[set] means (the_Target_of G).$1 in X;
consider IT being Subset of the_Edges_of G such that
A1: for e being set holds e in IT iff e in the_Edges_of G & P[e] from
SUBSET_1:sch 1;
take IT;
thus thesis by A1;
end;
uniqueness
proof
let IT1, IT2 be Subset of the_Edges_of G such that
A2: for e being set holds e in IT1 iff e in the_Edges_of G & (
the_Target_of G).e in X and
A3: for e being set holds e in IT2 iff e in the_Edges_of G & (
the_Target_of G).e in X;
now
let e be object;
hereby
assume
A4: e in IT1;
then (the_Target_of G).e in X by A2;
hence e in IT2 by A3,A4;
end;
assume
A5: e in IT2;
then (the_Target_of G).e in X by A3;
hence e in IT1 by A2,A5;
end;
hence thesis by TARSKI:2;
end;
func G.edgesOutOf(X) -> Subset of the_Edges_of G means
:Def27:
for e being
set holds e in it iff e in the_Edges_of G & (the_Source_of G).e in X;
existence
proof
defpred P[set] means (the_Source_of G).$1 in X;
consider IT being Subset of the_Edges_of G such that
A6: for e being set holds e in IT iff e in the_Edges_of G & P[e] from
SUBSET_1:sch 1;
take IT;
thus thesis by A6;
end;
uniqueness
proof
let IT1, IT2 be Subset of the_Edges_of G such that
A7: for e being set holds e in IT1 iff e in the_Edges_of G & (
the_Source_of G).e in X and
A8: for e being set holds e in IT2 iff e in the_Edges_of G & (
the_Source_of G).e in X;
now
let e be object;
hereby
assume
A9: e in IT1;
then (the_Source_of G).e in X by A7;
hence e in IT2 by A8,A9;
end;
assume
A10: e in IT2;
then (the_Source_of G).e in X by A8;
hence e in IT1 by A7,A10;
end;
hence thesis by TARSKI:2;
end;
end;
definition
let G be _Graph, X be set;
func G.edgesInOut(X) -> Subset of the_Edges_of G equals
G.edgesInto(X) \/ G.edgesOutOf(X);
coherence;
func G.edgesBetween(X) -> Subset of the_Edges_of G equals
G.edgesInto(X) /\ G.edgesOutOf(X);
coherence;
end;
definition
let G be _Graph, X,Y be set;
func G.edgesBetween(X,Y) -> Subset of the_Edges_of G means
:Def30:
for e being object holds e in it iff e SJoins X,Y,G;
existence
proof
defpred P[object] means $1 SJoins X,Y,G;
consider IT being Subset of the_Edges_of G such that
A1: for e being set holds e in IT iff e in the_Edges_of G & P[e] from
SUBSET_1:sch 1;
take IT;
let e be object;
thus e in IT implies P[e] by A1;
assume
A2: e SJoins X,Y,G;
thus thesis by A1,A2;
end;
uniqueness
proof
let IT1,IT2 being Subset of the_Edges_of G such that
A3: for e being object holds e in IT1 iff e SJoins X,Y,G and
A4: for e being object holds e in IT2 iff e SJoins X,Y,G;
for e being object holds e in IT2 iff e in IT1 by A3,A4;
hence thesis by TARSKI:2;
end;
func G.edgesDBetween(X,Y) -> Subset of the_Edges_of G means
:Def31:
for e being object holds e in it iff e DSJoins X,Y,G;
existence
proof
defpred P[object] means $1 DSJoins X,Y,G;
consider IT being Subset of the_Edges_of G such that
A5: for e being set holds e in IT iff e in the_Edges_of G & P[e] from
SUBSET_1:sch 1;
take IT;
let e be object;
thus e in IT implies P[e] by A5;
assume
A6: e DSJoins X,Y,G;
thus thesis by A5,A6;
end;
uniqueness
proof
let IT1,IT2 being Subset of the_Edges_of G such that
A7: for e being object holds e in IT1 iff e DSJoins X,Y,G and
A8: for e being object holds e in IT2 iff e DSJoins X,Y,G;
for e being object holds e in IT2 iff e in IT1 by A7,A8;
hence thesis by TARSKI:2;
end;
end;
scheme
FinGraphOrderInd{P[_Graph]}: for G being _finite _Graph holds P[G]
provided
A1: for G being _finite _Graph st G.order() = 1 holds P[G] and
A2: for k being non zero Nat st (for Gk being _finite _Graph st Gk
.order() = k holds P[Gk]) holds
for Gk1 being _finite _Graph st Gk1.order() = k+1 holds P[Gk1]
proof
defpred P2[Nat] means for G being _finite _Graph st G.order()=$1 holds P[G];
A3: for k being non zero Nat st P2[k] holds P2[k+1] by A2;
let G be _finite _Graph;
A4: G.order() = G.order();
A5: P2[1] by A1;
for k being non zero Nat holds P2[k] from NAT_1:sch 10(A5,A3);
hence thesis by A4;
end;
scheme
FinGraphSizeInd{P[_Graph]}: for G being _finite _Graph holds P[G]
provided
A1: for G being _finite _Graph st G.size() = 0 holds P[G] and
A2: for k being Nat st
(for Gk being _finite _Graph st Gk.size() = k holds P[Gk]) holds
for Gk1 being _finite _Graph st Gk1.size() = k+1
holds P[Gk1]
proof
defpred P2[Nat] means for G being _finite _Graph st G.size()=$1
holds P[G];
A3: for k being Nat st P2[k] holds P2[k+1] by A2;
let G be _finite _Graph;
A4: G.size() = G.size();
A5: P2[ 0 ] by A1;
for k being Nat holds P2[k] from NAT_1:sch 2(A5,A3);
hence thesis by A4;
end;
definition
let G be _Graph;
mode Subgraph of G -> _Graph means
:Def32:
the_Vertices_of it c= the_Vertices_of G &
the_Edges_of it c= the_Edges_of G & for e being set st e in
the_Edges_of it holds (the_Source_of it).e = (the_Source_of G).e & (
the_Target_of it).e = (the_Target_of G).e;
existence
proof
take G;
thus thesis;
end;
end;
definition
let G1 be _Graph, G2 be Subgraph of G1;
redefine func the_Vertices_of G2 -> non empty Subset of the_Vertices_of G1; :: redefines the_Vertices_of (GLIB_000, definition)
coherence by Def32;
redefine func the_Edges_of G2 -> Subset of the_Edges_of G1; :: redefines the_Edges_of (GLIB_000, definition)
coherence by Def32;
end;
registration
let G be _Graph;
cluster _trivial simple for Subgraph of G;
existence
proof
set v = the Element of the_Vertices_of G;
set V = {v}, E = {};
reconsider S = {} as Function of E,V by RELSET_1:12;
set IT = createGraph(V,E,S,S);
A1: the_Vertices_of IT = {v} & for e being set st e in the_Edges_of IT
holds ( the_Source_of IT).e = (the_Source_of G).e & (the_Target_of IT).e = (
the_Target_of G).e;
the_Edges_of IT c= the_Edges_of G;
then reconsider IT as Subgraph of G by A1,Def32;
take IT;
thus thesis;
end;
end;
Lm3: for G being _Graph holds G is Subgraph of G
proof
let G be _Graph;
for e being set st e in the_Edges_of G holds (the_Source_of G).e = (
the_Source_of G).e & (the_Target_of G).e = (the_Target_of G).e;
hence thesis by Def32;
end;
Lm4: for G1 being _Graph, G2 being Subgraph of G1,
x,y,e being object holds e
Joins x,y,G2 implies e Joins x,y,G1
proof
let G1 be _Graph, G2 be Subgraph of G1, x,y,e be object;
assume
A1: e Joins x,y,G2;
then
A2: e in the_Edges_of G2;
(the_Source_of G2).e = x & (the_Target_of G2).e = y or ( the_Source_of
G2).e = y & (the_Target_of G2).e = x by A1;
then (the_Source_of G1).e = x & (the_Target_of G1).e = y or ( the_Source_of
G1).e = y & (the_Target_of G1).e = x by A2,Def32;
hence thesis by A2;
end;
registration
let G be _finite _Graph;
cluster -> _finite for Subgraph of G;
coherence
proof
let G2 be Subgraph of G;
the_Vertices_of G2 is finite & the_Edges_of G2 is finite;
hence thesis;
end;
end;
registration
let G be loopless _Graph;
cluster -> loopless for Subgraph of G;
coherence
proof
let G2 be Subgraph of G;
now
given e being object such that
A1: e in the_Edges_of G2 and
A2: (the_Source_of G2).e = (the_Target_of G2).e;
(the_Source_of G2).e = (the_Source_of G).e & (the_Target_of G2).e =
( the_Target_of G).e by A1,Def32;
hence contradiction by A1,A2,Def18;
end;
hence thesis;
end;
end;
registration
let G be _trivial _Graph;
cluster -> _trivial for Subgraph of G;
coherence
proof
let G2 be Subgraph of G;
card the_Vertices_of G = 1 by Def19;
then consider v being object such that
A1: the_Vertices_of G = {v} by CARD_2:42;
the_Vertices_of G2 = {v} by A1,ZFMISC_1:33;
then card the_Vertices_of G2 = 1 by CARD_1:30;
hence thesis;
end;
end;
registration
let G be non-multi _Graph;
cluster -> non-multi for Subgraph of G;
coherence
proof
let G2 be Subgraph of G;
now
let e1,e2,v1,v2 be object;
assume e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2;
then e1 Joins v1,v2,G & e2 Joins v1,v2,G by Lm4;
hence e1 = e2 by Def20;
end;
hence thesis;
end;
end;
definition
let G1 be _Graph, G2 be Subgraph of G1;
attr G2 is spanning means
:Def33:
the_Vertices_of G2 = the_Vertices_of G1;
end;
registration
let G be _Graph;
cluster spanning for Subgraph of G;
existence
proof
reconsider G9=G as Subgraph of G by Lm3;
take G9;
thus thesis;
end;
end;
definition
let G1, G2 be _Graph;
pred G1 == G2 means
the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1 = the_Source_of G2 &
the_Target_of G1 = the_Target_of G2;
reflexivity;
symmetry;
end;
notation
let G1,G2 be _Graph;
antonym G1 != G2 for G1 == G2;
end;
definition
let G1,G2 be _Graph;
pred G1 c= G2 means
G1 is Subgraph of G2;
reflexivity by Lm3;
end;
definition
let G1,G2 be _Graph;
pred G1 c< G2 means
G1 c= G2 & G1 != G2;
irreflexivity;
end;
definition
let G be _Graph, V, E be set;
mode inducedSubgraph of G,V,E -> Subgraph of G means
:Def37:
the_Vertices_of
it = V & the_Edges_of it = E if V is non empty Subset of the_Vertices_of G & E
c= G.edgesBetween(V) otherwise it == G;
existence
proof
hereby
assume that
A1: V is non empty Subset of the_Vertices_of G and
A2: E c= G.edgesBetween(V);
reconsider E9 = E as Subset of the_Edges_of G by A2,XBOOLE_1:1;
set S = (the_Source_of G) | E9, T = (the_Target_of G) | E9;
reconsider V9 = V as non empty Subset of the_Vertices_of G by A1;
dom the_Target_of G = the_Edges_of G by FUNCT_2:def 1;
then
A3: dom T = E9 by RELAT_1:62;
now
let e be object;
assume
A4: e in E9;
then e in G.edgesInto(V) by A2,XBOOLE_0:def 4;
then (the_Target_of G).e in V by Def26;
hence T.e in V by A4,FUNCT_1:49;
end;
then reconsider T as Function of E9,V9 by A3,FUNCT_2:3;
dom the_Source_of G = the_Edges_of G by FUNCT_2:def 1;
then
A5: dom S = E9 by RELAT_1:62;
now
let e be object;
assume
A6: e in E9;
then e in G.edgesOutOf(V) by A2,XBOOLE_0:def 4;
then (the_Source_of G).e in V by Def27;
hence S.e in V by A6,FUNCT_1:49;
end;
then reconsider S as Function of E9,V9 by A5,FUNCT_2:3;
set IT = createGraph(V9,E9,S,T);
the_Vertices_of IT = V & for e being set st e in the_Edges_of IT
holds ( the_Source_of IT).e = (the_Source_of G).e & (the_Target_of IT).e = (
the_Target_of G).e by FUNCT_1:49;
then reconsider IT as Subgraph of G by Def32;
take IT;
thus the_Vertices_of IT = V & the_Edges_of IT = E;
end;
G is Subgraph of G by Lm3;
hence thesis;
end;
consistency;
end;
definition
let G be _Graph, V be set;
mode inducedSubgraph of G,V is inducedSubgraph of G,V,G.edgesBetween(V);
end;
registration
let G be _Graph, V be finite non empty Subset of the_Vertices_of G, E be
finite Subset of G.edgesBetween(V);
cluster -> _finite for inducedSubgraph of G,V,E;
coherence by Def37;
end;
registration
let G be _Graph, v be Element of the_Vertices_of G, E be Subset of G
.edgesBetween({v});
cluster -> _trivial for inducedSubgraph of G,{v},E;
coherence
proof
let IT be inducedSubgraph of G,{v},E;
the_Vertices_of IT = {v} by Def37;
then card the_Vertices_of IT = 1 by CARD_1:30;
hence thesis;
end;
end;
registration
let G be _Graph, v be Element of the_Vertices_of G;
cluster -> _finite _trivial for inducedSubgraph of G,{v},{};
coherence
proof
reconsider E = {} as finite Subset of G.edgesBetween({v}) by XBOOLE_1:2;
let IT be inducedSubgraph of G,{v},{};
IT is inducedSubgraph of G,{v},E;
hence thesis;
end;
end;
registration
let G be _Graph, V be non empty Subset of the_Vertices_of G;
cluster -> simple for inducedSubgraph of G,V,{};
coherence
proof
let IT be inducedSubgraph of G,V,{};
reconsider E = {} as Subset of G.edgesBetween(V) by XBOOLE_1:2;
IT is inducedSubgraph of G,V,E;
then the_Edges_of IT = {} by Def37;
hence thesis by Lm2;
end;
end;
Lm5: for G being _Graph, e,X being set holds e in the_Edges_of G & (
the_Source_of G).e in X & (the_Target_of G).e in X iff e in G.edgesBetween(X)
proof
let G be _Graph, e,X be set;
hereby
assume
e in the_Edges_of G & (the_Source_of G).e in X & (the_Target_of G) .e in X;
then e in G.edgesInto(X) & e in G.edgesOutOf(X) by Def26,Def27;
hence e in G.edgesBetween(X) by XBOOLE_0:def 4;
end;
assume e in G.edgesBetween(X);
then e in G.edgesInto(X) & e in G.edgesOutOf(X) by XBOOLE_0:def 4;
hence thesis by Def26,Def27;
end;
Lm6: for G being _Graph holds the_Edges_of G = G.edgesBetween(the_Vertices_of
G)
proof
let G be _Graph;
set EG = the_Edges_of G, SG = the_Source_of G, TG = the_Target_of G;
now
let x be object;
hereby
assume
A1: x in EG;
then SG.x in the_Vertices_of G & TG.x in the_Vertices_of G by FUNCT_2:5;
hence x in G.edgesBetween(the_Vertices_of G) by A1,Lm5;
end;
assume x in G.edgesBetween(the_Vertices_of G);
hence x in EG;
end;
hence thesis by TARSKI:2;
end;
registration
let G be _Graph, E be Subset of the_Edges_of G;
cluster -> spanning for inducedSubgraph of G,the_Vertices_of G, E;
coherence
proof
let G1 be inducedSubgraph of G,the_Vertices_of G, E;
G.edgesBetween(the_Vertices_of G) = the_Edges_of G & the_Vertices_of G
c= the_Vertices_of G by Lm6;
then the_Vertices_of G1 = the_Vertices_of G by Def37;
hence thesis;
end;
end;
registration
let G be _Graph;
cluster -> spanning for inducedSubgraph of G,the_Vertices_of G,{};
coherence
proof
let G1 be inducedSubgraph of G,the_Vertices_of G,{};
the_Vertices_of G c= the_Vertices_of G & {} c= G.edgesBetween(
the_Vertices_of G);
then the_Vertices_of G1 = the_Vertices_of G by Def37;
hence thesis;
end;
end;
definition
let G be _Graph, v be set;
mode removeVertex of G,v is inducedSubgraph of G, the_Vertices_of G \ {v};
end;
definition
let G be _Graph, V be set;
mode removeVertices of G,V is inducedSubgraph of G, the_Vertices_of G \ V;
end;
definition
let G be _Graph, e be set;
mode removeEdge of G,e is inducedSubgraph of G, the_Vertices_of G,
the_Edges_of G \ {e};
end;
definition
let G be _Graph, E be set;
mode removeEdges of G,E is inducedSubgraph of G, the_Vertices_of G,
the_Edges_of G \ E;
end;
registration
let G be _Graph, e be set;
cluster -> spanning for removeEdge of G,e;
coherence;
end;
registration
let G be _Graph, E be set;
cluster -> spanning for removeEdges of G,E;
coherence;
end;
definition
let G be _Graph;
mode Vertex of G is Element of the_Vertices_of G;
end;
definition
let G be _Graph, v be Vertex of G;
func v.edgesIn() -> Subset of the_Edges_of G equals
G.edgesInto( {v} );
coherence;
func v.edgesOut() -> Subset of the_Edges_of G equals
G.edgesOutOf( {v} );
coherence;
func v.edgesInOut() -> Subset of the_Edges_of G equals
G.edgesInOut( {v} );
coherence;
end;
Lm7: for G being _Graph, v being Vertex of G, e being set holds e in v
.edgesIn() iff e in the_Edges_of G & (the_Target_of G).e = v
proof
let G be _Graph, v be Vertex of G, e be set;
hereby
assume
A1: e in v.edgesIn();
then (the_Target_of G).e in {v} by Def26;
hence e in the_Edges_of G & (the_Target_of G).e = v by A1,TARSKI:def 1;
end;
assume that
A2: e in the_Edges_of G and
A3: (the_Target_of G).e = v;
(the_Target_of G).e in {v} by A3,TARSKI:def 1;
hence thesis by A2,Def26;
end;
Lm8: for G being _Graph, v being Vertex of G, e being set holds e in v
.edgesOut() iff e in the_Edges_of G & (the_Source_of G).e = v
proof
let G be _Graph, v be Vertex of G, e be set;
hereby
assume
A1: e in v.edgesOut();
then (the_Source_of G).e in {v} by Def27;
hence e in the_Edges_of G & (the_Source_of G).e = v by A1,TARSKI:def 1;
end;
assume that
A2: e in the_Edges_of G and
A3: (the_Source_of G).e = v;
(the_Source_of G).e in {v} by A3,TARSKI:def 1;
hence thesis by A2,Def27;
end;
definition
let G be _Graph, v be Vertex of G, e be object;
func v.adj(e) -> Vertex of G equals
:Def41:
(the_Source_of G).e if e in
the_Edges_of G & (the_Target_of G).e = v, (the_Target_of G).e if e in
the_Edges_of G & (the_Source_of G).e = v & not (the_Target_of G).e = v
otherwise v;
coherence by FUNCT_2:5;
consistency;
end;
definition
let G be _Graph, v be Vertex of G;
func v.inDegree() -> Cardinal equals
card v.edgesIn();
coherence;
func v.outDegree() -> Cardinal equals
card v.edgesOut();
coherence;
end;
definition
let G be _finite _Graph, v be Vertex of G;
redefine func v.inDegree() -> Element of NAT; :: redefines .inDegree() (GLIB_000, definition)
coherence
proof
v.inDegree() = card v.edgesIn();
hence thesis;
end;
redefine func v.outDegree() -> Element of NAT; :: redefines .outDegree() (GLIB_000, definition)
coherence
proof
v.outDegree() = card v.edgesOut();
hence thesis;
end;
end;
definition
let G be _Graph, v be Vertex of G;
func v.degree() -> Cardinal equals
v.inDegree() +` v.outDegree();
coherence;
end;
definition
let G be _finite _Graph, v be Vertex of G;
redefine func v.degree() -> Element of NAT equals :: redefines .degree() (GLIB_000, definition)
v.inDegree() + v
.outDegree();
correctness
proof
v.degree() = card (v.inDegree() +^ v.outDegree()) by CARD_2:def 1
.= card (v.inDegree() + v.outDegree()) by CARD_2:36
.= v.inDegree() + v.outDegree();
hence thesis;
end;
end;
definition
let G be _Graph, v be Vertex of G;
func v.inNeighbors() -> Subset of the_Vertices_of G equals
(the_Source_of G)
.:v.edgesIn();
coherence;
func v.outNeighbors() -> Subset of the_Vertices_of G equals
(the_Target_of G
).:v.edgesOut();
coherence;
end;
definition
let G be _Graph, v be Vertex of G;
func v.allNeighbors() -> Subset of the_Vertices_of G equals
v.inNeighbors()
\/ v.outNeighbors();
coherence;
end;
definition
let G be _Graph, v being Vertex of G;
attr v is isolated means
v.edgesInOut() = {};
end;
definition
let G be _finite _Graph, v be Vertex of G;
redefine attr v is isolated means :: redefines isolated (GLIB_000, definition)
v.degree() = 0;
compatibility
proof
hereby
assume v is isolated;
then
A1: v.edgesInOut() = {};
then v.inDegree() = 0 by CARD_1:27,XBOOLE_1:15;
hence v.degree() = 0 by A1,CARD_1:27,XBOOLE_1:15;
end;
assume
A2: v.degree() = 0;
then v.edgesIn() = {};
hence thesis by A2;
end;
end;
definition
let G be _Graph, v be Vertex of G;
attr v is endvertex means
ex e being object st v.edgesInOut() = {e} & not e Joins v,v,G;
end;
definition
let G be _finite _Graph, v be Vertex of G;
redefine attr v is endvertex means :: redefines endvertex (GLIB_000, definition)
v.degree() = 1;
compatibility
proof
hereby
assume v is endvertex;
then consider e being object such that
A1: v.edgesInOut() = {e} and
A2: not e Joins v,v,G;
now
per cases by A1,ZFMISC_1:37;
suppose
A3: v.edgesIn() = {e} & v.edgesOut() = {e};
then e in v.edgesOut() by TARSKI:def 1;
then
A4: (the_Source_of G).e = v by Lm8;
A5: e in v.edgesIn() by A3,TARSKI:def 1;
then (the_Target_of G).e = v by Lm7;
hence v.degree() = 1 by A2,A5,A4;
end;
suppose
v.edgesIn() = {} & v.edgesOut() = {e};
hence v.degree() = 1 by CARD_1:30;
end;
suppose
v.edgesIn() = {e} & v.edgesOut() = {};
hence v.degree() = 1 by CARD_1:30;
end;
end;
hence v.degree() = 1;
end;
assume
A6: v.degree() = 1;
now
per cases;
suppose
A7: card v.edgesIn() = 0;
then consider e being object such that
A8: v.edgesOut() = {e} by A6,CARD_2:42;
A9: v.edgesIn() = {} by A7;
then
A10: not e Joins v,v,G by Lm7;
v.edgesInOut() = {e} by A9,A8;
hence thesis by A10;
end;
suppose
card v.edgesIn() <> 0;
then 0 < card v.edgesIn();
then
A11: 0+1 <= card v.edgesIn() by NAT_1:13;
card v.edgesIn() <= 1 by A6,NAT_1:11;
then
A12: card v.edgesIn() = 1 by A11,XXREAL_0:1;
then consider e being object such that
A13: v.edgesIn() = {e} by CARD_2:42;
A14: v.edgesOut() = {} by A6,A12;
then
A15: not e Joins v,v,G by Lm8;
v.edgesInOut() = {e} by A13,A14;
hence thesis by A15;
end;
end;
hence thesis;
end;
end;
LmNat:
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 F be Function;
attr F is Graph-yielding means
:Def53a:
for x being object st x in dom F holds F.x is _Graph;
end;
definition
let F be ManySortedSet of NAT;
redefine attr F is Graph-yielding means :Def53: :: redefines Graph-yielding (GLIB_000, definition)
for n being Nat holds F.n is _Graph;
compatibility
proof
thus F is Graph-yielding implies for n be Nat holds F.n is _Graph by LmNat;
assume A2: for n being Nat holds F.n is _Graph;
let x be object;
assume x in dom F;
hence thesis by A2;
end;
attr F is halting means
ex n being Nat st F.n = F.(n+1);
end;
definition
let F be ManySortedSet of NAT;
func F.Lifespan() -> Element of NAT means
F.it = F.(it+1) & for n being Nat
st F.n = F.(n+1) holds it <= n if F is halting otherwise it = 0;
existence
proof
defpred P[Nat] means F.$1 = F.($1+1);
hereby
assume F is halting;
then
A1: ex n being Nat st P[n];
ex IT being Nat st P[IT] & for n being Nat st P[n] holds IT <= n
from NAT_1:sch 5(A1);
then consider IT being Nat such that
A2: ( P[IT])& for n being Nat st P[n] holds IT <= n;
IT in NAT by ORDINAL1:def 12;
hence
ex IT being Element of NAT st P[IT] & for n being Nat st P[n] holds
IT <= n by A2;
end;
thus thesis;
end;
uniqueness
proof
let IT1, IT2 be Element of NAT;
hereby
assume F is halting;
assume
A3: F.IT1 = F.(IT1+1) & for n being Nat st F.n = F.(n+1) holds IT1 <= n;
assume
F.IT2 = F.(IT2+1) & for n being Nat st F.n = F.(n+1) holds IT2 <= n;
then IT1 <= IT2 & IT2 <= IT1 by A3;
hence IT1 = IT2 by XXREAL_0:1;
end;
thus thesis;
end;
consistency;
end;
definition
let F be ManySortedSet of NAT;
func F.Result() -> set equals
F.(F.Lifespan());
coherence;
end;
registration
cluster empty -> Graph-yielding for Function;
coherence;
end;
registration
let G be _Graph;
cluster NAT --> G -> Graph-yielding;
coherence
proof
set F = NAT --> G;
A1: dom F = NAT;
reconsider F as ManySortedSet of NAT;
let x be Nat;
x in NAT by ORDINAL1:def 12;
then F.x in rng F by A1,FUNCT_1:3;
then F.x in {G} by FUNCOP_1:8;
hence thesis by TARSKI:def 1;
end;
end;
registration
cluster Graph-yielding for ManySortedSet of NAT;
existence
proof
set G = the _Graph;
set F = NAT --> G;
reconsider F as ManySortedSet of NAT;
take F;
thus thesis;
end;
end;
definition
mode GraphSeq is Graph-yielding ManySortedSet of NAT;
end;
registration
cluster -> non empty for GraphSeq;
coherence
proof
let GSeq be GraphSeq;
dom GSeq = NAT by PARTFUN1:def 2;
hence thesis;
end;
end;
registration
cluster non empty Graph-yielding for Function;
existence
proof
take the GraphSeq;
thus thesis;
end;
end;
registration
let GF be non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> Function-like Relation-like;
coherence by Def53a;
end;
registration
let GSq be GraphSeq, x be Nat;
cluster GSq.x -> Function-like Relation-like;
coherence by Def53;
end;
registration
let GF be non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> NAT -defined finite;
coherence by Def53a;
end;
registration
let GSq be GraphSeq, x be Nat;
cluster GSq.x -> NAT -defined finite;
coherence by Def53;
end;
registration
let GF be non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> [Graph-like];
coherence by Def53a;
end;
registration
let GSq be GraphSeq, x be Nat;
cluster GSq.x -> [Graph-like];
coherence by Def53;
end;
definition
let GF be Graph-yielding Function;
attr GF is _finite means
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is _finite;
attr GF is loopless means
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is loopless;
attr GF is _trivial means
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is _trivial;
attr GF is non-trivial means
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is non _trivial;
attr GF is non-multi means
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is non-multi;
attr GF is non-Dmulti means
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is non-Dmulti;
attr GF is simple means
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is simple;
attr GF is Dsimple means
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is Dsimple;
end;
registration
cluster empty -> _finite loopless _trivial non-trivial non-multi
non-Dmulti simple Dsimple for Graph-yielding Function;
coherence;
end;
definition
let GF be non empty Graph-yielding Function;
redefine attr GF is _finite means :: redefines _finite (GLIB_000, definition)
:Def57b:
for x being Element of dom GF holds GF.x is _finite;
compatibility
proof
hereby
assume A1: GF is _finite;
let x be Element of dom GF;
consider G being _Graph such that
A2: GF.x = G & G is _finite by A1;
thus GF.x is _finite by A2;
end;
assume A3: for x being Element of dom GF holds GF.x is _finite;
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;
redefine attr GF is loopless means :: redefines loopless (GLIB_000, definition)
:Def58b:
for x being Element of dom GF holds GF.x is loopless;
compatibility
proof
hereby
assume A1: GF is loopless;
let x be Element of dom GF;
consider G being _Graph such that
A2: GF.x = G & G is loopless by A1;
thus GF.x is loopless by A2;
end;
assume A3: for x being Element of dom GF holds GF.x is loopless;
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;
redefine attr GF is _trivial means :: redefines _trivial (GLIB_000, definition)
:Def59b:
for x being Element of dom GF holds GF.x is _trivial;
compatibility
proof
hereby
assume A1: GF is _trivial;
let x be Element of dom GF;
consider G being _Graph such that
A2: GF.x = G & G is _trivial by A1;
thus GF.x is _trivial by A2;
end;
assume A3: for x being Element of dom GF holds GF.x is _trivial;
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;
redefine attr GF is non-trivial means :: redefines non-trivial (GLIB_000, definition)
:Def60b:
for x being Element of dom GF holds GF.x is non _trivial;
compatibility
proof
hereby
assume A1: GF is non-trivial;
let x be Element of dom GF;
consider G being _Graph such that
A2: GF.x = G & G is non _trivial by A1;
thus GF.x is non _trivial by A2;
end;
assume A3: for x being Element of dom GF holds GF.x is non _trivial;
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;
redefine attr GF is non-multi means :: redefines non-multi (GLIB_000, definition)
:Def61b:
for x being Element of dom GF holds GF.x is non-multi;
compatibility
proof
hereby
assume A1: GF is non-multi;
let x be Element of dom GF;
consider G being _Graph such that
A2: GF.x = G & G is non-multi by A1;
thus GF.x is non-multi by A2;
end;
assume A3: for x being Element of dom GF holds GF.x is non-multi;
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;
redefine attr GF is non-Dmulti means :: redefines non-Dmulti (GLIB_000, definition)
:Def62b:
for x being Element of dom GF holds GF.x is non-Dmulti;
compatibility
proof
hereby
assume A1: GF is non-Dmulti;
let x be Element of dom GF;
consider G being _Graph such that
A2: GF.x = G & G is non-Dmulti by A1;
thus GF.x is non-Dmulti by A2;
end;
assume A3: for x being Element of dom GF holds GF.x is non-Dmulti;
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;
redefine attr GF is simple means :: redefines simple (GLIB_000, definition)
:Def63b:
for x being Element of dom GF holds GF.x is simple;
compatibility
proof
hereby
assume A1: GF is simple;
let x be Element of dom GF;
consider G being _Graph such that
A2: GF.x = G & G is simple by A1;
thus GF.x is simple by A2;
end;
assume A3: for x being Element of dom GF holds GF.x is simple;
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;
redefine attr GF is Dsimple means :: redefines Dsimple (GLIB_000, definition)
:Def64b:
for x being Element of dom GF holds GF.x is Dsimple;
compatibility
proof
hereby
assume A1: GF is Dsimple;
let x be Element of dom GF;
consider G being _Graph such that
A2: GF.x = G & G is Dsimple by A1;
thus GF.x is Dsimple by A2;
end;
assume A3: for x being Element of dom GF holds GF.x is Dsimple;
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 _finite means :: redefines _finite (GLIB_000, redefinition) → _finite (GLIB_000, definition)
:Def57:
for x being Nat holds GSq.x is _finite;
compatibility
proof
hereby
assume A1: GSq is _finite;
let x be Nat;
x in dom GSq by LmNat;
hence GSq.x is _finite by A1;
end;
assume A2: for x being Nat holds GSq.x is _finite;
let x be Element of dom GSq;
thus thesis by A2;
end;
redefine attr GSq is loopless means :: redefines loopless (GLIB_000, redefinition) → loopless (GLIB_000, definition)
:Def58:
for x being Nat holds GSq.x is loopless;
compatibility
proof
hereby
assume A1: GSq is loopless;
let x be Nat;
x in dom GSq by LmNat;
hence GSq.x is loopless by A1;
end;
assume A2: for x being Nat holds GSq.x is loopless;
let x be Element of dom GSq;
thus thesis by A2;
end;
redefine attr GSq is _trivial means :: redefines _trivial (GLIB_000, redefinition) → _trivial (GLIB_000, definition)
:Def59:
for x being Nat holds GSq.x is _trivial;
compatibility
proof
hereby
assume A1: GSq is _trivial;
let x be Nat;
x in dom GSq by LmNat;
hence GSq.x is _trivial by A1;
end;
assume A2: for x being Nat holds GSq.x is _trivial;
let x be Element of dom GSq;
thus thesis by A2;
end;
redefine attr GSq is non-trivial means :: redefines non-trivial (GLIB_000, redefinition) → non-trivial (GLIB_000, definition)
:Def60:
for x being Nat holds GSq.x is non _trivial;
compatibility
proof
hereby
assume A1: GSq is non-trivial;
let x be Nat;
x in dom GSq by LmNat;
hence GSq.x is non _trivial by A1;
end;
assume A2: for x being Nat holds GSq.x is non _trivial;
let x be Element of dom GSq;
thus thesis by A2;
end;
redefine attr GSq is non-multi means :: redefines non-multi (GLIB_000, redefinition) → non-multi (GLIB_000, definition)
:Def61:
for x being Nat holds GSq.x is non-multi;
compatibility
proof
hereby
assume A1: GSq is non-multi;
let x be Nat;
x in dom GSq by LmNat;
hence GSq.x is non-multi by A1;
end;
assume A2: for x being Nat holds GSq.x is non-multi;
let x be Element of dom GSq;
thus thesis by A2;
end;
redefine attr GSq is non-Dmulti means :: redefines non-Dmulti (GLIB_000, redefinition) → non-Dmulti (GLIB_000, definition)
:Def62:
for x being Nat holds GSq.x is non-Dmulti;
compatibility
proof
hereby
assume A1: GSq is non-Dmulti;
let x be Nat;
x in dom GSq by LmNat;
hence GSq.x is non-Dmulti by A1;
end;
assume A2: for x being Nat holds GSq.x is non-Dmulti;
let x be Element of dom GSq;
thus thesis by A2;
end;
redefine attr GSq is simple means :: redefines simple (GLIB_000, redefinition) → simple (GLIB_000, definition)
:Def63:
for x being Nat holds GSq.x is simple;
compatibility
proof
hereby
assume A1: GSq is simple;
let x be Nat;
x in dom GSq by LmNat;
hence GSq.x is simple by A1;
end;
assume A2: for x being Nat holds GSq.x is simple;
let x be Element of dom GSq;
thus thesis by A2;
end;
redefine attr GSq is Dsimple means :: redefines Dsimple (GLIB_000, redefinition) → Dsimple (GLIB_000, definition)
:Def64:
for x being Nat holds GSq.x is Dsimple;
compatibility
proof
hereby
assume A1: GSq is Dsimple;
let x be Nat;
x in dom GSq by LmNat;
hence GSq.x is Dsimple by A1;
end;
assume A2: for x being Nat holds GSq.x is Dsimple;
let x be Element of dom GSq;
thus thesis by A2;
end;
end;
definition
let GSq be GraphSeq;
redefine attr GSq is halting means :: redefines halting (GLIB_000, definition)
ex n being Nat st GSq.n = GSq.(n+1);
compatibility;
end;
registration
cluster halting _finite loopless _trivial non-multi non-Dmulti
simple Dsimple for GraphSeq;
existence
proof
set G = the _finite loopless _trivial non-multi
non-Dmulti simple Dsimple _Graph;
set F = NAT --> G;
reconsider F as ManySortedSet of NAT;
reconsider F as GraphSeq;
A2: F.(1+1) = G;
take F;
F.1 = G;
hence F is halting by A2;
thus thesis;
end;
cluster halting _finite loopless non-trivial non-multi non-Dmulti simple
Dsimple for GraphSeq;
existence
proof
set G = the _finite loopless non _trivial non-multi non-Dmulti
simple Dsimple _Graph;
set F = NAT --> G;
reconsider F as ManySortedSet of NAT;
reconsider F as GraphSeq;
A4: F.(1+1) = G;
take F;
F.1 = G;
hence F is halting by A4;
thus thesis;
end;
end;
registration
let GF be _finite non empty Graph-yielding Function,
x be Element of dom GF;
cluster GF.x -> _finite;
coherence by Def57b;
end;
registration
let GSq be _finite GraphSeq, x be Nat;
cluster GSq.x -> _finite;
coherence by Def57;
end;
registration
let GF be loopless non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> loopless;
coherence by Def58b;
end;
registration
let GSq be loopless GraphSeq, x be Nat;
cluster GSq.x -> loopless for _Graph;
coherence by Def58;
end;
registration
let GF be _trivial non empty Graph-yielding Function,
x be Element of dom GF;
cluster GF.x -> _trivial;
coherence by Def59b;
end;
registration
let GSq be _trivial GraphSeq, x be Nat;
cluster GSq.x -> _trivial for _Graph;
coherence by Def59;
end;
registration
let GF be non-trivial non empty Graph-yielding Function;
let x be Element of dom GF;
cluster GF.x -> non _trivial;
coherence by Def60b;
end;
registration
let GSq be non-trivial GraphSeq, x be Nat;
cluster GSq.x -> non _trivial for _Graph;
coherence by Def60;
end;
registration
let GF be non-multi non empty Graph-yielding Function;
let x be Element of dom GF;
cluster GF.x -> non-multi;
coherence by Def61b;
end;
registration
let GSq be non-multi GraphSeq, x be Nat;
cluster GSq.x -> non-multi for _Graph;
coherence by Def61;
end;
registration
let GF be non-Dmulti non empty Graph-yielding Function;
let x be Element of dom GF;
cluster GF.x -> non-Dmulti;
coherence by Def62b;
end;
registration
let GSq be non-Dmulti GraphSeq, x be Nat;
cluster GSq.x -> non-Dmulti for _Graph;
coherence by Def62;
end;
registration
let GF be simple non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> simple;
coherence by Def63b;
end;
registration
let GSq be simple GraphSeq, x be Nat;
cluster GSq.x -> simple for _Graph;
coherence by Def63;
end;
registration
let GF be Dsimple non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> Dsimple;
coherence by Def64b;
end;
registration
let GSq be Dsimple GraphSeq, x be Nat;
cluster GSq.x -> Dsimple for _Graph;
coherence by Def64;
end;
registration
cluster non-multi -> non-Dmulti for Graph-yielding Function;
coherence
proof
let GF be Graph-yielding Function;
per cases;
suppose GF is empty;
hence thesis;
end;
suppose GF is non empty;
hence thesis;
end;
end;
end;
registration
cluster simple -> loopless non-multi for Graph-yielding Function;
coherence
proof
let GF be Graph-yielding Function;
per cases;
suppose GF is empty;
hence thesis;
end;
suppose GF is non empty;
hence thesis;
end;
end;
end;
registration
cluster loopless non-multi -> simple for Graph-yielding Function;
coherence
proof
let GF be Graph-yielding Function;
per cases;
suppose GF is empty;
hence thesis;
end;
suppose GF is non empty;
hence thesis;
end;
end;
end;
registration
cluster loopless non-Dmulti -> Dsimple for Graph-yielding Function;
coherence
proof
let GF be Graph-yielding Function;
per cases;
suppose GF is empty;
hence thesis;
end;
suppose GF is non empty;
hence thesis;
end;
end;
end;
registration
cluster Dsimple -> loopless non-Dmulti for Graph-yielding Function;
coherence
proof
let GF be Graph-yielding Function;
per cases;
suppose GF is empty;
hence thesis;
end;
suppose GF is non empty;
hence thesis;
end;
end;
end;
registration
cluster _trivial loopless -> _finite for Graph-yielding Function;
coherence
proof
let GF be Graph-yielding Function;
per cases;
suppose GF is empty;
hence thesis;
end;
suppose GF is non empty;
hence thesis;
end;
end;
end;
registration
cluster _trivial non-Dmulti -> _finite for Graph-yielding Function;
coherence
proof
let GF be Graph-yielding Function;
per cases;
suppose GF is empty;
hence thesis;
end;
suppose GF is non empty;
hence thesis;
end;
end;
end;
begin :: Theorems
reserve GS for GraphStruct;
reserve G,G1,G2,G3 for _Graph;
reserve e,x,x1,x2,y,y1,y2,E,V,X,Y for set;
reserve n,n1,n2 for Nat;
reserve v,v1,v2 for Vertex of G;
theorem
VertexSelector = 1 & EdgeSelector = 2 & SourceSelector = 3 &
TargetSelector = 4;
theorem
_GraphSelectors c= dom G
proof
let x be object;
assume x in _GraphSelectors;
then x = VertexSelector or x = EdgeSelector or x = SourceSelector or x =
TargetSelector by ENUMSET1:def 2;
hence x in dom G by Def10;
end;
theorem
the_Vertices_of GS = GS.VertexSelector & the_Edges_of GS = GS.
EdgeSelector & the_Source_of GS = GS.SourceSelector & the_Target_of GS = GS.
TargetSelector;
theorem Th4:
dom (the_Source_of G) = the_Edges_of G & dom (the_Target_of G) =
the_Edges_of G & rng (the_Source_of G) c= the_Vertices_of G & rng (
the_Target_of G) c= the_Vertices_of G by FUNCT_2:def 1;
theorem
GS is [Graph-like] iff _GraphSelectors c= dom GS & the_Vertices_of GS
is non empty & the_Source_of GS is Function of the_Edges_of GS,the_Vertices_of
GS & the_Target_of GS is Function of the_Edges_of GS,the_Vertices_of GS by Lm1;
theorem ::: obsolete as reductions are added
for V being non empty set, E being set, S,T being Function of E,V holds
the_Vertices_of createGraph(V,E,S,T) = V &
the_Edges_of createGraph(V,E,S,T) = E &
the_Source_of createGraph(V,E,S,T) = S &
the_Target_of createGraph(V,E,S,T) = T;
registration
let V be non empty set, E be set, S,T be Function of E,V;
reduce the_Vertices_of createGraph(V,E,S,T) to V;
reducibility;
reduce the_Edges_of createGraph(V,E,S,T) to E;
reducibility;
reduce the_Source_of createGraph(V,E,S,T) to S;
reducibility;
reduce the_Target_of createGraph(V,E,S,T) to T;
reducibility;
end;
theorem Th7:
dom GS.set(n,x) = dom GS \/ {n}
proof
set G2 = GS.set(n,x);
thus dom G2 = dom GS \/ dom (n.-->x) by FUNCT_4:def 1
.= dom GS \/ {n};
end;
theorem Th8:
GS.set(n,x).n = x
proof
set G2 = GS.set(n,x);
n in dom (n.-->x) by TARSKI:def 1;
hence G2.n = (n.-->x).n by FUNCT_4:13
.= x by FUNCOP_1:72;
end;
theorem Th9:
n1 <> n2 implies GS.n2 = GS.set(n1,x).n2
proof
assume n1 <> n2;
then not n2 in dom (n1.-->x) by TARSKI:def 1;
hence thesis by FUNCT_4:11;
end;
theorem
not n in _GraphSelectors implies the_Vertices_of G = the_Vertices_of G
.set(n,x) & the_Edges_of G = the_Edges_of G.set(n,x) & the_Source_of G =
the_Source_of G.set(n,x) & the_Target_of G = the_Target_of G.set(n,x) & G.set(n
,x) is _Graph
proof
set G2 = G.set(n,x);
A1: dom G c= dom G2 by FUNCT_4:10;
assume
A2: not n in _GraphSelectors;
then EdgeSelector <> n by ENUMSET1:def 2;
then
A3: not EdgeSelector in dom (n .--> x) by TARSKI:def 1;
TargetSelector <> n by A2,ENUMSET1:def 2;
then
A4: not TargetSelector in dom (n .--> x) by TARSKI:def 1;
SourceSelector <> n by A2,ENUMSET1:def 2;
then
A5: not SourceSelector in dom (n .--> x) by TARSKI:def 1;
VertexSelector <> n by A2,ENUMSET1:def 2;
then not VertexSelector in dom (n .--> x) by TARSKI:def 1;
hence
A6: the_Vertices_of G2 = the_Vertices_of G & the_Edges_of G2 =
the_Edges_of G & the_Source_of G2 = the_Source_of G & the_Target_of G2 =
the_Target_of G by A3,A5,A4,FUNCT_4:11;
A7: SourceSelector in dom G & TargetSelector in dom G by Def10;
VertexSelector in dom G & EdgeSelector in dom G by Def10;
hence thesis by A7,A1,A6,Def10;
end;
theorem
the_Vertices_of GS.set(VertexSelector,x) = x & the_Edges_of GS.set(
EdgeSelector,x) = x & the_Source_of GS.set(SourceSelector,x) = x &
the_Target_of GS.set(TargetSelector,x) = x by Th8;
theorem
n1 <> n2 implies n1 in dom GS.set(n1,x).set(n2,y) & n2 in dom GS.set(
n1,x).set(n2,y) & GS.set(n1,x).set(n2,y).n1 = x & GS.set(n1,x).set(n2,y).n2 = y
proof
assume
A1: n1 <> n2;
set G2 = GS.set(n1,x), G3 = G2.set(n2,y);
A2: dom G3 = dom G2 \/ {n2} by Th7;
dom G2 = dom GS \/ {n1} & n1 in {n1} by Th7,TARSKI:def 1;
then n1 in dom G2 by XBOOLE_0:def 3;
hence n1 in dom GS.set(n1,x).set(n2,y) by A2,XBOOLE_0:def 3;
n2 in {n2} by TARSKI:def 1;
hence n2 in dom GS.set(n1,x).set(n2,y) by A2,XBOOLE_0:def 3;
thus GS.set(n1,x).set(n2,y).n1 = G2.n1 by A1,Th9
.= x by Th8;
thus thesis by Th8;
end;
theorem
for e,x,y being object holds
e Joins x,y,G implies x in the_Vertices_of G & y in the_Vertices_of G
by FUNCT_2:5;
theorem
for e,x,y being object holds
e Joins x,y,G implies e Joins y,x,G;
theorem
for e,x1,x2,y1,y2 being object holds
e Joins x1,y1,G & e Joins x2,y2,G implies x1 = x2 & y1 = y2 or x1 = y2
& y1 = x2;
theorem
for e,x,y being object holds
e Joins x,y,G iff (e DJoins x,y,G or e DJoins y,x,G);
theorem
for e,x,y being object st
e Joins x,y,G & ( x in X & y in Y or x in Y & y in X ) holds
e SJoins X,Y,G;
theorem Th18:
G is loopless iff for v being object holds
not ex e being object st e Joins v,v,G
proof
thus G is loopless implies for v being object
holds not ex e being object st e Joins v,v,G;
assume
A1: for v being object holds not ex e being object st e Joins v,v,G;
now
given e being object such that
A2: e in the_Edges_of G & (the_Source_of G).e = (the_Target_of G).e;
set v = (the_Source_of G).e;
e Joins v,v,G by A2;
hence contradiction by A1;
end;
hence thesis;
end;
theorem
for G being loopless _Graph, v being Vertex of G holds
v.degree() = card v.edgesInOut()
proof
let G be loopless _Graph, v be Vertex of G;
set In = v.edgesIn(), Out = v.edgesOut();
now
given e being object such that
A1: e in In /\ Out;
e in Out by A1,XBOOLE_0:def 4;
then
A2: (the_Source_of G).e = v by Lm8;
e in In by A1,XBOOLE_0:def 4;
then (the_Target_of G).e = v by Lm7;
hence contradiction by A1,A2,Def18;
end;
then In /\ Out = {} by XBOOLE_0:def 1;
then In misses Out by XBOOLE_0:def 7;
hence thesis by CARD_2:35;
end;
theorem Th20:
for G being non _trivial _Graph, v being Vertex of G holds
(the_Vertices_of G) \ {v} is non empty
proof
let G be non _trivial _Graph, v be Vertex of G;
set VG = the_Vertices_of G;
now
assume VG \ {v} = {};
then VG c= {v} by XBOOLE_1:37;
then VG = {v} by ZFMISC_1:33;
then card VG = 1 by CARD_1:30;
hence contradiction by Def19;
end;
hence thesis;
end;
theorem Th21:
for G being non _trivial _Graph holds ex v1, v2 being Vertex of G st v1 <> v2
proof
let G be non _trivial _Graph;
set VG = the_Vertices_of G;
take v1 = the Element of VG;
set VG2 = VG \ {v1};
now
assume
A1: VG2 = {};
card (VG2 \/ {v1}) = card VG2 +` card {v1} by CARD_2:35,XBOOLE_1:79
.= 0 +` 1 by A1,CARD_1:30
.= card (0 +^ 1) by CARD_2:def 1
.= card (0+1) by CARD_2:36
.= 1;
then card VG = 1 by XBOOLE_1:45;
hence contradiction by Def19;
end;
then reconsider VG2 as non empty set;
set v2 = the Element of VG2;
A2: not v2 in {v1} by XBOOLE_0:def 5;
reconsider v2 as Vertex of G by XBOOLE_0:def 5;
take v2;
thus thesis by A2,TARSKI:def 1;
end;
theorem Th22:
for G being _trivial _Graph holds ex v being Vertex of G st
the_Vertices_of G = {v}
proof
let G be _trivial _Graph;
card (the_Vertices_of G) = 1 by Def19;
then consider v being object such that
A1: the_Vertices_of G = {v} by CARD_2:42;
reconsider v as Vertex of G by A1,TARSKI:def 1;
take v;
thus thesis by A1;
end;
theorem
for G being _trivial loopless _Graph holds the_Edges_of G = {}
proof
let G be _trivial loopless _Graph;
consider v being Vertex of G such that
A1: the_Vertices_of G = {v} by Th22;
now
assume the_Edges_of G <> {};
then consider e being object such that
A2: e in the_Edges_of G by XBOOLE_0:def 1;
(the_Target_of G).e in {v} by A1,A2,FUNCT_2:5;
then
A3: (the_Target_of G).e = v by TARSKI:def 1;
(the_Source_of G).e in {v} by A1,A2,FUNCT_2:5;
then (the_Source_of G).e = v by TARSKI:def 1;
hence contradiction by A2,A3,Def18;
end;
hence thesis;
end;
theorem
the_Edges_of G = {} implies G is simple
proof
assume
A1: the_Edges_of G = {};
then
A2: G is loopless;
for e1,e2,v1,v2 being object holds e1 Joins v1,v2,G & e2 Joins v1,v2,G
implies e1 = e2 by A1;
then G is non-multi;
hence thesis by A2;
end;
theorem
for G being _finite _Graph holds G.order() >= 1
proof
let G be _finite _Graph;
0+1 < G.order()+1 by NAT_1:3,XREAL_1:8;
hence thesis by NAT_1:13;
end;
theorem
for G being _Graph holds G.order() = 1 iff G is _trivial;
theorem
for G being _Graph holds G.order() = 1 iff ex v being Vertex of
G st the_Vertices_of G = {v}
proof
let G be _Graph;
hereby
assume G.order() = 1;
then consider v being object such that
A1: the_Vertices_of G = {v} by CARD_2:42;
reconsider v as Vertex of G by A1,TARSKI:def 1;
take v;
thus the_Vertices_of G = {v} by A1;
end;
given v being Vertex of G such that
A2: the_Vertices_of G = {v};
thus thesis by A2,CARD_1:30;
end;
theorem Th28:
e in the_Edges_of G & ((the_Source_of G).e in X or
(the_Target_of G).e in X) iff e in G.edgesInOut(X)
proof
hereby
assume that
A1: e in the_Edges_of G and
A2: (the_Source_of G).e in X or (the_Target_of G).e in X;
now
per cases by A2;
suppose
(the_Source_of G).e in X;
then e in G.edgesOutOf(X) by A1,Def27;
hence e in G.edgesInOut(X) by XBOOLE_0:def 3;
end;
suppose
(the_Target_of G).e in X;
then e in G.edgesInto(X) by A1,Def26;
hence e in G.edgesInOut(X) by XBOOLE_0:def 3;
end;
end;
hence e in G.edgesInOut(X);
end;
assume e in G.edgesInOut(X);
then e in G.edgesInto(X) or e in G.edgesOutOf(X) by XBOOLE_0:def 3;
hence thesis by Def26,Def27;
end;
theorem
G.edgesInto(X) c= G.edgesInOut(X) & G.edgesOutOf(X) c= G.edgesInOut(X)
by XBOOLE_0:def 3;
theorem
the_Edges_of G = G.edgesInOut(the_Vertices_of G)
proof
set EG = the_Edges_of G, SG = the_Source_of G;
now
let x be object;
hereby
assume
A1: x in EG;
then SG.x in the_Vertices_of G by FUNCT_2:5;
hence x in G.edgesInOut(the_Vertices_of G) by A1,Th28;
end;
assume x in G.edgesInOut(the_Vertices_of G);
hence x in EG;
end;
hence thesis by TARSKI:2;
end;
theorem
e in the_Edges_of G & (the_Source_of G).e in X & (the_Target_of G).e
in X iff e in G.edgesBetween(X) by Lm5;
theorem
for e,x,y being object holds
x in X & y in X & e Joins x,y,G implies e in G.edgesBetween(X) by Lm5;
theorem
G.edgesBetween(X) c= G.edgesInOut(X)
proof
let z be object;
assume z in G.edgesBetween(X);
then z in G.edgesInto(X) by XBOOLE_0:def 4;
hence z in G.edgesInOut(X) by XBOOLE_0:def 3;
end;
theorem Th34:
the_Edges_of G = G.edgesBetween(the_Vertices_of G)
proof
set EG = the_Edges_of G, SG = the_Source_of G, TG = the_Target_of G;
now
let x be object;
hereby
assume
A1: x in EG;
then SG.x in the_Vertices_of G & TG.x in the_Vertices_of G by FUNCT_2:5;
hence x in G.edgesBetween(the_Vertices_of G) by A1,Lm5;
end;
assume x in G.edgesBetween(the_Vertices_of G);
hence x in EG;
end;
hence thesis by TARSKI:2;
end;
theorem Th35:
(the_Edges_of G) \ (G.edgesInOut(X)) = G.edgesBetween( (
the_Vertices_of G) \ X)
proof
set EG = the_Edges_of G, VG = the_Vertices_of G;
set EIO = G.edgesInOut(X), EB = G.edgesBetween(VG\X);
now
let x be object;
hereby
assume
A1: x in EG \ EIO;
then
A2: (the_Target_of G).x in VG by FUNCT_2:5;
A3: not x in EIO by A1,XBOOLE_0:def 5;
then not (the_Target_of G).x in X by A1,Th28;
then
A4: (the_Target_of G).x in VG \ X by A2,XBOOLE_0:def 5;
A5: (the_Source_of G).x in VG by A1,FUNCT_2:5;
not (the_Source_of G).x in X by A1,A3,Th28;
then (the_Source_of G).x in VG \ X by A5,XBOOLE_0:def 5;
hence x in EB by A1,A4,Lm5;
end;
assume
A6: x in EB;
then (the_Target_of G).x in VG \ X by Lm5;
then
A7: not (the_Target_of G).x in X by XBOOLE_0:def 5;
(the_Source_of G).x in VG \ X by A6,Lm5;
then not (the_Source_of G).x in X by XBOOLE_0:def 5;
then not x in EIO by A7,Th28;
hence x in EG\EIO by A6,XBOOLE_0:def 5;
end;
hence thesis by TARSKI:2;
end;
theorem
X c= Y implies G.edgesBetween(X) c= G.edgesBetween(Y)
proof
assume
A1: X c= Y;
let x be object;
assume
A2: x in G.edgesBetween(X);
then (the_Source_of G).x in X & (the_Target_of G).x in X by Lm5;
hence x in G.edgesBetween(Y) by A1,A2,Lm5;
end;
theorem Th37:
for G being _Graph, X1,X2,Y1,Y2 being set st X1 c= X2 & Y1 c= Y2 holds
G.edgesBetween(X1,Y1) c= G.edgesBetween(X2,Y2)
proof
let G be _Graph, X1,X2,Y1,Y2 be set;
assume
A1: X1 c= X2 & Y1 c= Y2;
let e be object;
assume e in G.edgesBetween(X1,Y1);
then e SJoins X1,Y1,G by Def30;
then e SJoins X2,Y2,G by A1;
hence e in G.edgesBetween(X2,Y2) by Def30;
end;
theorem
for G being _Graph, X1,X2,Y1,Y2 being set st X1 c= X2 & Y1 c= Y2 holds
G.edgesDBetween(X1,Y1) c= G.edgesDBetween(X2,Y2)
proof
let G be _Graph, X1,X2,Y1,Y2 be set;
assume
A1: X1 c= X2 & Y1 c= Y2;
let e be object;
assume e in G.edgesDBetween(X1,Y1);
then e DSJoins X1,Y1,G by Def31;
then e DSJoins X2,Y2,G by A1;
hence e in G.edgesDBetween(X2,Y2) by Def31;
end;
theorem Th39:
for G being _Graph, v being Vertex of G holds v.edgesIn() = G
.edgesDBetween(the_Vertices_of G, {v}) & v.edgesOut() = G.edgesDBetween({v},
the_Vertices_of G)
proof
let G be _Graph, v be Vertex of G;
now
let e be object;
hereby
assume
A1: e in v.edgesIn();
then (the_Target_of G).e = v by Lm7;
then
A2: (the_Target_of G).e in {v} by TARSKI:def 1;
(the_Source_of G).e in the_Vertices_of G by A1,FUNCT_2:5;
then e DSJoins the_Vertices_of G,{v},G by A1,A2;
hence e in G.edgesDBetween(the_Vertices_of G, {v}) by Def31;
end;
assume
A3: e in G.edgesDBetween(the_Vertices_of G, {v});
then e DSJoins the_Vertices_of G, {v}, G by Def31;
then (the_Target_of G).e = v by TARSKI:def 1;
hence e in v.edgesIn() by A3,Lm7;
end;
hence v.edgesIn() = G.edgesDBetween(the_Vertices_of G, {v}) by TARSKI:2;
now
let e be object;
hereby
assume
A4: e in v.edgesOut();
then (the_Source_of G).e = v by Lm8;
then
A5: (the_Source_of G).e in {v} by TARSKI:def 1;
(the_Target_of G).e in the_Vertices_of G by A4,FUNCT_2:5;
then e DSJoins {v},the_Vertices_of G,G by A4,A5;
hence e in G.edgesDBetween({v},the_Vertices_of G) by Def31;
end;
assume
A6: e in G.edgesDBetween({v},the_Vertices_of G);
then e DSJoins {v},the_Vertices_of G, G by Def31;
then (the_Source_of G).e = v by TARSKI:def 1;
hence e in v.edgesOut() by A6,Lm8;
end;
hence thesis by TARSKI:2;
end;
theorem
G is Subgraph of G by Lm3;
theorem Th41:
G1 is Subgraph of G2 & G2 is Subgraph of G1 iff the_Vertices_of
G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1
= the_Source_of G2 & the_Target_of G1 = the_Target_of G2
proof
hereby
assume that
A1: G1 is Subgraph of G2 and
A2: G2 is Subgraph of G1;
A3: the_Vertices_of G2 c= the_Vertices_of G1 & the_Edges_of G2 c=
the_Edges_of G1 by A2,Def32;
the_Vertices_of G1 c= the_Vertices_of G2 & the_Edges_of G1 c=
the_Edges_of G2 by A1,Def32;
hence
A4: the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 =
the_Edges_of G2 by A3,XBOOLE_0:def 10;
then
A5: dom the_Source_of G1 = the_Edges_of G1 & dom the_Source_of G2 =
the_Edges_of G1 by FUNCT_2:def 1;
for e being object st e in dom the_Source_of G1 holds (the_Source_of G1)
.e = (the_Source_of G2).e by A1,Def32;
hence the_Source_of G1 = the_Source_of G2 by A5,FUNCT_1:2;
A6: dom the_Target_of G1 = the_Edges_of G1 & dom the_Target_of G2 =
the_Edges_of G1 by A4,FUNCT_2:def 1;
for e being object st e in dom the_Target_of G1 holds (the_Target_of G1)
.e = (the_Target_of G2).e by A1,Def32;
hence the_Target_of G1 = the_Target_of G2 by A6,FUNCT_1:2;
end;
assume that
A7: the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 =
the_Edges_of G2 and
A8: the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of G2;
for e being set st e in the_Edges_of G1 holds (the_Source_of G1).e = (
the_Source_of G2).e & (the_Target_of G1).e = (the_Target_of G2).e by A8;
hence thesis by A7,Def32;
end;
theorem
for G1 being _Graph, G2 being Subgraph of G1, x being set holds (x in
the_Vertices_of G2 implies x in the_Vertices_of G1) & (x in the_Edges_of G2
implies x in the_Edges_of G1);
theorem Th43:
for G1 being _Graph, G2 being Subgraph of G1, G3 being Subgraph
of G2 holds G3 is Subgraph of G1
proof
let G1 be _Graph, G2 be Subgraph of G1, G3 be Subgraph of G2;
A1: the_Edges_of G2 c= the_Edges_of G1;
A2: the_Vertices_of G3 c= the_Vertices_of G2;
now
thus the_Vertices_of G3 c= the_Vertices_of G1 by A2,XBOOLE_1:1;
thus the_Edges_of G3 c= the_Edges_of G1 by A1;
let e be set;
assume
A3: e in the_Edges_of G3;
hence (the_Source_of G3).e = (the_Source_of G2).e by Def32
.= (the_Source_of G1).e by A3,Def32;
thus (the_Target_of G3).e = (the_Target_of G2).e by A3,Def32
.= (the_Target_of G1).e by A3,Def32;
end;
hence thesis by Def32;
end;
theorem Th44:
for G being _Graph, G1, G2 being Subgraph of G st
the_Vertices_of G1 c= the_Vertices_of G2 & the_Edges_of G1 c= the_Edges_of G2
holds G1 is Subgraph of G2
proof
let G be _Graph, G1, G2 be Subgraph of G;
assume that
A1: the_Vertices_of G1 c= the_Vertices_of G2 and
A2: the_Edges_of G1 c= the_Edges_of G2;
now
let e be set;
assume
A3: e in the_Edges_of G1;
hence (the_Source_of G1).e = (the_Source_of G).e by Def32
.= (the_Source_of G2).e by A2,A3,Def32;
thus (the_Target_of G1).e = (the_Target_of G).e by A3,Def32
.= (the_Target_of G2).e by A2,A3,Def32;
end;
hence thesis by A1,A2,Def32;
end;
theorem Th45:
for G1 being _Graph, G2 being Subgraph of G1 holds the_Source_of
G2 = (the_Source_of G1) | the_Edges_of G2 & the_Target_of G2 = (the_Target_of
G1) | the_Edges_of G2
proof
let G1 be _Graph, G2 be Subgraph of G1;
set S2 = (the_Source_of G1) | the_Edges_of G2;
set T2 = (the_Target_of G1) | the_Edges_of G2;
A1: now
let x be object;
assume
A2: x in dom the_Source_of G2;
hence (the_Source_of G2).x = (the_Source_of G1).x by Def32
.= S2.x by A2,FUNCT_1:49;
end;
dom the_Source_of G1 = the_Edges_of G1 by FUNCT_2:def 1;
then dom the_Source_of G2 = the_Edges_of G2 & dom S2 = the_Edges_of G2 by
FUNCT_2:def 1,RELAT_1:62;
hence the_Source_of G2 = S2 by A1,FUNCT_1:2;
A3: now
let x be object;
assume
A4: x in dom the_Target_of G2;
hence (the_Target_of G2).x = (the_Target_of G1).x by Def32
.= T2.x by A4,FUNCT_1:49;
end;
dom the_Target_of G1 = the_Edges_of G1 by FUNCT_2:def 1;
then dom the_Target_of G2 = the_Edges_of G2 & dom T2 = the_Edges_of G2 by
FUNCT_2:def 1,RELAT_1:62;
hence thesis by A3,FUNCT_1:2;
end;
theorem
for G being _Graph, V1,V2,E1,E2 being set, G1 being inducedSubgraph of
G,V1,E1, G2 being inducedSubgraph of G,V2,E2 st V2 c= V1 & E2 c= E1 & V2 is non
empty Subset of the_Vertices_of G & E2 c= G.edgesBetween(V2) holds G2 is
Subgraph of G1
proof
let G be _Graph, V1,V2,E1,E2 be set, G1 be inducedSubgraph of G,V1,E1, G2 be
inducedSubgraph of G,V2,E2;
assume that
A1: V2 c= V1 & E2 c= E1 and
A2: V2 is non empty Subset of the_Vertices_of G & E2 c= G.edgesBetween( V2);
A3: the_Vertices_of G2 = V2 & the_Edges_of G2 = E2 by A2,Def37;
now
per cases;
suppose
V1 is non empty Subset of the_Vertices_of G & E1 c= G .edgesBetween(V1);
then the_Vertices_of G1 = V1 & the_Edges_of G1 = E1 by Def37;
hence thesis by A1,A3,Th44;
end;
suppose
not (V1 is non empty Subset of the_Vertices_of G & E1 c= G
.edgesBetween(V1));
then G1 == G by Def37;
hence thesis by A3,Th44;
end;
end;
hence thesis;
end;
theorem Th47:
for G1 being non _trivial _Graph, v being Vertex of G1, G2 being
removeVertex of G1,v holds the_Vertices_of G2 = the_Vertices_of G1 \ {v} &
the_Edges_of G2 = G1.edgesBetween(the_Vertices_of G1 \ {v})
proof
let G1 be non _trivial _Graph,v be Vertex of G1,
G2 be removeVertex of G1,v;
set VG = the_Vertices_of G1, V = VG \ {v};
now
assume V is empty;
then VG c= {v} by XBOOLE_1:37;
then VG = {v} by ZFMISC_1:33;
then card VG = 1 by CARD_1:30;
hence contradiction by Def19;
end;
then reconsider V as non empty Subset of VG;
G2 is inducedSubgraph of G1,V;
hence thesis by Def37;
end;
theorem
for G1 being _finite non _trivial _Graph, v being Vertex of G1, G2 being
removeVertex of G1,v holds G2.order() + 1 = G1.order() & G2.size() + card v
.edgesInOut() = G1.size()
proof
let G1 be _finite non _trivial _Graph, v be Vertex of G1,
G2 be removeVertex of G1,v;
set VG1 = the_Vertices_of G1, VG2 = the_Vertices_of G2;
set EG1 = the_Edges_of G1, EG2 = the_Edges_of G2, EV = v.edgesInOut();
A1: VG2 = VG1 \ {v} by Th47;
v in {v} by TARSKI:def 1;
then not v in VG2 by A1,XBOOLE_0:def 5;
then card (( VG1 \ {v}) \/ {v}) = G2.order() + 1 by A1,CARD_2:41;
hence G2.order() + 1 = G1.order() by XBOOLE_1:45;
A2: EG2 = G1.edgesBetween(VG1 \ {v}) & G1.edgesBetween(VG1 \ {v}) = EG1 \ EV
by Th35,Th47;
then EG1 = EG2 \/ EV by XBOOLE_1:45;
hence thesis by A2,CARD_2:40,XBOOLE_1:79;
end;
theorem Th49:
for G1 being _Graph, V being set, G2 being removeVertices of G1,
V st V c< the_Vertices_of G1 holds the_Vertices_of G2 = the_Vertices_of G1 \ V
& the_Edges_of G2 = G1.edgesBetween(the_Vertices_of G1 \ V)
proof
let G1 be _Graph, V be set, G2 be removeVertices of G1,V;
set VG2 = the_Vertices_of G1 \ V;
assume
A1: V c< the_Vertices_of G1;
now
assume VG2 is empty;
then the_Vertices_of G1 c= V by XBOOLE_1:37;
hence contradiction by A1,XBOOLE_0:def 8;
end;
then reconsider VG2 as non empty Subset of the_Vertices_of G1;
G2 is inducedSubgraph of G1,VG2;
hence thesis by Def37;
end;
theorem
for G1 being _finite _Graph, V being Subset of the_Vertices_of G1, G2
being removeVertices of G1,V st V <> the_Vertices_of G1 holds G2.order() + card
V = G1.order() & G2.size() + card G1.edgesInOut(V) = G1.size()
proof
let G1 be _finite _Graph, V be Subset of the_Vertices_of G1, G2 be
removeVertices of G1,V;
set VG1 = the_Vertices_of G1, VG2 = the_Vertices_of G2;
set EG1 = the_Edges_of G1, EG2 = the_Edges_of G2;
A1: G1.edgesBetween(VG1 \ V) = EG1 \ G1.edgesInOut(V) by Th35;
assume V <> VG1;
then
A2: V c< VG1 by XBOOLE_0:def 8;
then
A3: VG2 = VG1 \ V by Th49;
then card (VG2 \/ V) = card VG2 + card V by CARD_2:40,XBOOLE_1:79;
hence G2.order() + card V = G1.order() by A3,XBOOLE_1:45;
A4: EG2 = G1.edgesBetween(VG1 \ V) by A2,Th49;
then EG1 = EG2 \/ G1.edgesInOut(V) by A1,XBOOLE_1:45;
hence thesis by A4,A1,CARD_2:40,XBOOLE_1:79;
end;
theorem Th51:
for G1 being _Graph, e being set, G2 being removeEdge of G1,e
holds the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = the_Edges_of
G1 \ {e}
proof
let G1 be _Graph, e be set, G2 be removeEdge of G1,e;
set V = the_Vertices_of G1;
V c= V;
then reconsider V as non empty Subset of the_Vertices_of G1;
set E = the_Edges_of G1 \ {e};
reconsider E as Subset of G1.edgesBetween(V) by Th34;
G2 is inducedSubgraph of G1,V,E;
hence thesis by Def37;
end;
theorem
for G1 being _finite _Graph, e being set, G2 being removeEdge of G1,e
holds G1.order() = G2.order() & (e in the_Edges_of G1 implies G2.size() + 1 =
G1.size())
proof
let G1 be _finite _Graph, e be set, G2 be removeEdge of G1,e;
A1: the_Edges_of G2 = the_Edges_of G1 \ {e} by Th51;
thus G1.order() = G2.order() by Th51;
assume e in the_Edges_of G1;
then for x being object st x in {e} holds x in the_Edges_of G1
by TARSKI:def 1;
then {e} c= the_Edges_of G1;
then
A2: the_Edges_of G1 = the_Edges_of G2 \/ {e} by A1,XBOOLE_1:45;
e in {e} by TARSKI:def 1;
then not e in the_Edges_of G2 by A1,XBOOLE_0:def 5;
hence thesis by A2,CARD_2:41;
end;
theorem Th53:
for G1 being _Graph, E being set, G2 being removeEdges of G1,E
holds the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = the_Edges_of
G1 \ E
proof
let G1 be _Graph, E be set, G2 be removeEdges of G1,E;
set V = the_Vertices_of G1;
V c= V;
then reconsider V as non empty Subset of the_Vertices_of G1;
set E2 = the_Edges_of G1 \ E;
reconsider E2 as Subset of G1.edgesBetween(V) by Th34;
G2 is inducedSubgraph of G1,V,E2;
hence thesis by Def37;
end;
theorem
for G1 being _Graph, E being set, G2 being removeEdges of G1,E
holds G1.order() = G2.order() by Th53;
theorem
for G1 being _finite _Graph, E being Subset of the_Edges_of G1, G2
being removeEdges of G1,E holds G2.size() + card E = G1.size()
proof
let G1 be _finite _Graph, E be Subset of the_Edges_of G1, G2 be removeEdges
of G1,E;
A1: the_Edges_of G2 = the_Edges_of G1 \ E by Th53;
then the_Edges_of G1 = the_Edges_of G2 \/ E by XBOOLE_1:45;
hence thesis by A1,CARD_2:40,XBOOLE_1:79;
end;
theorem
e in v.edgesIn() iff e in the_Edges_of G & (the_Target_of G).e = v by Lm7;
theorem Th57:
e in v.edgesIn() iff ex x being set st e DJoins x,v,G
proof
hereby
set x = (the_Source_of G).e;
assume
A1: e in v.edgesIn();
take x;
(the_Target_of G).e = v by A1,Lm7;
hence e DJoins x,v,G by A1;
end;
given x being set such that
A2: e DJoins x,v,G;
e in the_Edges_of G & (the_Target_of G).e = v by A2;
hence thesis by Lm7;
end;
theorem
e in v.edgesOut() iff e in the_Edges_of G & (the_Source_of G).e = v by Lm8;
theorem Th59:
e in v.edgesOut() iff ex x being set st e DJoins v,x,G
proof
hereby
set x = (the_Target_of G).e;
assume
A1: e in v.edgesOut();
take x;
(the_Source_of G).e = v by A1,Lm8;
hence e DJoins v,x,G by A1;
end;
given x being set such that
A2: e DJoins v,x,G;
e in the_Edges_of G & (the_Source_of G).e = v by A2;
hence thesis by Lm8;
end;
theorem
v.edgesInOut() = v.edgesIn() \/ v.edgesOut();
theorem Th61:
e in v.edgesInOut() iff e in the_Edges_of G & ((the_Source_of G)
.e = v or (the_Target_of G).e = v)
proof
hereby
assume
A1: e in v.edgesInOut();
hence e in the_Edges_of G;
e in v.edgesIn() or e in v.edgesOut() by A1,XBOOLE_0:def 3;
hence (the_Source_of G).e=v or (the_Target_of G).e=v by Lm7,Lm8;
end;
assume
e in the_Edges_of G &( (the_Source_of G).e=v or (the_Target_of G).e= v);
then e in v.edgesIn() or e in v.edgesOut() by Lm7,Lm8;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th62:
for e,x being object holds
e Joins v1,x,G implies e in v1.edgesInOut() by Th61;
theorem Th63:
e Joins v1,v2,G implies e in v1.edgesIn() & e in v2.edgesOut()
or e in v2.edgesIn() & e in v1.edgesOut()
proof
assume
A1: e Joins v1,v2,G;
then
A2: e in the_Edges_of G;
now
per cases by A1;
suppose
(the_Source_of G).e = v1 & (the_Target_of G).e = v2;
hence thesis by A2,Lm7,Lm8;
end;
suppose
(the_Source_of G).e = v2 & (the_Target_of G).e = v1;
hence thesis by A2,Lm7,Lm8;
end;
end;
hence thesis;
end;
theorem Th64:
e in v1.edgesInOut() iff ex v2 being Vertex of G st e Joins v1,v2,G
proof
hereby
assume
A1: e in v1.edgesInOut();
now
per cases by A1,Th61;
suppose
A2: (the_Source_of G).e = v1;
set v2 = (the_Target_of G).e;
reconsider v2 as Vertex of G by A1,FUNCT_2:5;
take v2;
thus e Joins v1, v2, G by A1,A2;
end;
suppose
A3: (the_Target_of G).e = v1;
set v2 = (the_Source_of G).e;
reconsider v2 as Vertex of G by A1,FUNCT_2:5;
take v2;
thus e Joins v1,v2,G by A1,A3;
end;
end;
hence ex v2 being Vertex of G st e Joins v1,v2,G;
end;
given v2 being Vertex of G such that
A4: e Joins v1,v2,G;
thus thesis by A4,Th62;
end;
theorem
for e,x,y being object holds
e in v.edgesInOut() & e Joins x,y,G implies v = x or v = y
proof let e,x,y be object;
assume that
A1: e in v.edgesInOut() and
A2: e Joins x,y,G;
now
assume
A3: v <> x;
now
per cases by A1,Th61;
suppose
(the_Source_of G).e = v;
hence v = y by A2,A3;
end;
suppose
(the_Target_of G).e = v;
hence v = y by A2,A3;
end;
end;
hence v = y;
end;
hence thesis;
end;
theorem
for e being object holds
e Joins v1,v2,G implies v1.adj(e) = v2 & v2.adj(e) = v1
proof let e be object;
assume
A1: e Joins v1, v2,G;
then
A2: e in v1.edgesInOut() by Th62;
now
per cases by A1;
suppose
A3: (the_Source_of G).e = v2 & (the_Target_of G).e = v1;
hence v1.adj(e) = v2 by A2,Def41;
now
per cases;
suppose
v1 = v2;
hence v2.adj(e) = v1 by A2,A3,Def41;
end;
suppose
v1 <> v2;
hence v2.adj(e) = v1 by A2,A3,Def41;
end;
end;
hence v2.adj(e) = v1;
end;
suppose
A4: (the_Source_of G).e = v1 & (the_Target_of G).e = v2;
now
per cases;
suppose
v1 = v2;
hence v1.adj(e) = v2 by A2,A4,Def41;
end;
suppose
v1 <> v2;
hence v1.adj(e) = v2 by A2,A4,Def41;
end;
end;
hence v1.adj(e) = v2;
thus v2.adj(e) = v1 by A2,A4,Def41;
end;
end;
hence thesis;
end;
theorem Th67:
e in v.edgesInOut() iff e Joins v,v.adj(e),G
proof
hereby
assume
A1: e in v.edgesInOut();
then
A2: (the_Source_of G).e = v or (the_Target_of G).e = v by Th61;
now
per cases;
suppose
A3: (the_Target_of G).e = v;
then v.adj(e) = (the_Source_of G).e by A1,Def41;
hence e Joins v,v.adj(e),G by A1,A3;
end;
suppose
A4: (the_Target_of G).e <> v;
then v.adj(e) = (the_Target_of G).e by A1,A2,Def41;
hence e Joins v,v.adj(e),G by A1,A2,A4;
end;
end;
hence e Joins v,v.adj(e),G;
end;
assume e Joins v,v.adj(e),G;
hence thesis by Th62;
end;
theorem
for G being _finite _Graph, e being set, v1,v2 being Vertex of G holds
e Joins v1,v2,G implies 1 <= v1.degree() & 1 <= v2.degree()
proof
let G be _finite _Graph, e be set, v1, v2 be Vertex of G;
assume
A1: e Joins v1, v2,G;
now
per cases by A1,Th63;
suppose
A2: e in v1.edgesIn() & e in v2.edgesOut();
then for x being object st x in {e}
holds x in v1.edgesIn() by TARSKI:def 1;
then {e} c= v1.edgesIn();
then card {e} <= card v1.edgesIn() by NAT_1:43;
then 1 <= v1.inDegree() by CARD_1:30;
hence 1 <= v1.degree() by NAT_1:12;
for x being object
st x in {e} holds x in v2.edgesOut() by A2,TARSKI:def 1;
then {e} c= v2.edgesOut();
then card {e} <= card v2.edgesOut() by NAT_1:43;
then 1 <= v2.outDegree() by CARD_1:30;
hence 1 <= v2.degree() by NAT_1:12;
end;
suppose
A3: e in v2.edgesIn() & e in v1.edgesOut();
then for x being object
st x in {e} holds x in v1.edgesOut() by TARSKI:def 1;
then {e} c= v1.edgesOut();
then card {e} <= card v1.edgesOut() by NAT_1:43;
then 1 <= v1.outDegree() by CARD_1:30;
hence 1 <= v1.degree() by NAT_1:12;
for x being object
st x in {e} holds x in v2.edgesIn() by A3,TARSKI:def 1;
then {e} c= v2.edgesIn();
then card {e} <= card v2.edgesIn() by NAT_1:43;
then 1 <= v2.inDegree() by CARD_1:30;
hence 1 <= v2.degree() by NAT_1:12;
end;
end;
hence thesis;
end;
theorem Th69:
x in v.inNeighbors() iff ex e being object st e DJoins x,v,G
proof
hereby
assume x in v.inNeighbors();
then consider e being object such that
A1: e in dom (the_Source_of G) and
A2: e in v.edgesIn() and
A3: x = (the_Source_of G).e by FUNCT_1:def 6;
take e;
(the_Target_of G).e = v by A2,Lm7;
hence e DJoins x,v,G by A1,A3;
end;
given e being object such that
A4: e DJoins x,v,G;
A5: e in the_Edges_of G by A4;
then
A6: e in dom (the_Source_of G) by FUNCT_2:def 1;
(the_Target_of G).e = v by A4;
then
A7: e in v.edgesIn() by A5,Lm7;
(the_Source_of G).e = x by A4;
hence thesis by A7,A6,FUNCT_1:def 6;
end;
theorem Th70:
x in v.outNeighbors() iff ex e being object st e DJoins v,x,G
proof
hereby
assume x in v.outNeighbors();
then consider e being object such that
A1: e in dom (the_Target_of G) and
A2: e in v.edgesOut() and
A3: x = (the_Target_of G).e by FUNCT_1:def 6;
take e;
(the_Source_of G).e = v by A2,Lm8;
hence e DJoins v,x,G by A1,A3;
end;
given e being object such that
A4: e DJoins v,x,G;
A5: e in the_Edges_of G by A4;
then
A6: e in dom (the_Target_of G) by FUNCT_2:def 1;
(the_Source_of G).e = v by A4;
then
A7: e in v.edgesOut() by A5,Lm8;
(the_Target_of G).e = x by A4;
hence thesis by A7,A6,FUNCT_1:def 6;
end;
theorem Th71:
x in v.allNeighbors() iff ex e being object st e Joins v,x,G
proof
hereby
assume
A1: x in v.allNeighbors();
now
per cases by A1,XBOOLE_0:def 3;
suppose
x in v.inNeighbors();
then consider e being object such that
A2: e DJoins x,v,G by Th69;
take e;
thus e Joins v,x,G by A2;
end;
suppose
x in v.outNeighbors();
then consider e being object such that
A3: e DJoins v,x,G by Th70;
take e;
thus e Joins v,x,G by A3;
end;
end;
hence ex e being object st e Joins v,x,G;
end;
given e being object such that
A4: e Joins v,x,G;
now
per cases by A4;
suppose
e DJoins x,v,G;
then x in v.inNeighbors() by Th69;
hence x in v.inNeighbors() \/ v.outNeighbors() by XBOOLE_0:def 3;
end;
suppose
e DJoins v,x,G;
then x in v.outNeighbors() by Th70;
hence x in v.inNeighbors() \/ v.outNeighbors() by XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
theorem Th72:
for G1 being _Graph, G2 being Subgraph of G1,
x,y being set, e being object
holds (e Joins x,y,G2 implies e Joins x,y,G1) & (e DJoins x,y,G2 implies e
DJoins x,y,G1) & (e SJoins x,y,G2 implies e SJoins x,y,G1) & (e DSJoins x,y,G2
implies e DSJoins x,y,G1)
proof
let G1 be _Graph, G2 be Subgraph of G1, x,y be set, e be object;
thus e Joins x,y,G2 implies e Joins x,y,G1 by Lm4;
hereby
assume
A1: e DJoins x,y,G2;
then
A2: e in the_Edges_of G2;
(the_Target_of G2) .e=y by A1;
then
A3: (the_Target_of G1).e = y by A2,Def32;
(the_Source_of G2).e=x by A1;
then (the_Source_of G1).e = x by A2,Def32;
hence e DJoins x,y,G1 by A2,A3;
end;
hereby
assume
A4: e SJoins x,y,G2;
then
A5: (the_Source_of G2).e in x & (the_Target_of G2).e in y or (
the_Source_of G2).e in y & (the_Target_of G2).e in x;
A6: e in the_Edges_of G2 by A4;
then (the_Source_of G2).e = (the_Source_of G1).e & (the_Target_of G2).e =
( the_Target_of G1).e by Def32;
hence e SJoins x,y,G1 by A6,A5;
end;
assume
A7: e DSJoins x,y,G2;
then
A8: (the_Source_of G2).e in x & (the_Target_of G2).e in y;
A9: e in the_Edges_of G2 by A7;
then (the_Source_of G2).e = (the_Source_of G1).e & (the_Target_of G2).e = (
the_Target_of G1).e by Def32;
hence thesis by A9,A8;
end;
theorem
for G1 being _Graph, G2 being Subgraph of G1, x,y,e being set st e in
the_Edges_of G2 holds (e Joins x,y,G1 implies e Joins x,y,G2) & (e DJoins x,y,
G1 implies e DJoins x,y,G2) & (e SJoins x,y,G1 implies e SJoins x,y,G2) & (e
DSJoins x,y,G1 implies e DSJoins x,y,G2)
by Def32;
theorem
for G1 being _Graph, G2 being spanning Subgraph of G1, G3 being
spanning Subgraph of G2 holds G3 is spanning Subgraph of G1
proof
let G1 be _Graph, G2 be spanning Subgraph of G1, G3 be spanning Subgraph of
G2;
the_Vertices_of G3 = the_Vertices_of G2 by Def33
.= the_Vertices_of G1 by Def33;
hence thesis by Def33,Th43;
end;
theorem
for G1 being _finite _Graph, G2 being Subgraph of G1 holds G2.order()
<= G1.order() & G2.size() <= G1.size()
proof
let G1 be _finite _Graph, G2 be Subgraph of G1;
card the_Vertices_of G2 <= card the_Vertices_of G1 by NAT_1:43;
hence G2.order() <= G1.order();
card the_Edges_of G2 <= card the_Edges_of G1 by NAT_1:43;
hence thesis;
end;
theorem Th76:
for G1 being _Graph, G2 being Subgraph of G1, X being set holds G2
.edgesInto(X) c= G1.edgesInto(X) & G2.edgesOutOf(X) c= G1.edgesOutOf(X) & G2
.edgesInOut(X) c= G1.edgesInOut(X) & G2.edgesBetween(X) c= G1.edgesBetween(X)
proof
let G1 be _Graph, G2 be Subgraph of G1, X be set;
now
let e be object;
assume
A1: e in G2.edgesInto(X);
then
A2: (the_Target_of G2).e = (the_Target_of G1).e by Def32;
e in the_Edges_of G2 & (the_Target_of G2).e in X by A1,Def26;
hence e in G1.edgesInto(X) by A2,Def26;
end;
hence
A3: G2.edgesInto(X) c= G1.edgesInto(X);
then
A4: G2.edgesInto(X) c= G1.edgesInOut(X) by XBOOLE_1:10;
now
let e be object;
assume
A5: e in G2.edgesOutOf(X);
then
A6: (the_Source_of G2).e = (the_Source_of G1).e by Def32;
e in the_Edges_of G2 & (the_Source_of G2).e in X by A5,Def27;
hence e in G1.edgesOutOf(X) by A6,Def27;
end;
hence
A7: G2.edgesOutOf(X) c= G1.edgesOutOf(X);
then G2.edgesOutOf(X) c= G1.edgesInOut(X) by XBOOLE_1:10;
hence G2.edgesInOut(X) c= G1.edgesInOut(X) by A4,XBOOLE_1:8;
thus thesis by A3,A7,XBOOLE_1:27;
end;
theorem
for G1 being _Graph, G2 being Subgraph of G1, X,Y being set holds G2
.edgesBetween(X,Y) c= G1.edgesBetween(X,Y) & G2.edgesDBetween(X,Y) c= G1
.edgesDBetween(X,Y)
proof
let G1 be _Graph, G2 be Subgraph of G1, X,Y be set;
now
let x be object;
assume x in G2.edgesBetween(X,Y);
then x SJoins X,Y,G2 by Def30;
then x SJoins X,Y,G1 by Th72;
hence x in G1.edgesBetween(X,Y) by Def30;
end;
hence G2.edgesBetween(X,Y) c= G1.edgesBetween(X,Y);
now
let x be object;
assume x in G2.edgesDBetween(X,Y);
then x DSJoins X,Y,G2 by Def31;
then x DSJoins X,Y,G1 by Th72;
hence x in G1.edgesDBetween(X,Y) by Def31;
end;
hence thesis;
end;
theorem Th78:
for G1 being _Graph, G2 being Subgraph of G1, v1 being Vertex of
G1, v2 being Vertex of G2 st v1 = v2 holds v2.edgesIn() c= v1.edgesIn() & v2
.edgesOut() c= v1.edgesOut() & v2.edgesInOut() c= v1.edgesInOut()
proof
let G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of
G2;
assume
A1: v1 = v2;
now
let x be object;
assume
A2: x in v2.edgesIn();
then (the_Target_of G2).x = v2 by Lm7;
then
A3: (the_Target_of G1).x = v1 by A1,A2,Def32;
x in the_Edges_of G2 by A2;
hence x in v1.edgesIn() by A3,Lm7;
end;
hence v2.edgesIn() c= v1.edgesIn();
now
let x be object;
assume
A4: x in v2.edgesOut();
then (the_Source_of G2).x = v2 by Lm8;
then
A5: (the_Source_of G1).x = v1 by A1,A4,Def32;
x in the_Edges_of G2 by A4;
hence x in v1.edgesOut() by A5,Lm8;
end;
hence v2.edgesOut() c= v1.edgesOut();
now
let x be object;
assume
A6: x in v2.edgesInOut();
then (the_Source_of G2).x = v2 or (the_Target_of G2).x = v2 by Th61;
then
A7: (the_Source_of G1).x = v1 or (the_Target_of G1).x=v1 by A1,A6,Def32;
x in the_Edges_of G2 by A6;
hence x in v1.edgesInOut() by A7,Th61;
end;
hence thesis;
end;
theorem Th79:
for G1 being _Graph, G2 being Subgraph of G1, v1 being Vertex of
G1, v2 being Vertex of G2 st v1 = v2 holds v2.edgesIn() = v1.edgesIn() /\ (
the_Edges_of G2) & v2.edgesOut() = v1.edgesOut() /\ (the_Edges_of G2) & v2
.edgesInOut() = v1.edgesInOut() /\ (the_Edges_of G2)
proof
let G1 be _Graph, G2 be Subgraph of G1, 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.edgesIn();
v2.edgesIn() c= v1.edgesIn() by A1,Th78;
hence x in v1.edgesIn()/\(the_Edges_of G2) by A2,XBOOLE_0:def 4;
end;
assume
A3: x in v1.edgesIn() /\ (the_Edges_of G2);
then
A4: x in the_Edges_of G2 by XBOOLE_0:def 4;
x in v1.edgesIn() by A3,XBOOLE_0:def 4;
then (the_Target_of G1).x = v1 by Lm7;
then (the_Target_of G2).x = v2 by A1,A4,Def32;
hence x in v2.edgesIn() by A4,Lm7;
end;
hence
A5: v2.edgesIn() = v1.edgesIn() /\ (the_Edges_of G2) by TARSKI:2;
now
let x be object;
hereby
assume
A6: x in v2.edgesOut();
v2.edgesOut() c= v1.edgesOut() by A1,Th78;
hence x in v1.edgesOut() /\ (the_Edges_of G2) by A6,XBOOLE_0:def 4;
end;
assume
A7: x in v1.edgesOut() /\ (the_Edges_of G2);
then
A8: x in the_Edges_of G2 by XBOOLE_0:def 4;
x in v1.edgesOut() by A7,XBOOLE_0:def 4;
then (the_Source_of G1).x = v1 by Lm8;
then (the_Source_of G2).x = v2 by A1,A8,Def32;
hence x in v2.edgesOut() by A8,Lm8;
end;
hence
A9: v2.edgesOut() = v1.edgesOut() /\ (the_Edges_of G2) by TARSKI:2;
now
let x be object;
hereby
assume
A10: x in v1.edgesInOut() /\ (the_Edges_of G2);
then
A11: x in the_Edges_of G2 by XBOOLE_0:def 4;
A12: x in v1.edgesInOut() by A10,XBOOLE_0:def 4;
now
per cases by A12,XBOOLE_0:def 3;
suppose
x in v1.edgesIn();
then x in v1.edgesIn()/\(the_Edges_of G2) by A11,XBOOLE_0:def 4;
hence x in v2.edgesInOut() by A5,XBOOLE_0:def 3;
end;
suppose
x in v1.edgesOut();
then x in v1.edgesOut()/\(the_Edges_of G2) by A11,XBOOLE_0:def 4;
hence x in v2.edgesInOut() by A9,XBOOLE_0:def 3;
end;
end;
hence x in v2.edgesInOut();
end;
assume
A13: x in v2.edgesInOut();
now
per cases by A5,A9,A13,XBOOLE_0:def 3;
suppose
A14: x in v1.edgesIn() /\ (the_Edges_of G2);
then x in v1.edgesIn() by XBOOLE_0:def 4;
then
A15: x in v1.edgesIn() \/ v1.edgesOut() by XBOOLE_0:def 3;
x in the_Edges_of G2 by A14,XBOOLE_0:def 4;
hence x in v1.edgesInOut() /\ (the_Edges_of G2) by A15,XBOOLE_0:def 4;
end;
suppose
A16: x in v1.edgesOut() /\ (the_Edges_of G2);
then x in v1.edgesOut() by XBOOLE_0:def 4;
then
A17: x in v1.edgesIn() \/ v1.edgesOut() by XBOOLE_0:def 3;
x in (the_Edges_of G2) by A16,XBOOLE_0:def 4;
hence x in v1.edgesInOut() /\ (the_Edges_of G2) by A17,XBOOLE_0:def 4;
end;
end;
hence x in v1.edgesInOut() /\ (the_Edges_of G2);
end;
hence thesis by TARSKI:2;
end;
theorem
for G1 being _Graph, G2 being Subgraph of G1, v1 being Vertex of G1,
v2 being Vertex of G2, e being set st v1 = v2 & e in the_Edges_of G2 holds v1
.adj(e) = v2.adj(e)
proof
let G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of
G2, e be set;
assume that
A1: v1 = v2 and
A2: e in the_Edges_of G2;
A3: (the_Source_of G2).e = (the_Source_of G1).e & (the_Target_of G2).e = (
the_Target_of G1).e by A2,Def32;
now
per cases;
suppose
A4: (the_Target_of G1).e = v1;
hence v1.adj(e) = (the_Source_of G1).e by A2,Def41
.= v2.adj(e) by A1,A2,A3,A4,Def41;
end;
suppose
A5: (the_Source_of G1).e = v1 & (the_Target_of G1).e <> v1;
hence v1.adj(e) = (the_Target_of G1).e by A2,Def41
.= v2.adj(e) by A1,A2,A3,A5,Def41;
end;
suppose
A6: (the_Source_of G1).e <> v1 & (the_Target_of G1).e <> v1;
hence v1.adj(e) = v2 by A1,Def41
.= v2.adj(e) by A1,A3,A6,Def41;
end;
end;
hence thesis;
end;
theorem
for G1 being _finite _Graph, G2 being Subgraph of G1, v1 being Vertex
of G1, v2 being Vertex of G2 st v1 = v2 holds v2.inDegree() <= v1.inDegree() &
v2.outDegree() <= v1.outDegree() & v2.degree() <= v1.degree()
proof
let G1 be _finite _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be
Vertex of G2;
assume
A1: v1 = v2;
then v2.edgesIn() = v1.edgesIn() /\ (the_Edges_of G2) by Th79;
hence
A2: v2.inDegree() <= v1.inDegree() by NAT_1:43,XBOOLE_1:17;
A3: v2.edgesOut() = v1.edgesOut()/\(the_Edges_of G2) by A1,Th79;
hence v2.outDegree() <= v1.outDegree() by NAT_1:43,XBOOLE_1:17;
v2.outDegree() <= card v1.edgesOut() by A3,NAT_1:43,XBOOLE_1:17;
hence thesis by A2,XREAL_1:7;
end;
theorem
for G1 being _Graph, G2 being Subgraph of G1, v1 being Vertex of G1,
v2 being Vertex of G2 st v1 = v2 holds v2.inNeighbors() c= v1.inNeighbors() &
v2.outNeighbors() c= v1.outNeighbors() & v2.allNeighbors() c= v1.allNeighbors()
proof
let G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of
G2;
assume
A1: v1 = v2;
now
let v be object;
assume v in v2.inNeighbors();
then consider e being object such that
A2: e DJoins v,v2,G2 by Th69;
e DJoins v,v1,G1 by A1,A2,Th72;
hence v in v1.inNeighbors() by Th69;
end;
hence v2.inNeighbors() c= v1.inNeighbors();
now
let v be object;
assume v in v2.outNeighbors();
then consider e being object such that
A3: e DJoins v2,v,G2 by Th70;
e DJoins v1,v,G1 by A1,A3,Th72;
hence v in v1.outNeighbors() by Th70;
end;
hence v2.outNeighbors() c= v1.outNeighbors();
let v be object;
assume v in v2.allNeighbors();
then consider e being object such that
A4: e Joins v2,v,G2 by Th71;
e Joins v1,v,G1 by A1,A4,Lm4;
hence v in v1.allNeighbors() by Th71;
end;
theorem
for G1 being _Graph, G2 being Subgraph of G1, v1 being Vertex of G1,
v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds v2 is isolated
proof
let G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of
G2;
assume v1 = v2 & v1 is isolated;
then v1.edgesInOut() = {} & v2.edgesInOut() c= v1.edgesInOut() by Th78;
hence thesis;
end;
theorem
for G1 being _Graph, G2 being Subgraph of G1, v1 being Vertex of G1,
v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds v2 is endvertex or v2
is isolated
proof
let G1 be _Graph, G2 be Subgraph of G1, v1 be Vertex of G1, v2 be Vertex of
G2;
assume that
A1: v1 = v2 and
A2: v1 is endvertex;
consider e being object such that
A3: v1.edgesInOut() = {e} and
A4: not e Joins v1,v1,G1 by A2;
v2.edgesInOut() c= v1.edgesInOut() by A1,Th78;
then
A5: v2.edgesInOut() = {} or v2.edgesInOut() = {e} by A3,ZFMISC_1:33;
v2 is not isolated implies v2 is endvertex by A5,A1,A4,Lm4;
hence thesis;
end;
theorem
G1 == G2 & G2 == G3 implies G1 == G3;
theorem Th86:
for G being _Graph, G1,G2 being Subgraph of G st the_Vertices_of
G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 holds G1 == G2
proof
let G be _Graph, G1,G2 be Subgraph of G;
assume that
A1: the_Vertices_of G1 = the_Vertices_of G2 and
A2: the_Edges_of G1 = the_Edges_of G2;
A3: dom (the_Target_of G1) = the_Edges_of G1 & dom (the_Target_of G2) =
the_Edges_of G2 by FUNCT_2:def 1;
now
let e be object;
assume
A4: e in the_Edges_of G1;
then (the_Target_of G1).e = (the_Target_of G).e by Def32;
hence (the_Target_of G1).e = (the_Target_of G2).e by A2,A4,Def32;
end;
then
A5: the_Target_of G1 = the_Target_of G2 by A2,A3,FUNCT_1:2;
A6: now
let e be object;
assume
A7: e in the_Edges_of G1;
then (the_Source_of G1).e = (the_Source_of G).e by Def32;
hence (the_Source_of G1).e = (the_Source_of G2).e by A2,A7,Def32;
end;
dom (the_Source_of G1) = the_Edges_of G1 & dom (the_Source_of G2) =
the_Edges_of G2 by FUNCT_2:def 1;
then the_Source_of G1 = the_Source_of G2 by A2,A6,FUNCT_1:2;
hence thesis by A1,A2,A5;
end;
theorem Th87:
G1 == G2 iff G1 is Subgraph of G2 & G2 is Subgraph of G1 by Th41;
theorem
for e,x,y being object holds
G1 == G2 implies (e Joins x,y,G1 implies e Joins x,y,G2) & (e
DJoins x,y,G1 implies e DJoins x,y,G2) & (e SJoins X,Y,G1 implies e SJoins X,Y,
G2) & (e DSJoins X,Y,G1 implies e DSJoins X,Y,G2);
theorem
G1 == G2 implies (G1 is _finite implies G2 is _finite) &
(G1 is loopless implies G2 is loopless) &
(G1 is _trivial implies G2 is _trivial) &
(G1 is non-multi implies G2 is non-multi) &
(G1 is non-Dmulti implies G2 is non-Dmulti) &
(G1 is simple implies G2 is simple) &
(G1 is Dsimple implies G2 is Dsimple)
proof
assume
A1: G1 == G2;
then
A2: the_Edges_of G1 = the_Edges_of G2;
the_Vertices_of G1 = the_Vertices_of G2 by A1;
hence G1 is _finite implies G2 is _finite by A2;
A3: the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of
G2 by A1;
A4: G1 is loopless implies G2 is loopless by A2,A3;
hence G1 is loopless implies G2 is loopless;
thus G1 is _trivial implies G2 is _trivial by A1;
A5: now
assume
A6: G1 is non-multi;
now
let e1,e2,v1,v2 be object;
assume e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2;
then e1 Joins v1,v2,G1 & e2 Joins v1,v2,G1 by A1;
hence e1 = e2 by A6;
end;
hence G2 is non-multi;
end;
hence G1 is non-multi implies G2 is non-multi;
A7: now
assume
A8: G1 is non-Dmulti;
now
let e1,e2,v1,v2 be object;
assume e1 DJoins v1,v2,G2 & e2 DJoins v1,v2,G2;
then e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1 by A1;
hence e1 = e2 by A8;
end;
hence G2 is non-Dmulti;
end;
hence G1 is non-Dmulti implies G2 is non-Dmulti;
thus G1 is simple implies G2 is simple by A4,A5;
thus thesis by A4,A7;
end;
theorem Th90:
G1 == G2 implies G1.order() = G2.order() & G1.size() = G2.size()
& G1.edgesInto(X) = G2.edgesInto(X) & G1.edgesOutOf(X) = G2.edgesOutOf(X) & G1
.edgesInOut(X) = G2.edgesInOut(X) & G1.edgesBetween(X) = G2.edgesBetween(X) &
G1.edgesDBetween(X,Y) = G2.edgesDBetween(X,Y)
proof
assume
A1: G1 == G2;
hence G1.order() = G2.order();
thus G1.size() = G2.size() by A1;
A2: the_Edges_of G1 = the_Edges_of G2 by A1;
A3: the_Target_of G1 = the_Target_of G2 by A1;
A4: now
let e be object;
e in G1.edgesInto(X) iff e in the_Edges_of G2 & (the_Target_of G2).e
in X by A2,A3,Def26;
hence e in G1.edgesInto(X) iff e in G2.edgesInto(X) by Def26;
end;
hence
A5: G1.edgesInto(X) = G2.edgesInto(X) by TARSKI:2;
A6: the_Source_of G1 = the_Source_of G2 by A1;
A7: now
let e be object;
e in G1.edgesOutOf(X) iff e in the_Edges_of G2 & (the_Source_of G2).e
in X by A2,A6,Def27;
hence e in G1.edgesOutOf(X) iff e in G2.edgesOutOf(X) by Def27;
end;
hence
A8: G1.edgesOutOf(X) = G2.edgesOutOf(X) by TARSKI:2;
thus G1.edgesInOut(X)= G2.edgesInOut(X) by A5,A7,TARSKI:2;
thus G1.edgesBetween(X)=G2.edgesBetween(X) by A4,A8,TARSKI:2;
now
let e be object;
e in G1.edgesDBetween(X,Y) iff e DSJoins X,Y,G1 by Def31;
then e in G1.edgesDBetween(X,Y) iff e DSJoins X,Y,G2 by A1;
hence e in G2.edgesDBetween(X,Y) iff e in G1.edgesDBetween(X,Y) by Def31;
end;
hence thesis by TARSKI:2;
end;
theorem Th91:
G1 == G2 & G3 is Subgraph of G1 implies G3 is Subgraph of G2
proof
assume that
A1: G1 == G2 and
A2: G3 is Subgraph of G1;
the_Vertices_of G3 c= the_Vertices_of G1 by A2,Def32;
hence the_Vertices_of G3 c= the_Vertices_of G2 by A1;
the_Edges_of G3 c= the_Edges_of G1 by A2,Def32;
hence the_Edges_of G3 c= the_Edges_of G2 by A1;
let e be set;
assume
A3: e in the_Edges_of G3;
hence (the_Source_of G3).e = (the_Source_of G1).e by A2,Def32
.= (the_Source_of G2).e by A1;
thus (the_Target_of G3).e = (the_Target_of G1).e by A2,A3,Def32
.= (the_Target_of G2).e by A1;
end;
theorem Th92:
G1 == G2 & G1 is Subgraph of G3 implies G2 is Subgraph of G3
proof
assume that
A1: G1 == G2 and
A2: G1 is Subgraph of G3;
A3: the_Edges_of G1 = the_Edges_of G2 by A1;
A4: the_Source_of G1 = the_Source_of G2 & the_Target_of G1 = the_Target_of
G2 by A1;
the_Vertices_of G1 = the_Vertices_of G2 by A1;
hence the_Vertices_of G2 c= the_Vertices_of G3 & the_Edges_of G2 c=
the_Edges_of G3 by A2,A3,Def32;
let e be set;
assume e in the_Edges_of G2;
hence thesis by A2,A3,A4,Def32;
end;
theorem Th93:
for G1,G2 being inducedSubgraph of G,V,E holds G1 == G2
proof
let G1,G2 be inducedSubgraph of G,V,E;
now
per cases;
suppose
A1: V is non empty Subset of the_Vertices_of G & E c= G.edgesBetween (V);
then
A2: the_Edges_of G1 = E & the_Edges_of G2 = E by Def37;
the_Vertices_of G1 = V & the_Vertices_of G2 = V by A1,Def37;
hence thesis by A2,Th86;
end;
suppose
not (V is non empty Subset of the_Vertices_of G & E c= G
.edgesBetween(V));
then G1 == G & G2 == G by Def37;
hence thesis;
end;
end;
hence thesis;
end;
theorem
for G1 being _Graph, G2 being inducedSubgraph of G1,the_Vertices_of G1
holds G1 == G2
proof
let G1 be _Graph, G2 be inducedSubgraph of G1, the_Vertices_of G1;
A1: the_Vertices_of G1 c= the_Vertices_of G1;
then the_Edges_of G2 = G1.edgesBetween(the_Vertices_of G1) by Def37;
then
A2: the_Edges_of G2 = the_Edges_of G1 by Th34;
then the_Source_of G2 = (the_Source_of G1)|the_Edges_of G1 by Th45;
then the_Source_of G2 = (the_Source_of G1)|(dom the_Source_of G1);
then
A3: the_Source_of G2 = the_Source_of G1;
the_Target_of G2 = (the_Target_of G1)|the_Edges_of G1 by A2,Th45;
then the_Target_of G2 = (the_Target_of G1)|(dom the_Target_of G1);
then
A4: the_Target_of G2 = the_Target_of G1;
the_Vertices_of G2 = the_Vertices_of G1 by A1,Def37;
hence thesis by A2,A3,A4;
end;
theorem Th95:
for G1,G2 being _Graph, V,E being set, G3 being inducedSubgraph of G1,
V,E st G1 == G2 holds G3 is inducedSubgraph of G2,V,E
proof
let G1,G2 be _Graph, V,E be set, G3 be inducedSubgraph of G1,V,E;
assume
A1: G1 == G2;
now
per cases;
suppose
A2: V is non empty Subset of the_Vertices_of G1 & E c= G1 .edgesBetween(V);
then
A3: the_Vertices_of G3 = V & the_Edges_of G3 = E by Def37;
A4: G3 is Subgraph of G2 by A1,Th91;
V is non empty Subset of the_Vertices_of G2 & E c= G2.edgesBetween(V
) by A1,A2,Th90;
hence thesis by A3,A4,Def37;
end;
suppose
A5: not (V is non empty Subset of the_Vertices_of G1 & E c= G1
.edgesBetween(V));
then
A6: not (V is non empty Subset of the_Vertices_of G2 & E c= G2
.edgesBetween(V)) by A1,Th90;
G3 == G1 by A5,Def37;
then
A7: G3 == G2 by A1;
then G3 is Subgraph of G2 by Th87;
hence thesis by A6,A7,Def37;
end;
end;
hence thesis;
end;
theorem Th96:
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 & G1
== G2 holds v1.edgesIn() = v2.edgesIn() & v1.edgesOut() = v2.edgesOut() & v1
.edgesInOut() = v2.edgesInOut() & v1.adj(e) = v2.adj(e) & v1.inDegree() = v2
.inDegree() & v1.outDegree() = v2.outDegree() & v1.degree() = v2.degree() & v1
.inNeighbors() = v2.inNeighbors() & v1.outNeighbors() = v2.outNeighbors() & v1
.allNeighbors() = v2.allNeighbors()
proof
let v1 be Vertex of G1, v2 be Vertex of G2;
assume that
A1: v1 = v2 and
A2: G1 == G2;
thus
A3: v1.edgesIn() = v2.edgesIn() by A1,A2,Th90;
thus
A4: v1.edgesOut() = v2.edgesOut() by A1,A2,Th90;
thus v1.edgesInOut() = v2.edgesInOut() by A1,A2,Th90;
now
per cases;
suppose
A5: e in the_Edges_of G1 & (the_Target_of G1).e = v1;
then
A6: e in the_Edges_of G2 & (the_Target_of G2).e = v2 by A1,A2;
thus v1.adj(e) = (the_Source_of G1).e by A5,Def41
.= (the_Source_of G2).e by A2
.= v2.adj(e) by A6,Def41;
end;
suppose
A7: e in the_Edges_of G1 & (the_Source_of G1).e = v1 & not (
the_Target_of G1).e = v1;
then
A8: not (the_Target_of G2).e = v2 by A1,A2;
A9: e in the_Edges_of G2 & (the_Source_of G2).e = v2 by A1,A2,A7;
thus v1.adj(e) = (the_Target_of G1).e by A7,Def41
.= (the_Target_of G2).e by A2
.= v2.adj(e) by A9,A8,Def41;
end;
suppose
A10: not (e in the_Edges_of G1 & (the_Target_of G1).e = v1) & not (e
in the_Edges_of G1 & (the_Source_of G1).e = v1 & not (the_Target_of G1).e = v1)
;
then
A11: ( not (e in the_Edges_of G2 & (the_Target_of G2).e = v2))& not (e
in the_Edges_of G2 & (the_Source_of G2).e = v2 & not ( the_Target_of G2).e = v2
) by A1,A2;
thus v1.adj(e) = v2 by A1,A10,Def41
.= v2.adj(e) by A11,Def41;
end;
end;
hence v1.adj(e) = v2.adj(e);
thus v1.inDegree() = v2.inDegree() by A1,A2,Th90;
thus v1.outDegree() = v2.outDegree() by A1,A2,Th90;
hence v1.degree() = v2.degree() by A1,A2,Th90;
thus v1.inNeighbors() = v2.inNeighbors() by A2,A3;
thus v1.outNeighbors() = v2.outNeighbors() by A2,A4;
hence thesis by A2,A3;
end;
theorem
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 & G1 == G2
holds (v1 is isolated implies v2 is isolated) & (v1 is endvertex implies v2 is
endvertex)
proof
let v1 be Vertex of G1, v2 be Vertex of G2;
assume
A1: v1 = v2 & G1 == G2;
hence v1 is isolated implies v2 is isolated by Th96;
assume v1 is endvertex;
then consider e being object such that
A2: v1.edgesInOut() = {e} & not e Joins v1,v1,G1;
v2.edgesInOut() = {e} & not e Joins v2,v2,G2 by A1,A2,Th96;
hence thesis;
end;
theorem Th98:
for G being _Graph, G1,G2 being Subgraph of G st G1 c< G2 holds
(the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2
)
proof
let G be _Graph, G1,G2 be Subgraph of G;
assume
A1: G1 c< G2;
then G1 c= G2;
then
A2: G1 is Subgraph of G2;
then
A3: the_Vertices_of G1 c= the_Vertices_of G2 by Def32;
A4: the_Edges_of G1 c= the_Edges_of G2 by A2,Def32;
A5: not G1 == G2 by A1;
now
per cases by A5,Th86;
suppose
the_Vertices_of G1 <> the_Vertices_of G2;
hence thesis by A3,XBOOLE_0:def 8;
end;
suppose
the_Edges_of G1 <> the_Edges_of G2;
hence thesis by A4,XBOOLE_0:def 8;
end;
end;
hence thesis;
end;
theorem
for G being _Graph, G1,G2 being Subgraph of G st G1 c< G2 holds (ex v
being object st v in the_Vertices_of G2 & not v in the_Vertices_of G1) or
ex e being object st e in the_Edges_of G2 & not e in the_Edges_of G1
proof
let G be _Graph, G1,G2 be Subgraph of G;
assume G1 c< G2;
then the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c<
the_Edges_of G2 by Th98;
hence thesis by XBOOLE_0:6;
end;
begin :: Addenda
:: from GLIB_006, 2024.10.20, S.K.
registration
let G be non-Dmulti _Graph;
cluster -> non-Dmulti for Subgraph of G;
coherence
proof
let G1 be Subgraph of G;
let e1,e2,v1,v2 be object;
reconsider w1=v1, w2=v2 as set by TARSKI:1;
assume e1 DJoins v1,v2,G1 & e2 DJoins v1,v2,G1;
then e1 DJoins w1,w2,G1 & e2 DJoins w1,w2,G1;
then e1 DJoins v1,v2,G & e2 DJoins v1,v2,G by Th72;
hence e1 = e2 by Def21;
end;
end;
theorem
for G being _Graph holds G is inducedSubgraph of G, the_Vertices_of G
proof
let G be _Graph;
set V = the_Vertices_of G;
set E = the_Edges_of G;
V is non empty & V c= V;
then A2: V is non empty Subset of the_Vertices_of G;
A3: G is Subgraph of G by Lm3;
E c= G.edgesBetween(V) by Th34;
then G is inducedSubgraph of G,V,E by A2, A3, Def37;
hence thesis by Th34;
end;
theorem Th101:
for G1,G3 being _Graph, V,E being set, G2 being inducedSubgraph of G1,V,E
st G2 == G3 holds G3 is inducedSubgraph of G1,V,E
proof
let G1,G3 be _Graph, V,E be set;
let G2 be inducedSubgraph of G1,V,E;
assume A1: G2 == G3;
then G3 is Subgraph of G2 by Th87;
then A2: G3 is Subgraph of G1 by Th43;
per cases;
suppose A3: V is non empty Subset of the_Vertices_of G1 &
E c= G1.edgesBetween(V);
then the_Vertices_of G2 = V & the_Edges_of G2 = E by Def37;
then the_Vertices_of G3 = V & the_Edges_of G3 = E by A1;
hence thesis by A2, A3, Def37;
end;
suppose A4: not (V is non empty Subset of the_Vertices_of G1 &
E c= G1.edgesBetween(V));
then G2 == G1 by Def37;
then G3 == G1 by A1;
hence thesis by A2, A4, Def37;
end;
end;
theorem Th102:
for G being _Graph, X being set, e,y being object st e SJoins X,{y},G
ex x being object st x in X & e Joins x,y,G
proof
let G be _Graph, X be set, e,y be object;
assume A1: e SJoins X,{y},G;
then A2: e in the_Edges_of G;
per cases by A1;
suppose A3: (the_Source_of G).e in X & (the_Target_of G).e in {y};
take (the_Source_of G).e;
(the_Target_of G).e = y by A3, TARSKI:def 1;
then e DJoins (the_Source_of G).e,y,G by A2;
hence thesis by A3;
end;
suppose A4: (the_Source_of G).e in {y} & (the_Target_of G).e in X;
take (the_Target_of G).e;
(the_Source_of G).e = y by A4, TARSKI:def 1;
then e DJoins y,(the_Target_of G).e,G by A2;
hence thesis by A4;
end;
end;
theorem
for G being _Graph, X being set st X /\ the_Vertices_of G = {}
holds G.edgesInto(X) = {} & G.edgesOutOf(X) = {} &
G.edgesInOut(X) = {} & G.edgesBetween(X) = {}
proof
let G be _Graph, X be set;
assume A1: X /\ the_Vertices_of G = {};
thus A2: G.edgesInto(X) = {}
proof
assume A3: G.edgesInto(X) <> {};
set e = the Element of G.edgesInto(X);
A4: e in the_Edges_of G & (the_Target_of G).e in X
by Def26,A3;
then e Joins (the_Source_of G).e,(the_Target_of G).e, G;
then (the_Target_of G).e in the_Vertices_of G by FUNCT_2:5;
hence contradiction by A1, A4, XBOOLE_0:def 4;
end;
thus A5: G.edgesOutOf(X) = {}
proof
assume A6: G.edgesOutOf(X) <> {};
set e = the Element of G.edgesOutOf(X);
A7: e in the_Edges_of G & (the_Source_of G).e in X
by A6, Def27;
then e Joins (the_Source_of G).e,(the_Target_of G).e, G;
then (the_Source_of G).e in the_Vertices_of G by FUNCT_2:5;
hence contradiction by A1, A7, XBOOLE_0:def 4;
end;
thus G.edgesInOut(X) = {} by A2, A5;
thus G.edgesBetween(X) = {} by A2;
end;
theorem
for G being _Graph, X1, X2 being set, y being object st X1 misses X2
holds G.edgesBetween(X1,{y}) misses G.edgesBetween(X2,{y})
proof
let G be _Graph, X1, X2 be set, y be object;
assume X1 misses X2;
then A1: X1 /\ X2 = {} by XBOOLE_0:def 7;
set E1 = G.edgesBetween(X1,{y}), E2 = G.edgesBetween(X2,{y});
assume not E1 misses E2;
then A2: E1 /\ E2 <> {} by XBOOLE_0:def 7;
set e = the Element of E1 /\ E2;
A3: e in E1 /\ E2 by A2;
then e in E1 by XBOOLE_0:def 4;
then e SJoins X1,{y},G by Def30;
then consider x1 being object such that
A4: x1 in X1 & e Joins x1,y,G by Th102;
e in E2 by A3, XBOOLE_0:def 4;
then e SJoins X2,{y},G by Def30;
then consider x2 being object such that
A5: x2 in X2 & e Joins x2,y,G by Th102;
thus contradiction by A1, A4, A5, XBOOLE_0:def 4;
end;
theorem
for G being _Graph, X1, X2 being set, y being object
holds G.edgesBetween(X1 \/ X2,{y})
= G.edgesBetween(X1,{y}) \/ G.edgesBetween(X2,{y})
proof
let G be _Graph, X1, X2 be set, y be object;
set E1 = G.edgesBetween(X1,{y}), E2 = G.edgesBetween(X2,{y});
X1 c= X1 \/ X2 & X2 c= X1 \/ X2 by XBOOLE_1:7;
then E1 c= G.edgesBetween(X1 \/ X2, {y}) &
E2 c= G.edgesBetween(X1 \/ X2, {y}) by Th37;
then A1: E1 \/ E2 c= G.edgesBetween(X1 \/ X2, {y}) by XBOOLE_1:8;
for e being object holds
e in G.edgesBetween(X1 \/ X2, {y}) implies e in E1 \/ E2
proof
let e be object;
assume e in G.edgesBetween(X1 \/ X2, {y});
then e SJoins X1 \/ X2,{y},G by Def30;
then consider x being object such that
A2: x in X1 \/ X2 & e Joins x,y,G by Th102;
A3: y in {y} by TARSKI:def 1;
per cases by A2, XBOOLE_0:def 3;
suppose x in X1;
then e SJoins X1,{y},G by A2, A3;
then e in E1 by Def30;
hence thesis by XBOOLE_0:def 3;
end;
suppose x in X2;
then e SJoins X2,{y},G by A2, A3;
then e in E2 by Def30;
hence thesis by XBOOLE_0:def 3;
end;
end;
then G.edgesBetween(X1 \/ X2, {y}) c= E1 \/ E2;
hence thesis by A1, XBOOLE_0:def 10;
end;
:: generalization of Th22, uses it for simplification of proof
theorem Th106:
for G being _trivial _Graph ex v being Vertex of G st the_Vertices_of G = {v}
& the_Source_of G = the_Edges_of G --> v
& the_Target_of G = the_Edges_of G --> v
proof
let G be _trivial _Graph;
consider v being Vertex of G such that
A1: the_Vertices_of G = {v} by Th22;
take v;
thus the_Vertices_of G = {v} by A1;
for e being object st e in dom the_Source_of G holds (the_Source_of G).e = v
proof
let e be object;
assume e in dom the_Source_of G;
then (the_Source_of G).e in the_Vertices_of G by PARTFUN1:4;
hence thesis by A1, TARSKI:def 1;
end;
hence the_Source_of G = (dom the_Source_of G) --> v by FUNCOP_1:11
.= the_Edges_of G --> v by Th4;
for e being object st e in dom the_Target_of G holds (the_Target_of G).e = v
proof
let e be object;
assume e in dom the_Target_of G;
then (the_Target_of G).e in the_Vertices_of G by PARTFUN1:4;
hence thesis by A1, TARSKI:def 1;
end;
hence the_Target_of G = (dom the_Target_of G) --> v by FUNCOP_1:11
.= the_Edges_of G --> v by Th4;
end;
:: from GLIB_008, 2024.10.23, S.K.
registration
let G be _Graph, v be Vertex of G;
cluster -> _trivial for inducedSubgraph of G, {v};
coherence
proof
G.edgesBetween({v}) c= G.edgesBetween({v});
hence thesis;
end;
end;
theorem Th107:
for G being _Graph, X being set, v being Vertex of G
holds G.edgesBetween(X \ {v}) = G.edgesBetween(X) \ v.edgesInOut()
proof
let G be _Graph, X be set, v be Vertex of G;
for e being object holds e in G.edgesBetween(X \ {v})
iff e in G.edgesBetween(X) \ v.edgesInOut()
proof
let e be object;
set u = (the_Source_of G).e, w = (the_Target_of G).e;
hereby
assume e in G.edgesBetween(X \ {v});
then A1: e in the_Edges_of G & u in X\{v} & w in X\{v} by Lm5;
then A2: e in G.edgesBetween(X) by Lm5;
not e in v.edgesInOut()
proof
assume e in v.edgesInOut();
then u = v or w = v by Th61;
hence contradiction by A1, ZFMISC_1:56;
end;
hence e in G.edgesBetween(X) \ v.edgesInOut() by A2, XBOOLE_0:def 5;
end;
assume e in G.edgesBetween(X) \ v.edgesInOut();
then A3: e in G.edgesBetween(X) & not e in v.edgesInOut()
by XBOOLE_0:def 5;
then A4: e in the_Edges_of G & u in X & w in X by Lm5;
u <> v & w <> v by A3, Th61;
then not u in {v} & not w in {v} by TARSKI:def 1;
then u in X\{v} & w in X\{v} by A4, XBOOLE_0:def 5;
hence thesis by A3, Lm5;
end;
hence thesis by TARSKI:2;
end;
theorem
for G being _Graph, X being set, v being Vertex of G st v is isolated
holds G.edgesBetween(X \ {v}) = G.edgesBetween(X)
proof
let G be _Graph, X be set, v be Vertex of G;
assume A1: v is isolated;
thus G.edgesBetween(X \ {v}) = G.edgesBetween(X) \ v.edgesInOut() by Th107
.= G.edgesBetween(X) by A1;
end;
theorem Th109:
for G being non-Dmulti _Graph, v being Vertex of G
holds v.inDegree() = card v.inNeighbors()
proof
let G be non-Dmulti _Graph, v be Vertex of G;
defpred P[object,object] means $2 DJoins $1,v,G;
A1: for x,y1,y2 being object st x in v.inNeighbors() & P[x,y1] & P[x,y2]
holds y1 = y2 by Def21;
A2: for x being object st x in v.inNeighbors() ex y being object st P[x,y]
by Th69;
consider f being Function such that
A3: dom f = v.inNeighbors() and
A4: for x being object st x in v.inNeighbors() holds P[x,f.x]
from FUNCT_1:sch 2(A1,A2);
for y being object holds y in rng f iff y in v.edgesIn()
proof
let y be object;
hereby
assume y in rng f;
then consider x being object such that
A5: x in dom f & f.x = y by FUNCT_1:def 3;
reconsider x as set by TARSKI:1;
thus y in v.edgesIn() by A3, A4, A5, Th57;
end;
assume y in v.edgesIn();
then consider x being set such that
A6: y DJoins x,v,G by Th57;
a7: x in v.inNeighbors() by A6, Th69;
then x in dom f & P[x,f.x] by A3, A4;
then y = f.x by A1, A3, A6;
hence thesis by a7, FUNCT_1:def 3, A3;
end;
then A8: rng f = v.edgesIn() by TARSKI:2;
for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1 = f.x2
holds x1 = x2
proof
let x1,x2 be object;
assume x1 in dom f & x2 in dom f & f.x1 = f.x2;
then P[x1,f.x1] & P[x2,f.x1] by A3, A4;
then (the_Source_of G).(f.x1) = x1 & (the_Source_of G).(f.x1) = x2
by Def14;
hence x1 = x2;
end;
then f is one-to-one by FUNCT_1:def 4;
then card v.inNeighbors() = card v.edgesIn()
by A3, A8, WELLORD2:def 4, CARD_1:5;
hence thesis;
end;
theorem Th110:
for G being non-Dmulti _Graph, v being Vertex of G
holds v.outDegree() = card v.outNeighbors()
proof
let G be non-Dmulti _Graph, v be Vertex of G;
defpred P[object,object] means $2 DJoins v,$1,G;
A1: for x,y1,y2 being object st x in v.outNeighbors() & P[x,y1] & P[x,y2]
holds y1 = y2 by Def21;
A2: for x being object st x in v.outNeighbors() ex y being object st P[x,y]
by Th70;
consider f being Function such that
A3: dom f = v.outNeighbors() and
A4: for x being object st x in v.outNeighbors() holds P[x,f.x]
from FUNCT_1:sch 2(A1,A2);
for y being object holds y in rng f iff y in v.edgesOut()
proof
let y be object;
hereby
assume y in rng f;
then consider x being object such that
A5: x in dom f & f.x = y by FUNCT_1:def 3;
reconsider x as set by TARSKI:1;
thus y in v.edgesOut() by A3, A4, A5, Th59;
end;
assume y in v.edgesOut();
then consider x being set such that
A6: y DJoins v,x,G by Th59;
a7: x in v.outNeighbors() by A6, Th70;
then x in dom f & P[x,f.x] by A3, A4;
then y = f.x by A1, A3, A6;
hence thesis by a7, A3, FUNCT_1:def 3;
end;
then A8: rng f = v.edgesOut() by TARSKI:2;
for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1 = f.x2
holds x1 = x2
proof
let x1,x2 be object;
assume x1 in dom f & x2 in dom f & f.x1 = f.x2;
then P[x1,f.x1] & P[x2,f.x1] by A3, A4;
then (the_Target_of G).(f.x1) = x1 & (the_Target_of G).(f.x1) = x2
by Def14;
hence x1 = x2;
end;
then f is one-to-one by FUNCT_1:def 4;
then card v.outNeighbors() = card v.edgesOut()
by A3, A8, WELLORD2:def 4, CARD_1:5;
hence thesis;
end;
theorem
for G being simple _Graph, v being Vertex of G
holds v.degree() = card v.allNeighbors()
proof
let G be simple _Graph, v be Vertex of G;
v.inNeighbors() /\ v.outNeighbors() = {}
proof
assume v.inNeighbors() /\ v.outNeighbors() <> {};
then consider w being object such that
A1: w in v.inNeighbors() /\ v.outNeighbors() by XBOOLE_0:def 1;
A2: w in v.inNeighbors() & w in v.outNeighbors() by A1, XBOOLE_0:def 4;
consider e1 being object such that
A3: e1 DJoins w,v,G by A2, Th69;
consider e2 being object such that
A4: e2 DJoins v,w,G by A2, Th70;
e1 Joins v,w,G & e2 Joins v,w,G by A3, A4;
then e1 = e2 by Def20;
then e1 in the_Edges_of G & (the_Source_of G).e1 = v &
(the_Target_of G).e1 = v by A3, A4;
hence contradiction by Def18;
end;
then card(v.inNeighbors() \/ v.outNeighbors())
= card v.inNeighbors() +` card v.outNeighbors()
by CARD_2:35,XBOOLE_0:def 7
.= v.inDegree() +` card v.outNeighbors() by Th109
.= v.degree() by Th110;
hence thesis;
end;
theorem
for G being _Graph holds G is loopless iff
for v being Vertex of G holds not v in v.allNeighbors()
proof
let G be _Graph;
hereby
assume A1: G is loopless;
let v be Vertex of G;
thus not v in v.allNeighbors()
proof
assume v in v.allNeighbors();
then consider e being object such that
A2: e Joins v,v,G by Th71;
thus contradiction by A1, A2;
end;
end;
assume A3: for v being Vertex of G holds not v in v.allNeighbors();
for v being object holds not ex e being object st e Joins v,v,G
proof
given v being object such that
A4: ex e being object st e Joins v,v,G;
reconsider v0 = v as Vertex of G by A4, FUNCT_2:5;
not v0 in v0.allNeighbors() by A3;
hence contradiction by A4, Th71;
end;
hence thesis by Th18;
end;
theorem
for G being _Graph, v being Vertex of G
holds v is isolated iff v.allNeighbors() = {}
proof
let G be _Graph, v be Vertex of G;
hereby
assume v is isolated;
then v.edgesInOut() = {};
then v.edgesIn() \/ v.edgesOut() = {};
then v.edgesIn() = {} & v.edgesOut() = {};
then (the_Source_of G).:v.edgesIn() = {} &
(the_Target_of G).:v.edgesOut() = {};
then v.inNeighbors() = {} & v.outNeighbors() = {};
then v.inNeighbors() \/ v.outNeighbors() = {} \/ {};
hence v.allNeighbors() = {};
end;
assume A1: v.allNeighbors() = {};
assume not v is isolated;
then A2: v.edgesInOut() <> {};
set e = the Element of v.edgesInOut();
consider v0 being Vertex of G such that
A3: e Joins v,v0,G by A2, Th64;
thus contradiction by A1, A3, Th71;
end;
Lm10:
for G1 being _Graph, v being set, G2 being removeVertex of G1, v
st not v in the_Vertices_of G1 holds G1 == G2
proof
let G1 be _Graph, v be set, G2 be removeVertex of G1, v;
set V = the_Vertices_of G1 \ {v};
assume not v in the_Vertices_of G1;
then A1: V = the_Vertices_of G1 by ZFMISC_1:57;
then the_Vertices_of G2 = V & the_Edges_of G2 = G1.edgesBetween(V)
by Def37;
then A2: the_Vertices_of G2 = the_Vertices_of G1 &
the_Edges_of G2 = the_Edges_of G1 by A1, Th34;
G1 is Subgraph of G1 by Lm3;
hence thesis by A2, Th86;
end;
theorem Th114:
for G1 being _Graph, v being set, G2 being removeVertex of G1, v
st G1 is _trivial or not v in the_Vertices_of G1 holds G1 == G2
proof
let G1 be _Graph, v be set, G2 be removeVertex of G1, v;
assume G1 is _trivial or not v in the_Vertices_of G1;
then per cases;
suppose G1 is _trivial;
then consider v1 being Vertex of G1 such that
A1: the_Vertices_of G1 = {v1} by Th22;
set V = the_Vertices_of G1 \ {v}, E = G1.edgesBetween(V);
per cases;
suppose V is non empty Subset of the_Vertices_of G1 &
E c= G1.edgesBetween(V);
then V = {v1} by A1, ZFMISC_1:33;
hence thesis by A1, Lm10, ZFMISC_1:57;
end;
suppose not (V is non empty Subset of the_Vertices_of G1 &
E c= G1.edgesBetween(V));
hence thesis by Def37;
end;
end;
suppose not v in the_Vertices_of G1;
hence thesis by Lm10;
end;
end;
Lm11:
for G1, G2 being _Graph, v being set
st G1 == G2 & not v in the_Vertices_of G1
holds G2 is removeVertex of G1, v
proof
let G1, G2 be _Graph, v be set;
assume A1: G1 == G2 & not v in the_Vertices_of G1;
then A2: G2 is Subgraph of G1 by Th87;
set V = the_Vertices_of G1 \ {v};
A3: V = the_Vertices_of G1 by A1, ZFMISC_1:57;
A4: G1.edgesBetween(V) = the_Edges_of G2 by A1, A3, Th34;
V = the_Vertices_of G2 by A1, A3;
hence thesis by A2, A4, Def37;
end;
theorem Th115:
for G1, G2 being _Graph, v being set
st G1 == G2 & (G1 is _trivial or not v in the_Vertices_of G1)
holds G2 is removeVertex of G1, v
proof
let G1, G2 be _Graph, v be set;
assume that
A1: G1 == G2 and
A2: G1 is _trivial or not v in the_Vertices_of G1;
A3: G2 is Subgraph of G1 by A1, Th87;
set V = the_Vertices_of G1 \ {v};
per cases by A2;
suppose G1 is _trivial;
then consider v1 being Vertex of G1 such that
A4: the_Vertices_of G1 = {v1} by Th22;
per cases;
suppose v = v1;
then V = {} by A4, XBOOLE_1:37;
hence thesis by A1, A3, Def37;
end;
suppose v <> v1;
then not v in the_Vertices_of G1 by A4, TARSKI:def 1;
hence thesis by A1, Lm11;
end;
end;
suppose not v in the_Vertices_of G1;
hence thesis by A1, Lm11;
end;
end;
:: converse of Th21
theorem Th116:
for G being _Graph holds (ex v1, v2 being Vertex of G st v1 <> v2)
implies G is non _trivial
proof
let G be _Graph;
given v1, v2 being Vertex of G such that
A1: v1 <> v2;
card the_Vertices_of G <> 1
proof
assume card the_Vertices_of G = 1;
then card {v1,v2} c= 1 by CARD_1:11;
then {0,1} c= 1 by A1, CARD_2:57, CARD_1:50;
then 1 in 1 by ZFMISC_1:32;
hence contradiction;
end;
hence thesis;
end;
registration
let G be non _trivial _Graph, X be set;
cluster -> non _trivial for removeEdges of G, X;
coherence
proof
let G2 be removeEdges of G, X;
ex v1, v2 being Vertex of G2 st v1 <> v2
proof
consider v1, v2 being Vertex of G such that
A1: v1 <> v2 by Th21;
reconsider v1, v2 as Vertex of G2 by Th53;
take v1, v2;
thus thesis by A1;
end;
hence thesis by Th116;
end;
end;
theorem
for G1 being _finite _Graph, G2 being Subgraph of G1
holds G2 is spanning iff G1.order() = G2.order() by CARD_2:102;
theorem Th118:
for G1 being _Graph, G2 being spanning Subgraph of G1
st the_Edges_of G1 = the_Edges_of G2 holds G1 == G2
proof
let G1 be _Graph, G2 be spanning Subgraph of G1;
assume A1: the_Edges_of G1 = the_Edges_of G2;
A2: G1 is Subgraph of G1 by Lm3;
the_Vertices_of G1 = the_Vertices_of G2 by Def33;
hence thesis by A1, A2, Th86;
end;
theorem
for G1 being _finite _Graph, G2 being spanning Subgraph of G1
st G1.size() = G2.size() holds G1 == G2
proof
let G1 be _finite _Graph, G2 be spanning Subgraph of G1;
assume A1: G1.size() = G2.size();
card the_Edges_of G1 = card the_Edges_of G2 by A1;
then the_Edges_of G1 = the_Edges_of G2 by CARD_2:102;
hence thesis by Th118;
end;
theorem
for G1 being _Graph, V being set, G2 being inducedSubgraph of G1, V
st G2 is spanning holds G1 == G2
proof
let G1 be _Graph, V be set, G2 be inducedSubgraph of G1, V;
assume G2 is spanning;
then A1: the_Vertices_of G1 = the_Vertices_of G2;
per cases;
suppose V is non empty Subset of the_Vertices_of G1;
then the_Vertices_of G2 = V & the_Edges_of G2 = G1.edgesBetween(V)
by Def37;
then A2: the_Edges_of G2 = the_Edges_of G1 by A1, Th34;
G1 is Subgraph of G1 by Lm3;
hence thesis by A1, A2, Th86;
end;
suppose not V is non empty Subset of the_Vertices_of G1;
hence thesis by Def37;
end;
end;
theorem
for G being _Graph holds G is non _trivial iff
ex H being Subgraph of G st H is non spanning
proof
let G be _Graph;
hereby
assume A1: G is non _trivial;
set v1 = the Vertex of G, v2 = the Vertex of G;
reconsider H = the removeVertex of G, v1 as Subgraph of G;
take H;
A2: the_Vertices_of H = the_Vertices_of G \ {v1} by A1, Th47;
v1 in {v1} by TARSKI:def 1;
then the_Vertices_of H <> the_Vertices_of G by A2, XBOOLE_0:def 5;
hence H is non spanning;
end;
given H being Subgraph of G such that
A3: H is non spanning;
A4: the_Vertices_of G <> the_Vertices_of H by A3;
the_Vertices_of H c= the_Vertices_of G;
then reconsider v1 = the Vertex of H as Vertex of G;
not the_Vertices_of G c= the_Vertices_of H by A4, XBOOLE_0:def 10;
then A5: the_Vertices_of G \ the_Vertices_of H <> {} by XBOOLE_1:37;
set v2 = the Element of the_Vertices_of G \ the_Vertices_of H;
reconsider v2 as Vertex of G by A5, TARSKI:def 3;
A6: v1 <> v2 by A5, XBOOLE_0:def 5;
card {v1, v2} c= card the_Vertices_of G by CARD_1:11;
then A7: 2 c= card the_Vertices_of G by A6, CARD_2:57;
assume G is _trivial;
then A8: 2 c= 1 by A7;
1 in {0,1} by TARSKI:def 2;
then 1 in 1 by A8, CARD_1:50;
hence contradiction;
end;
theorem
for G being _Graph
holds (ex v being Vertex of G st v is endvertex) implies G is non _trivial
proof
let G be _Graph;
given v being Vertex of G such that
A1: v is endvertex;
set G2 = the removeVertex of G, v;
consider e being object such that
A2: v.edgesInOut() = {e} & not e Joins v,v,G by A1;
set w = v.adj(e);
A3: e in v.edgesInOut() by A2, TARSKI:def 1;
for u being Vertex of G holds the_Vertices_of G <> {u}
proof
let u be Vertex of G;
assume the_Vertices_of G = {u};
then v = u & w = u by TARSKI:def 1;
hence contradiction by A2, A3, Th67;
end;
hence G is non _trivial by Th22;
end;
:: note that induced subgraphs generally commute
::theorem
:: for G1 being _Graph, V1, E1, V2, E2 being set
:: for G2 being inducedSubgraph of G1, V1, E1
:: for G3 being inducedSubgraph of G1, V2, E2
:: for G4 being inducedSubgraph of G2, V2, E2
:: holds G4 is inducedSubgraph of G3, V1, E1;
:: but the form above doesn't translate to removeEdge/Vertex exactly
Lm12:
for G1, G2 being _Graph, e being set
for G3 being removeEdge of G1, e, G4 being removeEdge of G2, e
st G1 == G2 holds G3 == G4
proof
let G1, G2 be _Graph, e be set;
let G3 be removeEdge of G1, e, G4 be removeEdge of G2, e;
assume G1 == G2;
then G4 is removeEdge of G1, e by Th95;
hence thesis by Th93;
end;
:: removeEdge and removeVertex commute, Part I
theorem
for G1 being _Graph, v,e being set, G2 being removeVertex of G1, v
for G3 being removeEdge of G1, e, G4 being removeEdge of G2, e
holds G4 is removeVertex of G3, v
proof
let G1 be _Graph, v,e be set, G2 be removeVertex of G1, v;
let G3 be removeEdge of G1, e, G4 be removeEdge of G2, e;
A1: the_Vertices_of G3 = the_Vertices_of G1 &
the_Edges_of G3 = the_Edges_of G1 \ {e} by Th51;
A2: the_Vertices_of G4 = the_Vertices_of G2 &
the_Edges_of G4 = the_Edges_of G2 \ {e} by Th51;
per cases;
suppose A3: G1 is non _trivial & v in the_Vertices_of G1;
then reconsider v1 = v as Vertex of G1;
:: basic relations
reconsider v3 = v1 as Vertex of G3 by A1;
A4: the_Vertices_of G2 = the_Vertices_of G1 \ {v} &
the_Edges_of G2 = G1.edgesBetween(the_Vertices_of G1 \ {v})
by A3, Th47;
then A5: the_Edges_of G2
= G1.edgesBetween(the_Vertices_of G1) \ v1.edgesInOut() by Th107
.= the_Edges_of G1 \ v1.edgesInOut() by Th34;
:: G4 is subgraph of G3
A6: the_Vertices_of G4 c= the_Vertices_of G3 by A1, A2;
A7: G4 is Subgraph of G1 by Th43;
for x being object holds x in the_Edges_of G4 implies x in the_Edges_of G3
proof
let x be object;
assume x in the_Edges_of G4;
then x in the_Edges_of G2 & not x in {e} by A2, XBOOLE_0:def 5;
hence thesis by A1, XBOOLE_0:def 5;
end;
then the_Edges_of G4 c= the_Edges_of G3;
then A8: G4 is Subgraph of G3 by A6, A7, Th44;
:: properties of removeVertex
now
thus the_Vertices_of G4 = the_Vertices_of G3 \ {v} by A1, A2, A4;
for x being object holds x in the_Edges_of G4 iff
x in G3.edgesBetween(the_Vertices_of G3 \ {v})
proof
let x be object;
A9: G3.edgesBetween(the_Vertices_of G3 \ {v})
= G3.edgesBetween(the_Vertices_of G3) \ v3.edgesInOut() by Th107
.= the_Edges_of G3 \ v3.edgesInOut() by Th34;
hereby
assume x in the_Edges_of G4;
then A10: x in the_Edges_of G2 & not x in {e} by A2, XBOOLE_0:def 5;
then x in the_Edges_of G1 & not x in v1.edgesInOut()
by A5, XBOOLE_0:def 5;
then A11: not x in v3.edgesInOut() by Th78, TARSKI:def 3;
x in the_Edges_of G3 by A1, A10, XBOOLE_0:def 5;
hence x in G3.edgesBetween(the_Vertices_of G3 \ {v})
by A9, A11, XBOOLE_0:def 5;
end;
assume x in G3.edgesBetween(the_Vertices_of G3 \ {v});
then A12: x in the_Edges_of G3 & not x in v3.edgesInOut()
by A9, XBOOLE_0:def 5;
then A13: x in the_Edges_of G1 & not x in {e} by A1, XBOOLE_0:def 5;
not x in v1.edgesInOut()
proof
assume x in v1.edgesInOut();
then x in v1.edgesInOut() /\ (the_Edges_of G3)
by A12, XBOOLE_0:def 4;
hence contradiction by A12, Th79;
end;
then x in the_Edges_of G2 by A5, A13, XBOOLE_0:def 5;
hence thesis by A2, A13, XBOOLE_0:def 5;
end;
hence the_Edges_of G4 = G3.edgesBetween(the_Vertices_of G3 \ {v})
by TARSKI:2;
end;
hence thesis by A8, Def37;
end;
suppose A14: G1 is _trivial or not v in the_Vertices_of G1;
then G1 == G2 by Th114;
then A15: G3 == G4 by Lm12;
G3 is _trivial or not v in the_Vertices_of G3 by A14;
hence thesis by A15, Th115;
end;
end;
Lm13:
for G1,G3,G4 being _Graph, e being set, G2 being removeEdge of G1, e
st G1 == G3 & G2 == G4 holds G4 is removeEdge of G3, e
proof
let G1,G3,G4 be _Graph, e be set;
let G2 be removeEdge of G1, e;
assume A1: G1 == G3 & G2 == G4;
then G2 is removeEdge of G3, e by Th95;
hence thesis by A1, Th101;
end;
:: removeEdge and removeVertex commute, Part II
theorem
for G1 being _Graph, v,e being set
for G2 being removeEdge of G1, e
for G3 being removeVertex of G1, v, G4 being removeVertex of G2, v
holds G4 is removeEdge of G3, e
proof
let G1 be _Graph, v,e be set;
let G2 be removeEdge of G1, e;
let G3 be removeVertex of G1, v, G4 be removeVertex of G2, v;
A1: the_Vertices_of G2 = the_Vertices_of G1 &
the_Edges_of G2 = the_Edges_of G1 \ {e} by Th51;
per cases;
suppose A2: G1 is non _trivial & v in the_Vertices_of G1;
then reconsider v1 = v as Vertex of G1;
reconsider v2 = v1 as Vertex of G2 by A1;
:: basic relations
the_Vertices_of G3 = the_Vertices_of G1 \ {v} &
the_Edges_of G3 = G1.edgesBetween(the_Vertices_of G1 \ {v})
by A2, Th47;
then A3: the_Edges_of G3
= G1.edgesBetween(the_Vertices_of G1) \ v1.edgesInOut() by Th107
.= the_Edges_of G1 \ v1.edgesInOut() by Th34;
the_Vertices_of G4 = the_Vertices_of G2 \ {v} &
the_Edges_of G4 = G2.edgesBetween(the_Vertices_of G2 \ {v})
by A1, A2, Th47;
then A4: the_Edges_of G4
= G2.edgesBetween(the_Vertices_of G2) \ v2.edgesInOut() by Th107
.= the_Edges_of G2 \ v2.edgesInOut() by Th34;
:: G4 is subgraph of G3
A5: the_Vertices_of G4 = the_Vertices_of G1 \ {v} by A1, A2, Th47
.= the_Vertices_of G3 by A2, Th47;
for x being object holds x in the_Edges_of G4
implies x in the_Edges_of G3 \ {e}
proof
let x be object;
assume x in the_Edges_of G4;
then A6: x in the_Edges_of G2 & not x in v2.edgesInOut()
by A4, XBOOLE_0:def 5;
then A7: x in the_Edges_of G1 & not x in {e} by A1, XBOOLE_0:def 5;
not x in v1.edgesInOut()
proof
assume x in v1.edgesInOut();
then per cases by Th61;
suppose (the_Source_of G1).x = v1;
then (the_Source_of G2).x = v1 by A6, Def32;
hence contradiction by A6, Th61;
end;
suppose (the_Target_of G1).x = v1;
then (the_Target_of G2).x = v1 by A6, Def32;
hence contradiction by A6, Th61;
end;
end;
then x in the_Edges_of G3 by A3, A6, XBOOLE_0:def 5;
hence thesis by A7, XBOOLE_0:def 5;
end;
then A8: the_Edges_of G4 c= the_Edges_of G3 \ {e};
the_Edges_of G3 \ {e} c= the_Edges_of G3 by XBOOLE_1:36;
then A9: the_Edges_of G4 c= the_Edges_of G3 by A8;
G4 is Subgraph of G1 by Th43;
then A10: G4 is Subgraph of G3 by A5, A9, Th44;
:: property assumptions for induced subgraph
A11: now
the_Vertices_of G3 c= the_Vertices_of G3;
hence the_Vertices_of G3 is non empty Subset of the_Vertices_of G3;
the_Edges_of G3 \ {e} c= the_Edges_of G3 by XBOOLE_1:36;
hence the_Edges_of G3 \ {e} c= G3.edgesBetween(the_Vertices_of G3)
by Th34;
end;
:: properties of removeEdge
now
thus the_Vertices_of G4 = the_Vertices_of G3 by A5;
for x being object holds x in the_Edges_of G3 \ {e}
implies x in the_Edges_of G4
proof
let x be object;
assume x in the_Edges_of G3 \ {e};
then A12: x in the_Edges_of G3 & not x in {e} by XBOOLE_0:def 5;
then A13: x in the_Edges_of G1 & not x in v1.edgesInOut()
by A3, XBOOLE_0:def 5;
A14: x in the_Edges_of G2 by A1, A12, XBOOLE_0:def 5;
not x in v2.edgesInOut() by A13, Th78, TARSKI:def 3;
hence thesis by A4, A14, XBOOLE_0:def 5;
end;
then the_Edges_of G3 \ {e} c= the_Edges_of G4;
hence the_Edges_of G4 = the_Edges_of G3 \ {e} by A8, XBOOLE_0:def 10;
end;
hence thesis by A10, A11, Def37;
end;
suppose A15: G1 is _trivial or not v in the_Vertices_of G1;
then A16: G1 == G3 by Th114;
G2 is _trivial or not v in the_Vertices_of G2
proof
per cases by A15;
suppose G1 is _trivial;
hence thesis;
end;
suppose not v in the_Vertices_of G1;
hence thesis;
end;
end;
then G2 == G4 by Th114;
hence thesis by A16, Lm13;
end;
end;
:: from GLIB_009, 2024.10.23, S.K.
theorem
for G being _Graph, e,x1,y1,x2,y2 being object
holds e DJoins x1,y1,G & e DJoins x2,y2,G implies x1 = x2 & y1 = y2;
registration
let G be _trivial _Graph;
cluster the_Vertices_of G -> trivial;
coherence
proof
ex v being Vertex of G st the_Vertices_of G = {v} by Th22;
hence thesis;
end;
end;
registration
cluster _trivial non-Dmulti -> non-multi for _Graph;
coherence
proof
let G be _Graph;
assume A1: G is _trivial non-Dmulti;
then consider v being Vertex of G such that
A2: the_Vertices_of G = {v} by Th22;
for e1,e2,v1,v2 being object holds
e1 Joins v1,v2,G & e2 Joins v1,v2,G implies e1 = e2
proof
let e1,e2,v1,v2 be object;
assume A3: e1 Joins v1,v2,G & e2 Joins v1,v2,G;
then v1 in the_Vertices_of G & v2 in the_Vertices_of G by FUNCT_2:5;
then v1 = v & v2 = v by A2, TARSKI:def 1;
then e1 DJoins v,v,G & e2 DJoins v,v,G by A3;
hence e1 = e2 by A1;
end;
hence thesis;
end;
let G be _trivial non-Dmulti _Graph;
cluster the_Edges_of G -> trivial;
coherence
proof
consider v being Vertex of G such that
the_Vertices_of G = {v} and
A4: the_Source_of G = the_Edges_of G --> v and
A5: the_Target_of G = the_Edges_of G --> v by Th106;
now
let e1, e2 be object;
assume A6: e1 in the_Edges_of G & e2 in the_Edges_of G;
then (the_Source_of G).e1 = v & (the_Target_of G).e1 = v &
(the_Source_of G).e2 = v & (the_Target_of G).e2 = v
by A4, A5, FUNCOP_1:7;
then e1 DJoins v,v,G & e2 DJoins v,v,G by A6;
hence e1 = e2 by Def21;
end;
hence thesis by ZFMISC_1:def 10;
end;
end;
theorem
for G being _Graph, X,Y being set, e,x,y being object
holds e DJoins x,y,G & x in X & y in Y implies e DSJoins X,Y,G;
theorem
for G being _trivial _Graph, H being _Graph
st the_Vertices_of H c= the_Vertices_of G & the_Edges_of H c= the_Edges_of G
holds H is _trivial & H is Subgraph of G
proof
let G be _trivial _Graph, H be _Graph;
assume A1: the_Vertices_of H c= the_Vertices_of G &
the_Edges_of H c= the_Edges_of G;
consider v being Vertex of G such that
A2: the_Vertices_of G = {v} by Th22;
A3: the_Vertices_of H = {v} by A1, A2, ZFMISC_1:33;
then card the_Vertices_of H = 1 by CARD_1:30;
hence H is _trivial;
now
let e be set;
assume A4: e in the_Edges_of H;
then (the_Source_of H).e in the_Vertices_of H &
(the_Target_of H).e in the_Vertices_of H by FUNCT_2:5;
then A5: (the_Source_of H).e = v & (the_Target_of H).e = v
by A3, TARSKI:def 1;
(the_Source_of G).e in the_Vertices_of G &
(the_Target_of G).e in the_Vertices_of G by A1, A4, FUNCT_2:5;
hence (the_Source_of H).e = (the_Source_of G).e &
(the_Target_of H).e = (the_Target_of G).e by A2, A5, TARSKI:def 1;
end;
hence thesis by A1, Def32;
end;
theorem
for G being _Graph holds G == G | _GraphSelectors
proof
let G be _Graph;
A1: VertexSelector in _GraphSelectors &
EdgeSelector in _GraphSelectors &
SourceSelector in _GraphSelectors &
TargetSelector in _GraphSelectors by ENUMSET1:def 2;
A2: the_Vertices_of G = the_Vertices_of (G | _GraphSelectors)
by A1, FUNCT_1:49;
A3: the_Edges_of G = the_Edges_of (G | _GraphSelectors) by A1, FUNCT_1:49;
A4: the_Source_of G = the_Source_of (G | _GraphSelectors) by A1, FUNCT_1:49;
the_Target_of G = the_Target_of (G | _GraphSelectors) by A1, FUNCT_1:49;
hence thesis by A2, A3, A4;
end;
theorem
for G being _Graph, X,Y being set, e being object
holds e SJoins X,Y,G iff e SJoins Y,X,G;
theorem
for G being _Graph, X,Y being set, e being object
holds e SJoins X,Y,G iff (e DSJoins X,Y,G or e DSJoins Y,X,G);
theorem Th131:
for G being _Graph, e,v,w being object
st e SJoins {v},{w},G holds e Joins v,w,G by TARSKI:def 1;
theorem Th132:
for G being _Graph, e,v,w being object
st e DSJoins {v},{w},G holds e DJoins v,w,G by TARSKI:def 1;
theorem
for G being _Graph, v,w being object st v <> w
holds G.edgesDBetween({v},{w}) misses G.edgesDBetween({w},{v}) &
G.edgesBetween({v},{w})
= G.edgesDBetween({v},{w}) \/ G.edgesDBetween({w},{v})
proof
let G be _Graph, v,w be object;
assume A1: v <> w;
G.edgesDBetween({v},{w}) /\ G.edgesDBetween({w},{v}) = {}
proof
assume G.edgesDBetween({v},{w}) /\ G.edgesDBetween({w},{v}) <> {};
then consider e being object such that
A2: e in G.edgesDBetween({v},{w}) /\ G.edgesDBetween({w},{v})
by XBOOLE_0:def 1;
e in G.edgesDBetween({v},{w}) & e in G.edgesDBetween({w},{v})
by A2, XBOOLE_0:def 4;
then e DSJoins {v},{w},G & e DSJoins {w},{v},G by Def31;
then (the_Source_of G).e in {v} & (the_Source_of G).e in {w};
then (the_Source_of G).e = v & (the_Source_of G).e = w by TARSKI:def 1;
hence contradiction by A1;
end;
hence G.edgesDBetween({v},{w}) misses G.edgesDBetween({w},{v})
by XBOOLE_0:def 7;
for e being object holds e in G.edgesBetween({v},{w}) iff
e in G.edgesDBetween({v},{w}) or e in G.edgesDBetween({w},{v})
proof
let e be object;
hereby
assume e in G.edgesBetween({v},{w});
then e SJoins {v},{w},G by Def30;
then e DSJoins {v},{w},G or e DSJoins {w},{v},G;
hence e in G.edgesDBetween({v},{w}) or e in G.edgesDBetween({w},{v})
by Def31;
end;
assume e in G.edgesDBetween({v},{w}) or e in G.edgesDBetween({w},{v});
then e DSJoins {v},{w},G or e DSJoins {w},{v},G by Def31;
then e SJoins {v},{w},G;
hence e in G.edgesBetween({v},{w}) by Def30;
end;
hence thesis by XBOOLE_0:def 3;
end;
theorem
for G being _Graph, X being set
holds G.edgesBetween(X,X) = G.edgesDBetween(X,X)
proof
let G be _Graph, X be set;
now
let e be object;
e in G.edgesBetween(X,X) iff e SJoins X,X,G by Def30;
then e in G.edgesBetween(X,X) iff e DSJoins X,X,G;
hence e in G.edgesBetween(X,X) iff e in G.edgesDBetween(X,X)
by Def31;
end;
hence thesis by TARSKI:2;
end;
theorem
for G being _Graph, X,Y being set
holds G.edgesBetween(X,Y) = G.edgesBetween(Y,X)
proof
let G be _Graph, X,Y be set;
now
let e be object;
e in G.edgesBetween(X,Y) iff e SJoins X,Y,G by Def30;
then e in G.edgesBetween(X,Y) iff e SJoins Y,X,G;
hence e in G.edgesBetween(X,Y) iff e in G.edgesBetween(Y,X)
by Def30;
end;
hence thesis by TARSKI:2;
end;
theorem Th136:
for G being _Graph holds G is loopless iff
for v being object holds not ex e being object st e DJoins v,v,G
proof
let G be _Graph;
thus G is loopless implies
for v being object holds not ex e being object st e DJoins v,v,G;
assume A3: for v being object holds not ex e being object st e DJoins v,v,G;
for v being object holds not ex e being object st e Joins v,v,G
proof
let v be object;
given e being object such that
A4: e Joins v,v,G;
e DJoins v,v,G by A4;
hence contradiction by A3;
end;
hence thesis by Th18;
end;
theorem Th137:
for G being _Graph holds G is loopless iff
for v being object holds not ex e being object st e SJoins {v},{v},G
proof
let G be _Graph;
thus G is loopless implies for v being object holds
not ex e being object st e SJoins {v},{v},G by Th131, Th18;
assume A1: for v being object
holds not ex e being object st e SJoins {v},{v},G;
for v being object holds not ex e being object st e Joins v,v,G
proof
let v be object;
given e being object such that
A2: e Joins v,v,G;
v in {v} by TARSKI:def 1;
then e SJoins {v},{v},G by A2;
hence contradiction by A1;
end;
hence thesis by Th18;
end;
theorem Th138:
for G being _Graph holds G is loopless iff
for v being object holds not ex e being object st e DSJoins {v},{v},G
proof
let G be _Graph;
hereby
assume A1: G is loopless;
let v be object;
given e being object such that
A2: e DSJoins {v},{v},G;
e SJoins {v},{v},G by A2;
hence contradiction by A1, Th137;
end;
assume A3: for v being object holds
not ex e being object st e DSJoins {v},{v},G;
for v being object holds not ex e being object st e SJoins {v},{v},G
proof
let v be object;
given e being object such that
A4: e SJoins {v},{v},G;
e DSJoins {v},{v},G by A4;
hence contradiction by A3;
end;
hence thesis by Th137;
end;
theorem Th139:
for G being _Graph holds G is loopless iff
for v being object holds G.edgesBetween({v},{v}) = {}
proof
let G be _Graph;
hereby
assume A1: G is loopless;
let v be object;
not ex e being object st e in G.edgesBetween({v},{v})
proof
given e being object such that
A2: e in G.edgesBetween({v},{v});
e SJoins {v},{v},G by A2, Def30;
hence contradiction by A1, Th137;
end;
hence G.edgesBetween({v},{v}) = {} by XBOOLE_0:def 1;
end;
assume A3: for v being object holds G.edgesBetween({v},{v}) = {};
for v being object holds not ex e being object st e SJoins {v},{v},G
proof
let v be object;
given e being object such that
A4: e SJoins {v},{v},G;
e in G.edgesBetween({v},{v}) by A4, Def30;
hence contradiction by A3;
end;
hence thesis by Th137;
end;
theorem Th140:
for G being _Graph holds G is loopless iff
for v being object holds G.edgesDBetween({v},{v}) = {}
proof
let G be _Graph;
hereby
assume A1: G is loopless;
let v be object;
not ex e being object st e in G.edgesDBetween({v},{v})
proof
given e being object such that
A2: e in G.edgesDBetween({v},{v});
e DSJoins {v},{v},G by A2, Def31;
hence contradiction by A1, Th138;
end;
hence G.edgesDBetween({v},{v}) = {} by XBOOLE_0:def 1;
end;
assume A3: for v being object holds G.edgesDBetween({v},{v}) = {};
for v being object holds not ex e being object st e DSJoins {v},{v},G
proof
let v be object;
given e being object such that
A4: e DSJoins {v},{v},G;
e in G.edgesDBetween({v},{v}) by A4, Def31;
hence contradiction by A3;
end;
hence thesis by Th138;
end;
registration
let G be loopless _Graph, v be object;
cluster G.edgesBetween({v},{v}) -> empty;
coherence by Th139;
cluster G.edgesDBetween({v},{v}) -> empty;
coherence by Th140;
end;
theorem Th141:
for G being _Graph holds G is non-multi iff
for v,w being object holds G.edgesBetween({v},{w}) is trivial
proof
let G be _Graph;
hereby
assume A1: G is non-multi;
let v,w be object;
for e1,e2 being object st e1 in G.edgesBetween({v},{w}) &
e2 in G.edgesBetween({v},{w}) holds e1 = e2
proof
let e1,e2 be object;
assume e1 in G.edgesBetween({v},{w});
then e1 SJoins {v},{w},G by Def30;
then A2: e1 Joins v,w,G by Th131;
assume e2 in G.edgesBetween({v},{w});
then e2 SJoins {v},{w},G by Def30;
then e2 Joins v,w,G by Th131;
hence e1 = e2 by A1, A2;
end;
hence G.edgesBetween({v},{w}) is trivial by ZFMISC_1:def 10;
end;
assume A3: for v,w being object holds G.edgesBetween({v},{w}) is trivial;
now
let e1,e2,v,w be object;
assume A4: e1 Joins v,w,G & e2 Joins v,w,G;
v in {v} & w in {w} by TARSKI:def 1;
then e1 SJoins {v},{w},G & e2 SJoins {v},{w},G by A4;
then A5: e1 in G.edgesBetween({v},{w}) & e2 in G.edgesBetween({v},{w})
by Def30;
G.edgesBetween({v},{w}) is trivial by A3;
hence e1 = e2 by A5, ZFMISC_1:def 10;
end;
hence thesis;
end;
registration
let G be non-multi _Graph, v, w be object;
cluster G.edgesBetween({v},{w}) -> trivial;
coherence by Th141;
end;
theorem Th142:
for G being _Graph holds G is non-Dmulti iff
for v,w being object holds G.edgesDBetween({v},{w}) is trivial
proof
let G be _Graph;
hereby
assume A1: G is non-Dmulti;
let v,w be object;
for e1,e2 being object st e1 in G.edgesDBetween({v},{w}) &
e2 in G.edgesDBetween({v},{w}) holds e1 = e2
proof
let e1,e2 be object;
assume e1 in G.edgesDBetween({v},{w});
then e1 DSJoins {v},{w},G by Def31;
then A2: e1 DJoins v,w,G by Th132;
assume e2 in G.edgesDBetween({v},{w});
then e2 DSJoins {v},{w},G by Def31;
then e2 DJoins v,w,G by Th132;
hence e1 = e2 by A1, A2;
end;
hence G.edgesDBetween({v},{w}) is trivial by ZFMISC_1:def 10;
end;
assume A3: for v,w being object holds G.edgesDBetween({v},{w}) is trivial;
now
let e1,e2,v,w be object;
assume A4: e1 DJoins v,w,G & e2 DJoins v,w,G;
v in {v} & w in {w} by TARSKI:def 1;
then e1 DSJoins {v},{w},G & e2 DSJoins {v},{w},G by A4;
then A5: e1 in G.edgesDBetween({v},{w}) & e2 in G.edgesDBetween({v},{w})
by Def31;
G.edgesDBetween({v},{w}) is trivial by A3;
hence e1 = e2 by A5, ZFMISC_1:def 10;
end;
hence thesis;
end;
registration
let G be non-Dmulti _Graph, v, w be object;
cluster G.edgesDBetween({v},{w}) -> trivial;
coherence by Th142;
end;
registration
let G be non _trivial _Graph;
cluster spanning -> non _trivial for Subgraph of G;
coherence by Def19;
end;
registration
let G be _Graph;
cluster isolated -> non endvertex for Vertex of G;
coherence;
end;
:: from GLIBPRE0, 2024.10.23, S.K.
theorem Th143:
for G being _Graph, v being Vertex of G, e,w being object
st v is isolated holds not e Joins v,w,G by Th62;
theorem Th144:
for G being _Graph, v being Vertex of G, e,w being object
st v is isolated holds not e DJoins v,w,G & not e DJoins w,v,G
proof
let G be _Graph, v be Vertex of G, e,w be object;
assume A1: v is isolated;
assume e DJoins v,w,G or e DJoins w,v,G;
then per cases;
suppose e DJoins v,w,G;
then e Joins v,w,G;
hence contradiction by A1, Th143;
end;
suppose e DJoins w,v,G;
then e Joins v,w,G;
hence contradiction by A1, Th143;
end;
end;
theorem
for G being _Graph, v being Vertex of G
holds v is isolated iff not v in rng the_Source_of G \/ rng the_Target_of G
proof
let G be _Graph, v be Vertex of G;
hereby
assume A1: v is isolated;
assume v in rng the_Source_of G \/ rng the_Target_of G;
then per cases by XBOOLE_0:def 3;
suppose v in rng the_Source_of G;
then consider e being object such that
A2: e in dom the_Source_of G & (the_Source_of G).e=v by FUNCT_1:def 3;
e DJoins v,(the_Target_of G).e,G by A2;
hence contradiction by A1, Th144;
end;
suppose v in rng the_Target_of G;
then consider e being object such that
A3: e in dom the_Target_of G & (the_Target_of G).e=v by FUNCT_1:def 3;
e DJoins (the_Source_of G).e,v,G by A3;
hence contradiction by A1, Th144;
end;
end;
assume A4: not v in rng the_Source_of G \/ rng the_Target_of G;
assume v is non isolated;
then v.edgesInOut() <> {};
then consider e being object such that
A5: e in v.edgesInOut() by XBOOLE_0:def 1;
A6: e in the_Edges_of G &
((the_Source_of G).e = v or (the_Target_of G).e = v) by A5, Th61;
then per cases;
suppose A7: (the_Source_of G).e = v;
e in dom the_Source_of G by A6, FUNCT_2:def 1;
then v in rng the_Source_of G by A7, FUNCT_1:3;
hence contradiction by A4, XBOOLE_0:def 3;
end;
suppose A8: (the_Target_of G).e = v;
e in dom the_Target_of G by A6, FUNCT_2:def 1;
then v in rng the_Target_of G by A8, FUNCT_1:3;
hence contradiction by A4, XBOOLE_0:def 3;
end;
end;
theorem
for G being _Graph, v being Vertex of G, e being object
st v is endvertex holds not e Joins v,v,G
proof
let G be _Graph, v be Vertex of G, e be object;
assume v is endvertex;
then consider e0 being object such that
A1: v.edgesInOut() = {e0} & not e0 Joins v,v,G;
assume A2: e Joins v,v,G;
then e in v.edgesInOut() by Th62;
hence contradiction by A1, A2, TARSKI:def 1;
end;
theorem
for G being _Graph, v being Vertex of G holds
v.edgesIn() = (the_Target_of G)"{v} & v.edgesOut() = (the_Source_of G)"{v}
proof
let G be _Graph, v be Vertex of G;
now
let e be object;
hereby
assume e in v.edgesIn();
then A1: e in the_Edges_of G & (the_Target_of G).e = v by Lm7;
then A2: e in dom the_Target_of G by FUNCT_2:def 1;
(the_Target_of G).e in {v} by A1, TARSKI:def 1;
hence e in (the_Target_of G)"{v} by A2, FUNCT_1:def 7;
end;
assume e in (the_Target_of G)"{v};
then A3: e in dom the_Target_of G & (the_Target_of G).e in {v}
by FUNCT_1:def 7;
then (the_Target_of G).e = v by TARSKI:def 1;
hence e in v.edgesIn() by A3, Lm7;
end;
hence v.edgesIn() = (the_Target_of G)"{v} by TARSKI:2;
now
let e be object;
hereby
assume e in v.edgesOut();
then A4: e in the_Edges_of G & (the_Source_of G).e = v by Lm8;
then A5: e in dom the_Source_of G by FUNCT_2:def 1;
(the_Source_of G).e in {v} by A4, TARSKI:def 1;
hence e in (the_Source_of G)"{v} by A5, FUNCT_1:def 7;
end;
assume e in (the_Source_of G)"{v};
then A6: e in dom the_Source_of G & (the_Source_of G).e in {v}
by FUNCT_1:def 7;
then (the_Source_of G).e = v by TARSKI:def 1;
hence e in v.edgesOut() by A6, Lm8;
end;
hence v.edgesOut() = (the_Source_of G)"{v} by TARSKI:2;
end;
theorem Th148:
for G being _trivial _Graph, v being Vertex of G holds
v.edgesIn() = the_Edges_of G & v.edgesOut() = the_Edges_of G &
v.edgesInOut() = the_Edges_of G
proof
let G be _trivial _Graph, v be Vertex of G;
consider v0 being Vertex of G such that
A1: the_Vertices_of G = {v0} by Th22;
A2: v = v0 by A1, TARSKI:def 1;
A3: now
let e be object;
assume A4: e in the_Edges_of G;
then e Joins (the_Source_of G).e,(the_Target_of G).e,G;
then (the_Source_of G).e in the_Vertices_of G &
(the_Target_of G).e in the_Vertices_of G by FUNCT_2:5;
then (the_Source_of G).e = v0 & (the_Target_of G).e = v0
by A1, TARSKI:def 1;
hence e DJoins v,v,G by A2, A4;
end;
for e being object st e in the_Edges_of G holds e in v.edgesIn()
by A3, Th57;
then the_Edges_of G c= v.edgesIn();
hence A5: v.edgesIn() = the_Edges_of G by XBOOLE_0:def 10;
for e being object st e in the_Edges_of G holds e in v.edgesOut()
by A3, Th59;
then the_Edges_of G c= v.edgesOut();
hence v.edgesOut() = the_Edges_of G by XBOOLE_0:def 10;
hence v.edgesInOut() = the_Edges_of G by A5;
end;
theorem
for G being _trivial _Graph, v being Vertex of G holds
v.inDegree() = G.size() & v.outDegree() = G.size() &
v.degree() = G.size() +` G.size()
proof
let G be _trivial _Graph, v be Vertex of G;
thus v.inDegree() = G.size() & v.outDegree() = G.size() by Th148;
hence v.degree() = G.size() +` G.size();
end;
theorem Th150:
for G being _Graph, X, Y being set
holds G.edgesBetween(X,Y) = G.edgesDBetween(X,Y) \/ G.edgesDBetween(Y,X)
proof
let G be _Graph, X, Y be set;
now
let e be object;
hereby
assume e in G.edgesDBetween(X,Y) \/ G.edgesDBetween(Y,X);
then per cases by XBOOLE_0:def 3;
suppose e in G.edgesDBetween(X,Y);
then e DSJoins X,Y,G by Def31;
hence e SJoins X,Y,G;
end;
suppose e in G.edgesDBetween(Y,X);
then e DSJoins Y,X,G by Def31;
hence e SJoins X,Y,G;
end;
end;
assume e SJoins X,Y,G;
then per cases;
suppose e DSJoins X,Y,G;
then e in G.edgesDBetween(X,Y) by Def31;
hence e in G.edgesDBetween(X,Y)\/G.edgesDBetween(Y,X) by XBOOLE_0:def 3;
end;
suppose e DSJoins Y,X,G;
then e in G.edgesDBetween(Y,X) by Def31;
hence e in G.edgesDBetween(X,Y)\/G.edgesDBetween(Y,X) by XBOOLE_0:def 3;
end;
end;
hence thesis by Def30;
end;
theorem
for G being _Graph, v being Vertex of G
holds v.edgesInOut() = G.edgesBetween(the_Vertices_of G,{v})
proof
let G be _Graph, v be Vertex of G;
thus v.edgesInOut() = v.edgesIn() \/ v.edgesOut()
.= G.edgesDBetween(the_Vertices_of G,{v}) \/ v.edgesOut() by Th39
.= G.edgesDBetween(the_Vertices_of G,{v}) \/
G.edgesDBetween({v},the_Vertices_of G) by Th39
.= G.edgesBetween(the_Vertices_of G,{v}) by Th150;
end;
theorem
for G being _Graph, X,Y being set
holds G.edgesDBetween(X,Y) = G.edgesOutOf(X) /\ G.edgesInto(Y)
proof
let G be _Graph, X,Y be set;
now
let e be object;
hereby
assume e in G.edgesDBetween(X,Y);
then e DSJoins X,Y,G by Def31;
then e in the_Edges_of G & (the_Source_of G).e in X &
(the_Target_of G).e in Y;
then e in G.edgesOutOf(X) & e in G.edgesInto(Y)
by Def26, Def27;
hence e in G.edgesOutOf(X) /\ G.edgesInto(Y) by XBOOLE_0:def 4;
end;
assume e in G.edgesOutOf(X) /\ G.edgesInto(Y);
then e in G.edgesOutOf(X) & e in G.edgesInto(Y) by XBOOLE_0:def 4;
then e in the_Edges_of G & (the_Source_of G).e in X &
(the_Target_of G).e in Y by Def26, Def27;
then e DSJoins X,Y,G;
hence e in G.edgesDBetween(X,Y) by Def31;
end;
hence thesis by TARSKI:2;
end;
theorem
for G being _Graph, X, Y being set
holds G.edgesDBetween(X,Y) c= G.edgesBetween(X,Y)
proof
let G be _Graph, X, Y be set;
now
let e be object;
assume e in G.edgesDBetween(X,Y);
then e DSJoins X,Y,G by Def31;
then e SJoins X,Y,G;
hence e in G.edgesBetween(X,Y) by Def30;
end;
hence thesis;
end;
:: generalized case for Th19
theorem
for G being _Graph, v being Vertex of G
st for e being object holds not e Joins v,v,G
holds card v.edgesInOut() = v.degree()
proof
let G be _Graph, v be Vertex of G;
assume A1: for e being object holds not e Joins v,v,G;
v.edgesIn() /\ v.edgesOut() = {}
proof
assume v.edgesIn() /\ v.edgesOut() <> {};
then consider e being object such that
A2: e in v.edgesIn() /\ v.edgesOut() by XBOOLE_0:def 1;
e in v.edgesIn() & e in v.edgesOut() by A2, XBOOLE_0:def 4;
then e in the_Edges_of G & (the_Target_of G).e = v &
(the_Source_of G).e = v by Lm7, Lm8;
then e Joins v,v,G;
hence contradiction by A1;
end;
hence thesis by CARD_2:35, XBOOLE_0:def 7;
end;
theorem
for G being _Graph, v being Vertex of G
holds v is isolated iff v.edgesIn() = {} & v.edgesOut() = {};
theorem Th156:
for G being _Graph, v being Vertex of G
holds v is isolated iff v.inDegree() = 0 & v.outDegree() = 0
proof
let G be _Graph, v be Vertex of G;
hereby
assume v is isolated;
then v.edgesIn() = {} & v.edgesOut() = {};
hence v.inDegree() = 0 & v.outDegree() = 0;
end;
assume v.inDegree() = 0 & v.outDegree() = 0;
then v.edgesIn() = {} & v.edgesOut() = {};
hence v is isolated;
end;
:: generalization of Def50
theorem
for G being _Graph, v being Vertex of G
holds v is isolated iff v.degree() = 0
proof
let G be _Graph, v be Vertex of G;
hereby
assume v is isolated;
then v.inDegree() = 0 & v.outDegree() = 0 by Th156;
hence v.degree() = card(0+0) by CARD_2:38
.= 0;
end;
assume A1: v.degree() = 0;
v.inDegree() c= v.degree() & v.outDegree() c= v.degree() by CARD_2:94;
then v.inDegree() = 0 & v.outDegree() = 0 by A1, XBOOLE_1:3;
hence thesis by Th156;
end;
theorem
for G being _Graph, X being set
holds G.edgesInto(X) = union {v.edgesIn() where v is Vertex of G : v in X}
proof
let G be _Graph, X be set;
set S = {v.edgesIn() where v is Vertex of G : v in X};
now
let e be object;
hereby
assume e in G.edgesInto(X);
then A1: e in the_Edges_of G & (the_Target_of G).e in X
by Def26;
then e Joins (the_Source_of G).e,(the_Target_of G).e,G;
then reconsider v = (the_Target_of G).e as Vertex of G
by FUNCT_2:5;
A2: e in v.edgesIn() by A1, Lm7;
v.edgesIn() in S by A1;
hence e in union S by A2, TARSKI:def 4;
end;
assume e in union S;
then consider E being set such that
A3: e in E & E in S by TARSKI:def 4;
consider v being Vertex of G such that
A4: E = v.edgesIn() & v in X by A3;
e in the_Edges_of G & (the_Target_of G).e = v by A3, A4, Lm7;
hence e in G.edgesInto(X) by A4, Def26;
end;
hence thesis by TARSKI:2;
end;
theorem
for G being _Graph, X being set
holds G.edgesOutOf(X) = union {v.edgesOut() where v is Vertex of G : v in X}
proof
let G be _Graph, X be set;
set S = {v.edgesOut() where v is Vertex of G : v in X};
now
let e be object;
hereby
assume e in G.edgesOutOf(X);
then A1: e in the_Edges_of G & (the_Source_of G).e in X
by Def27;
then e Joins (the_Source_of G).e,(the_Target_of G).e,G;
then reconsider v = (the_Source_of G).e as Vertex of G
by FUNCT_2:5;
A2: e in v.edgesOut() by A1, Lm8;
v.edgesOut() in S by A1;
hence e in union S by A2, TARSKI:def 4;
end;
assume e in union S;
then consider E being set such that
A3: e in E & E in S by TARSKI:def 4;
consider v being Vertex of G such that
A4: E = v.edgesOut() & v in X by A3;
e in the_Edges_of G & (the_Source_of G).e = v by A3, A4, Lm8;
hence e in G.edgesOutOf(X) by A4, Def27;
end;
hence thesis by TARSKI:2;
end;
theorem
for G being _Graph, X being set holds G.edgesInOut(X)
= union {v.edgesInOut() where v is Vertex of G : v in X}
proof
let G be _Graph, X be set;
set S = {v.edgesInOut() where v is Vertex of G : v in X};
now
let e be object;
hereby
assume e in G.edgesInOut(X);
then A1: e in the_Edges_of G & ((the_Source_of G).e in X
or (the_Target_of G).e in X) by Th28;
then A2: e Joins (the_Source_of G).e,(the_Target_of G).e,G;
per cases by A1;
suppose A3: (the_Source_of G).e in X;
reconsider v = (the_Source_of G).e as Vertex of G by A2, FUNCT_2:5;
A4: e in v.edgesInOut() by A1, Th61;
v.edgesInOut() in S by A3;
hence e in union S by A4, TARSKI:def 4;
end;
suppose A5: (the_Target_of G).e in X;
reconsider v = (the_Target_of G).e as Vertex of G by A2, FUNCT_2:5;
A6: e in v.edgesInOut() by A1, Th61;
v.edgesInOut() in S by A5;
hence e in union S by A6, TARSKI:def 4;
end;
end;
assume e in union S;
then consider E being set such that
A7: e in E & E in S by TARSKI:def 4;
consider v being Vertex of G such that
A8: E = v.edgesInOut() & v in X by A7;
e in the_Edges_of G & ((the_Source_of G).e = v or
(the_Target_of G).e = v) by A7, A8, Th61;
hence e in G.edgesInOut(X) by A8, Th28;
end;
hence thesis by TARSKI:2;
end;
theorem
for G being _Graph, X, Y being set holds G.edgesDBetween(X,Y)
= union {v.edgesOut() /\ w.edgesIn()
where v, w is Vertex of G : v in X & w in Y}
proof
let G be _Graph, X,Y be set;
set S = {v.edgesOut() /\ w.edgesIn()
where v, w is Vertex of G : v in X & w in Y};
now
let e be object;
hereby
assume e in G.edgesDBetween(X,Y);
then e DSJoins X,Y,G by Def31;
then A1: e in the_Edges_of G & (the_Source_of G).e in X &
(the_Target_of G).e in Y;
then A2: e DJoins (the_Source_of G).e, (the_Target_of G).e, G;
then e Joins (the_Source_of G).e, (the_Target_of G).e, G;
then reconsider v = (the_Source_of G).e, w = (the_Target_of G).e
as Vertex of G by FUNCT_2:5;
e DJoins v,w,G & e is set by A2;
then e in v.edgesOut() & e in w.edgesIn() by Th57, Th59;
then A3: e in v.edgesOut() /\ w.edgesIn() by XBOOLE_0:def 4;
v.edgesOut() /\ w.edgesIn() in S by A1;
hence e in union S by A3, TARSKI:def 4;
end;
assume e in union S;
then consider E being set such that
A4: e in E & E in S by TARSKI:def 4;
consider v,w being Vertex of G such that
A5: E = v.edgesOut() /\ w.edgesIn() & v in X & w in Y by A4;
e in v.edgesOut() & e in w.edgesIn() by A4, A5, XBOOLE_0:def 4;
then e in the_Edges_of G & (the_Source_of G).e = v &
(the_Target_of G).e = w by Lm7, Lm8;
then e DJoins v,w,G;
then e DSJoins X,Y,G by A5;
hence e in G.edgesDBetween(X,Y) by Def31;
end;
hence thesis by TARSKI:2;
end;
theorem Th162:
for G being _Graph, X, Y being set holds G.edgesBetween(X,Y)
c= union {v.edgesInOut() /\ w.edgesInOut()
where v, w is Vertex of G : v in X & w in Y}
proof
let G be _Graph, X,Y be set;
set S = {v.edgesInOut() /\ w.edgesInOut()
where v, w is Vertex of G : v in X & w in Y};
now
let e be object;
assume e in G.edgesBetween(X,Y);
then e SJoins X,Y,G by Def30;
then A1: e in the_Edges_of G & ((the_Source_of G).e in X &
(the_Target_of G).e in Y or (the_Source_of G).e in Y &
(the_Target_of G).e in X);
then A2: e Joins (the_Source_of G).e, (the_Target_of G).e, G;
then reconsider v = (the_Source_of G).e, w = (the_Target_of G).e
as Vertex of G by FUNCT_2:5;
e Joins v,w,G & e Joins w,v,G & e is set by A2;
then e in v.edgesInOut() & e in w.edgesInOut() by Th64;
then A3: e in v.edgesInOut() /\ w.edgesInOut() by XBOOLE_0:def 4;
v.edgesInOut() /\ w.edgesInOut() in S by A1;
hence e in union S by A3, TARSKI:def 4;
end;
hence thesis;
end;
theorem
for G being _Graph, X, Y being set st X misses Y holds G.edgesBetween(X,Y)
= union {v.edgesInOut() /\ w.edgesInOut()
where v, w is Vertex of G : v in X & w in Y}
proof
let G be _Graph, X,Y be set;
assume A1: X misses Y;
set S = {v.edgesInOut() /\ w.edgesInOut()
where v, w is Vertex of G : v in X & w in Y};
now
let e be object;
assume e in union S;
then consider E being set such that
A2: e in E & E in S by TARSKI:def 4;
consider v, w being Vertex of G such that
A3: E = v.edgesInOut() /\ w.edgesInOut() & v in X & w in Y by A2;
A4: e in v.edgesInOut() & e in w.edgesInOut() by A2, A3, XBOOLE_0:def 4;
then consider v2 being Vertex of G such that
A5: e Joins v,v2,G by Th64;
consider w2 being Vertex of G such that
A6: e Joins w,w2,G by A4, Th64;
A7: v = w & v2 = w2 or v = w2 & v2 = w by A5, A6;
v <> w
proof
assume v = w;
then v in X /\ Y by A3, XBOOLE_0:def 4;
hence contradiction by A1, XBOOLE_0:def 7;
end;
then e SJoins X,Y,G by A3, A5, A7;
hence e in G.edgesBetween(X,Y) by Def30;
end;
then A8: union S c= G.edgesBetween(X,Y);
G.edgesBetween(X,Y) c= union S by Th162;
hence thesis by A8, XBOOLE_0:def 10;
end;
theorem
for G1 being _Graph, E being set, G2 being removeEdges of G1, E
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds v2.edgesIn() = v1.edgesIn() \ E & v2.edgesOut() = v1.edgesOut() \ E &
v2.edgesInOut() = v1.edgesInOut() \ E
proof
let G1 be _Graph, E be set, G2 be removeEdges of G1, E;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2;
A2: the_Edges_of G2 = the_Edges_of G1 \ E by Th53;
now
let e be object;
hereby
assume A3: e in v2.edgesIn();
then A4: e in v1.edgesIn() by A1, Th78, TARSKI:def 3;
not e in E by A2, A3, XBOOLE_0:def 5;
hence e in v1.edgesIn() \ E by A4, XBOOLE_0:def 5;
end;
assume e in v1.edgesIn() \ E;
then A5: e in v1.edgesIn() & not e in E by XBOOLE_0:def 5;
then A6: e in the_Edges_of G2 by A2, XBOOLE_0:def 5;
v1 = (the_Target_of G1).e by A5, Lm7
.= (the_Target_of G2).e by A6, Def32;
hence e in v2.edgesIn() by A1, A6, Lm7;
end;
hence A7: v2.edgesIn() = v1.edgesIn() \ E by TARSKI:2;
now
let e be object;
hereby
assume A8: e in v2.edgesOut();
then A9: e in v1.edgesOut() by A1, Th78, TARSKI:def 3;
not e in E by A2, A8, XBOOLE_0:def 5;
hence e in v1.edgesOut() \ E by A9, XBOOLE_0:def 5;
end;
assume e in v1.edgesOut() \ E;
then A10: e in v1.edgesOut() & not e in E by XBOOLE_0:def 5;
then A11: e in the_Edges_of G2 by A2, XBOOLE_0:def 5;
v1 = (the_Source_of G1).e by A10, Lm8
.= (the_Source_of G2).e by A11, Def32;
hence e in v2.edgesOut() by A1, A11, Lm8;
end;
hence A12: v2.edgesOut() = v1.edgesOut() \ E by TARSKI:2;
thus v2.edgesInOut() = v1.edgesInOut() \ E by A7, A12, XBOOLE_1:42;
end;
theorem
for G1, G2 being _Graph, V being set
holds G2 is removeVertices of G1, V iff
G2 is removeVertices of G1, V /\ the_Vertices_of G1
proof
let G1, G2 be _Graph, V be set;
the_Vertices_of G1 \ V = the_Vertices_of G1 \ (V /\ the_Vertices_of G1)
by XBOOLE_1:47;
hence thesis;
end;
theorem Th166:
for G1 being _Graph, V being set, G2 being removeVertices of G1, V
for v1 being Vertex of G1, v2 being Vertex of G2
st V c< the_Vertices_of G1 & v1 = v2 holds
v2.edgesIn() = v1.edgesIn() \ G1.edgesOutOf(V) &
v2.edgesOut() = v1.edgesOut() \ G1.edgesInto(V) &
v2.edgesInOut() = v1.edgesInOut() \ G1.edgesInOut(V)
proof
let G1 be _Graph, V be set, G2 be removeVertices of G1, V;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: V c< the_Vertices_of G1 & v1 = v2;
then A2: the_Edges_of G2 = G1.edgesBetween(the_Vertices_of G1 \ V)
by Th49;
the_Vertices_of G2 = the_Vertices_of G1 \ V by A1, Th49;
then A3: not v2 in V by XBOOLE_0:def 5;
now
let e be object;
hereby
assume A4: e in v2.edgesIn();
then A5: e in v1.edgesIn() by A1, Th78, TARSKI:def 3;
e in G1.edgesOutOf(the_Vertices_of G1 \ V) by A2, A4, XBOOLE_0:def 4;
then (the_Source_of G1).e in the_Vertices_of G1 \ V by Def27;
then not (the_Source_of G1).e in V by XBOOLE_0:def 5;
then not e in G1.edgesOutOf(V) by Def27;
hence e in v1.edgesIn() \ G1.edgesOutOf(V) by A5, XBOOLE_0:def 5;
end;
assume e in v1.edgesIn() \ G1.edgesOutOf(V);
then A6: e in v1.edgesIn() & not e in G1.edgesOutOf(V) by XBOOLE_0:def 5;
then A7: not (the_Source_of G1).e in V by Def27;
e Joins (the_Source_of G1).e, (the_Target_of G1).e, G1 by A6;
then A8: (the_Source_of G1).e in the_Vertices_of G1 &
(the_Target_of G1).e in the_Vertices_of G1 by FUNCT_2:5;
then (the_Source_of G1).e in the_Vertices_of G1 \ V by A7, XBOOLE_0:def 5;
then A9: e in G1.edgesOutOf(the_Vertices_of G1\V) by A6, Def27;
not (the_Target_of G1).e in V by A1, A3, A6, Lm7;
then (the_Target_of G1).e in the_Vertices_of G1 \ V by A8, XBOOLE_0:def 5;
then e in G1.edgesInto(the_Vertices_of G1 \ V) by A6, Def26;
then A10: e in the_Edges_of G2 by A2, A9, XBOOLE_0:def 4;
v1 = (the_Target_of G1).e by A6, Lm7
.= (the_Target_of G2).e by A10, Def32;
hence e in v2.edgesIn() by A1, A10, Lm7;
end;
hence A11: v2.edgesIn() = v1.edgesIn() \ G1.edgesOutOf(V) by TARSKI:2;
now
let e be object;
hereby
assume A12: e in v2.edgesOut();
then A13: e in v1.edgesOut() by A1, Th78, TARSKI:def 3;
e in G1.edgesInto(the_Vertices_of G1 \ V) by A2, A12, XBOOLE_0:def 4;
then (the_Target_of G1).e in the_Vertices_of G1 \ V by Def26;
then not (the_Target_of G1).e in V by XBOOLE_0:def 5;
then not e in G1.edgesInto(V) by Def26;
hence e in v1.edgesOut() \ G1.edgesInto(V) by A13, XBOOLE_0:def 5;
end;
assume e in v1.edgesOut() \ G1.edgesInto(V);
then A14: e in v1.edgesOut() & not e in G1.edgesInto(V) by XBOOLE_0:def 5;
then A15: not (the_Target_of G1).e in V by Def26;
e Joins (the_Source_of G1).e, (the_Target_of G1).e, G1 by A14;
then A16: (the_Source_of G1).e in the_Vertices_of G1 &
(the_Target_of G1).e in the_Vertices_of G1 by FUNCT_2:5;
then (the_Target_of G1).e in the_Vertices_of G1 \ V by A15, XBOOLE_0:def 5;
then A17: e in G1.edgesInto(the_Vertices_of G1\V) by A14, Def26;
not (the_Source_of G1).e in V by A1, A3, A14, Lm8;
then (the_Source_of G1).e in the_Vertices_of G1 \ V by A16, XBOOLE_0:def 5;
then e in G1.edgesOutOf(the_Vertices_of G1 \ V) by A14, Def27;
then A18: e in the_Edges_of G2 by A2, A17, XBOOLE_0:def 4;
v1 = (the_Source_of G1).e by A14, Lm8
.= (the_Source_of G2).e by A18, Def32;
hence e in v2.edgesOut() by A1, A18, Lm8;
end;
hence A19: v2.edgesOut() = v1.edgesOut() \ G1.edgesInto(V) by TARSKI:2;
v1.edgesOut() /\ G1.edgesOutOf(V) = {}
proof
assume v1.edgesOut() /\ G1.edgesOutOf(V) <> {};
then consider e being object such that
A20: e in v1.edgesOut() /\ G1.edgesOutOf(V) by XBOOLE_0:def 1;
e in v1.edgesOut() & e in G1.edgesOutOf(V) by A20, XBOOLE_0:def 4;
then (the_Source_of G1).e = v1 & (the_Source_of G1).e in V
by Def27, Lm8;
hence contradiction by A1, A3;
end;
then v1.edgesOut() misses G1.edgesOutOf(V) by XBOOLE_0:def 7;
then A21: v1.edgesOut() \ G1.edgesInto(V) misses G1.edgesOutOf(V)
by XBOOLE_1:36, XBOOLE_1:63;
v1.edgesIn() /\ G1.edgesInto(V) = {}
proof
assume v1.edgesIn() /\ G1.edgesInto(V) <> {};
then consider e being object such that
A22: e in v1.edgesIn() /\ G1.edgesInto(V) by XBOOLE_0:def 1;
e in v1.edgesIn() & e in G1.edgesInto(V) by A22, XBOOLE_0:def 4;
then (the_Target_of G1).e = v1 & (the_Target_of G1).e in V
by Def26, Lm7;
hence contradiction by A1, A3;
end;
then A23: v1.edgesIn() misses G1.edgesInto(V) by XBOOLE_0:def 7;
thus v2.edgesInOut()
= (v1.edgesIn() \/ (v1.edgesOut() \ G1.edgesInto(V))) \
G1.edgesOutOf(V) by A11, A19, A21, XBOOLE_1:87
.= v1.edgesInOut() \ G1.edgesInto(V) \ G1.edgesOutOf(V) by A23, XBOOLE_1:87
.= v1.edgesInOut() \ G1.edgesInOut(V) by XBOOLE_1:41;
end;
theorem
for G1 being non _trivial _Graph, v being Vertex of G1
for G2 being removeVertex of G1, v
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 holds
v2.edgesIn() = v1.edgesIn() \ v.edgesOut() &
v2.edgesOut() = v1.edgesOut() \ v.edgesIn() &
v2.edgesInOut() = v1.edgesInOut() \ v.edgesInOut()
proof
let G1 be non _trivial _Graph, v be Vertex of G1;
let G2 be removeVertex of G1, v;
let v1 be Vertex of G1, v2 be Vertex of G2;
assume A1: v1 = v2;
(the_Vertices_of G1) \ {v} <> {} by Th20;
then the_Vertices_of G1 <> {v} by XBOOLE_1:37;
then {v} c< the_Vertices_of G1 by XBOOLE_0:def 8;
hence thesis by A1, Th166;
end;
:: from GLIBPRE1, 2024.10.29, S.K.
registration
let G be non _trivial _Graph;
cluster non empty proper for Subset of the_Vertices_of G;
existence
proof
set v = the Vertex of G;
reconsider S = {v} as Subset of the_Vertices_of G;
take S;
S <> the_Vertices_of G
proof
assume S = the_Vertices_of G;
then card the_Vertices_of G = 1 by CARD_1:30;
hence contradiction by Def19;
end;
hence thesis by SUBSET_1:def 6;
end;
end;
theorem
for G being _Graph, X being set holds G.edgesBetween(X,X) = G.edgesBetween(X)
proof
let G be _Graph, X be set;
now
let e be object;
hereby
assume e in G.edgesBetween(X,X);
then e SJoins X,X,G by Def30;
then e in the_Edges_of G & (the_Source_of G).e in X &
(the_Target_of G).e in X;
hence e in G.edgesBetween(X) by Lm5;
end;
assume e in G.edgesBetween(X);
then e in the_Edges_of G & (the_Source_of G).e in X &
(the_Target_of G).e in X by Lm5;
then e SJoins X,X,G;
hence e in G.edgesBetween(X,X) by Def30;
end;
hence thesis by TARSKI:2;
end;
theorem
for G being _Graph holds G is _trivial iff the_Vertices_of G is trivial
proof
let G be _Graph;
thus G is _trivial implies the_Vertices_of G is trivial;
assume A1: the_Vertices_of G is trivial;
assume G is non _trivial;
then consider v1, v2 being Vertex of G such that
A2: v1 <> v2 by Th21;
thus contradiction by A1, A2, ZFMISC_1:def 10;
end;
theorem
for G1 being _Graph, G2 being Subgraph of G1
holds G2 is inducedSubgraph of G1, the_Vertices_of G2, the_Edges_of G2
proof
let G1 be _Graph, G2 be Subgraph of G1;
the_Edges_of G2 = G2.edgesBetween(the_Vertices_of G2) by Th34;
then the_Edges_of G2 c= G1.edgesBetween(the_Vertices_of G2) by Th76;
hence thesis by Def37;
end;
theorem
for G1, G2 being _Graph, G3 being spanning Subgraph of G1
st G2 == G3 holds G2 is spanning Subgraph of G1
proof
let G1, G2 be _Graph, G3 be spanning Subgraph of G1;
assume A1: G2 == G3;
then the_Vertices_of G2 = the_Vertices_of G1 by Def33;
hence thesis by A1, Th92, Def33;
end;
theorem
for G being _Graph, e being object st e in the_Edges_of G
holds e in G.edgesBetween({(the_Source_of G).e,(the_Target_of G).e})
proof
let G be _Graph, e be object;
set v = (the_Source_of G).e, w = (the_Target_of G).e;
assume A1: e in the_Edges_of G;
v in {v,w} & w in {v,w} by TARSKI:def 2;
hence e in G.edgesBetween({v,w}) by A1, Lm5;
end;
theorem
for G being _Graph holds G == createGraph(the_Vertices_of G, the_Edges_of G,
the_Source_of G, the_Target_of G);
:: generalization of Def52
theorem
for G being _Graph, v being Vertex of G
holds v is endvertex iff v.degree() = 1
proof
let G be _Graph, v be Vertex of G;
hereby
assume v is endvertex;
then consider e being object such that
A1: v.edgesInOut() = {e} & not e Joins v,v,G;
e in v.edgesInOut() by A1, TARSKI:def 1;
:: symmetric cases
then per cases by XBOOLE_0:def 3;
suppose A2: e in v.edgesIn();
then consider w being set such that
A3: e DJoins w,v,G by Th57;
(the_Source_of G).e <> v by A1, A3;
then not e in v.edgesOut() by Lm8;
then A4: not {e} c= v.edgesOut() by ZFMISC_1:31;
v.edgesIn() c= {e} & v.edgesOut() c= {e} by A1, XBOOLE_1:7;
then v.edgesIn() = {e} & v.edgesOut() = {} by A2, A4, ZFMISC_1:33;
hence v.degree() = card 1 +` card 0 by CARD_1:30
.= card(1+0) by CARD_2:38
.= 1;
end;
suppose A5: e in v.edgesOut();
then consider w being set such that
A6: e DJoins v,w,G by Th59;
(the_Target_of G).e <> v by A1, A6;
then not e in v.edgesIn() by Lm7;
then A7: not {e} c= v.edgesIn() by ZFMISC_1:31;
v.edgesIn() c= {e} & v.edgesOut() c= {e} by A1, XBOOLE_1:7;
then v.edgesIn() = {} & v.edgesOut() = {e} by A5, A7, ZFMISC_1:33;
hence v.degree() = card 1 +` card 0 by CARD_1:30
.= card(1+0) by CARD_2:38
.= 1;
end;
end;
assume A8: v.degree() = 1;
:: prove with simple cardinal arithmetic
(v.inDegree()=1 & v.outDegree()=0) or (v.inDegree()=0 & v.outDegree()=1)
proof
assume not (v.inDegree()=1 & v.outDegree()=0);
then per cases;
suppose A9: v.inDegree() <> 1;
v.inDegree() c= 1 by A8, CARD_2:94;
then not 1 c= v.inDegree() by A9, XBOOLE_0:def 10;
then v.inDegree() in 1 by ORDINAL1:16;
hence v.inDegree() = 0 by CARD_1:49, TARSKI:def 1;
hence v.outDegree() = 1 by A8, CARD_2:18;
end;
suppose v.outDegree() <> 0;
then not v.outDegree() in 1 by CARD_1:49, TARSKI:def 1;
then A10: 1 c= v.outDegree() by ORDINAL1:16;
v.outDegree() c= 1 by A8, CARD_2:94;
then A11: v.outDegree() = 1 by A10, XBOOLE_0:def 10;
hereby
assume v.inDegree() <> 0;
then not v.inDegree() in 1 by CARD_1:49, TARSKI:def 1;
then A12: 1 c= v.inDegree() by ORDINAL1:16;
v.inDegree() c= 1 by A8, CARD_2:94;
then v.inDegree() +` v.outDegree()
= card 1 +` card 1 by A11, A12, XBOOLE_0:def 10
.= card(1+1) by CARD_2:38
.= 2;
hence contradiction by A8;
end;
thus thesis by A11;
end;
end;
:: symmetric cases
then per cases;
suppose A13: v.inDegree()=1 & v.outDegree()=0;
then v.inDegree() = card {{}} by CARD_1:30;
then consider e being object such that
A14: v.edgesIn() = {e} by CARD_1:29;
v.edgesOut() = {} by A13;
then A15: v.edgesInOut() = {e} by A14;
not e Joins v,v,G
proof
assume e Joins v,v,G;
then e DJoins v,v,G & e is set;
then e in v.edgesOut() by Th59;
hence contradiction by A13;
end;
hence thesis by A15;
end;
suppose A16: v.inDegree()=0 & v.outDegree()=1;
then v.outDegree() = card {{}} by CARD_1:30;
then consider e being object such that
A17: v.edgesOut() = {e} by CARD_1:29;
v.edgesIn() = {} by A16;
then A18: v.edgesInOut() = {e} by A17;
not e Joins v,v,G
proof
assume e Joins v,v,G;
then e DJoins v,v,G & e is set;
then e in v.edgesIn() by Th57;
hence contradiction by A16;
end;
hence thesis by A18;
end;
end;
theorem
for G being loopless _Graph, v being Vertex of G holds
v.inNeighbors() c= the_Vertices_of G \ {v} &
v.outNeighbors() c= the_Vertices_of G \ {v} &
v.allNeighbors() c= the_Vertices_of G \ {v}
proof
let G be loopless _Graph, v be Vertex of G;
now
let x be object;
assume A1: x in v.inNeighbors();
then ex e being object st e DJoins x,v,G by Th69;
then v <> x by Th136;
hence x in the_Vertices_of G \ {v} by A1, ZFMISC_1:56;
end;
hence v.inNeighbors() c= the_Vertices_of G \ {v};
now
let x be object;
assume A2: x in v.outNeighbors();
then ex e being object st e DJoins v,x,G by Th70;
then v <> x by Th136;
hence x in the_Vertices_of G \ {v} by A2, ZFMISC_1:56;
end;
hence v.outNeighbors() c= the_Vertices_of G \ {v};
now
let x be object;
assume A3: x in v.allNeighbors();
then ex e being object st e Joins v,x,G by Th71;
then v <> x by Th18;
hence x in the_Vertices_of G \ {v} by A3, ZFMISC_1:56;
end;
hence v.allNeighbors() c= the_Vertices_of G \ {v};
end;
theorem
for G being _Graph st (for v being Vertex of G holds
v.inNeighbors() c= the_Vertices_of G \ {v} or
v.outNeighbors() c= the_Vertices_of G \ {v} or
v.allNeighbors() c= the_Vertices_of G \ {v})
holds G is loopless
proof
let G be _Graph;
assume A1: for v being Vertex of G holds
v.inNeighbors() c= the_Vertices_of G \ {v} or
v.outNeighbors() c= the_Vertices_of G \ {v} or
v.allNeighbors() c= the_Vertices_of G \ {v};
now
let v be object;
given e being object such that
A2: e Joins v,v,G;
reconsider w = v as Vertex of G by A2, FUNCT_2:5;
e DJoins v,v,G by A2;
then A3: v in w.inNeighbors() & v in w.outNeighbors() &
v in w.allNeighbors() by A2, Th69, Th70, Th71;
v in the_Vertices_of G \ {w}
proof
per cases by A1;
suppose w.inNeighbors() c= the_Vertices_of G \ {w};
hence thesis by A3;
end;
suppose w.outNeighbors() c= the_Vertices_of G \ {w};
hence thesis by A3;
end;
suppose w.allNeighbors() c= the_Vertices_of G \ {w};
hence thesis by A3;
end;
end;
hence contradiction by ZFMISC_1:56;
end;
hence thesis by Th18;
end;
:: basic Proof copied from NAT --> G -> Graph-yielding
registration
let X be set, G be _Graph;
cluster X --> G -> Graph-yielding;
coherence
proof
per cases;
suppose A1: X <> {};
set F = X --> G;
reconsider F as ManySortedSet of X;
now
let x be object;
assume x in dom F;
then F.x in rng F by FUNCT_1:3;
then F.x in {G} by A1, FUNCOP_1:8;
hence F.x is _Graph by TARSKI:def 1;
end;
hence thesis;
end;
suppose X = {};
hence thesis;
end;
end;
end;
registration
let x be object, G be _Graph;
cluster x .--> G -> Graph-yielding;
coherence;
end;
registration
let X be set;
cluster Graph-yielding for ManySortedSet of X;
existence
proof
take X --> the _Graph;
thus thesis;
end;
end;
registration
let X be non empty set;
cluster non empty Graph-yielding for ManySortedSet of X;
existence
proof
take X --> the _Graph;
thus thesis;
end;
end;