:: About Graph Complements
:: by Sebastian Koch
::
:: Received December 30, 2019
:: Copyright (c) 2019-2021 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, RING_3, PARTFUN1, FUNCT_2, CHORD,
SCMYCIEL, REWRITE1, ARYTM_1, GLIB_006, GLIB_007, GLIB_009, GLIB_010,
GLIB_011, GLIB_012, MCART_1, WAYBEL_0, MOD_4, RELAT_2, GRAPH_1, GLIB_001,
ORDINAL4, ABIAN, SGRAPH1, RFINSEQ, FINSEQ_8, GRAPH_2;
notations TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1,
ENUMSET1, FUNCT_4, FINSET_1, CARD_1, PBOOLE, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, NAT_1, INT_1, VALUED_0, NAT_D, CARD_2, FINSEQ_1, NEWTON, ABIAN,
RFINSEQ, FINSEQ_6, FINSEQ_8, GRAPH_2, GLIB_000, GLIB_001, GLIB_002,
CHORD, GLIB_006, GLIB_007, GLIB_008, GLIB_009, GLIB_010, GLIB_011;
constructors DOMAIN_1, FUNCT_4, XXREAL_0, NAT_1, NAT_D, BINOP_2, CARD_2,
FINSEQ_4, PBOOLE, ORDINAL3, WELLORD2, PARTFUN1, RELSET_1, GLIB_000,
NEWTON, XTUPLE_0, CHORD, GLIB_002, GLIB_006, GLIB_007, GLIB_008,
GLIB_009, GLIB_010, GLIB_011, GLIB_001, ABIAN, BINOP_1, FINSOP_1,
RVSUM_1, FINSEQ_5, GRAPH_5, FUNCT_2, FIB_NUM2, FINSEQ_8, HELLY, FUNCT_3,
GRAPH_2, RFINSEQ, FINSEQ_6, FUNCT_7, FINSEQ_1, SUBSET_1, RELAT_1,
ENUMSET1, ORDINAL1, INT_1, XREAL_0, XCMPLX_0, FINSET_1, CARD_3, FUNCT_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCOP_1, FINSET_1,
XREAL_0, NAT_1, CARD_1, FINSEQ_1, RELSET_1, GLIB_000, CHORD, GLIB_006,
GLIB_007, GLIB_009, GLIB_008, GLIB_010, GLIB_011, XTUPLE_0, ABIAN,
GLIB_001, MEMBERED, INT_1, MSAFREE5;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
begin :: Loopfull Graphs
definition
let G be _Graph;
attr G is loopfull means
:: GLIB_012:def 1 :: or reflexive
for v being Vertex of G ex e being object st e Joins v,v,G;
end;
theorem :: GLIB_012:1
for G being _Graph holds G is loopfull iff
for v being Vertex of G ex e being object st e DJoins v,v,G;
theorem :: GLIB_012:2
for G being _Graph holds G is loopfull iff
for v being Vertex of G holds v,v are_adjacent;
registration
cluster loopfull -> non loopless for _Graph;
cluster _trivial non loopless -> loopfull for _Graph;
cluster loopfull complete for _Graph;
cluster non loopfull for _Graph;
end;
theorem :: GLIB_012:3
for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
holds G1 is loopfull iff G2 is loopfull;
registration
let G be loopfull _Graph, E be set;
cluster -> loopfull for reverseEdgeDirections of G, E;
end;
registration
let G be non loopfull _Graph, E be set;
cluster -> non loopfull for reverseEdgeDirections of G, E;
end;
theorem :: GLIB_012:4
for G1, G2 being _Graph st G1 == G2
holds G1 is loopfull implies G2 is loopfull;
theorem :: GLIB_012:5
for G2 being loopfull _Graph, G1 being Supergraph of G2
st the_Vertices_of G1 = the_Vertices_of G2 holds G1 is loopfull;
theorem :: GLIB_012:6
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st rng F_V = the_Vertices_of G2 & G1.loops() c= dom F_E
holds G1 is loopfull implies G2 is loopfull;
theorem :: GLIB_012:7
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is total onto holds G1 is loopfull implies G2 is loopfull;
theorem :: GLIB_012:8
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is semi-continuous & dom F_V=the_Vertices_of G1 & G2.loops() c= rng F_E
holds G2 is loopfull implies G1 is loopfull;
theorem :: GLIB_012:9
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is total onto semi-continuous
holds G2 is loopfull implies G1 is loopfull;
theorem :: GLIB_012:10
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is isomorphism holds G1 is loopfull iff G2 is loopfull;
registration
let G be loopfull _Graph, V be set;
cluster -> loopfull for inducedSubgraph of G, V;
cluster -> loopfull for removeVertices of G, V;
cluster -> loopfull for removeVertex of G, V;
end;
registration
let G be non loopfull _Graph;
cluster -> non loopfull for spanning Subgraph of G;
let E be set;
cluster -> non loopfull for inducedSubgraph of G, the_Vertices_of G, E;
cluster -> non loopfull for removeEdges of G, E;
cluster -> non loopfull for removeEdge of G, E;
end;
theorem :: GLIB_012:11
for G2 being _Graph, V being set, G1 being addVertices of G2, V
st V \ the_Vertices_of G2 <> {} holds G1 is non loopfull;
registration
let G be non loopfull _Graph, V be set;
cluster -> non loopfull for addVertices of G, V;
end;
registration
let G be loopfull _Graph, v,e,w be object;
cluster -> loopfull for addEdge of G,v,e,w;
end;
theorem :: GLIB_012:12
for G2 being _Graph, v being Vertex of G2, e,w being object
for G1 being addAdjVertex of G2,v,e,w
st not e in the_Edges_of G2 & not w in the_Vertices_of G2
holds G1 is non loopfull;
theorem :: GLIB_012:13
for G2 being _Graph, v,e being object, w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
st not e in the_Edges_of G2 & not v in the_Vertices_of G2
holds G1 is non loopfull;
registration
let G be non loopfull _Graph, v,e,w be object;
cluster -> non loopfull for addAdjVertex of G,v,e,w;
end;
theorem :: GLIB_012:14
for G2 being _Graph, v being object, V being Subset of the_Vertices_of G2
for G1 being addAdjVertexAll of G2,v,V st not v in the_Vertices_of G2
holds G1 is non loopfull;
registration
let G be non loopfull _Graph, v be object, V be set;
cluster -> non loopfull for addAdjVertexAll of G,v,V;
end;
registration
let G be loopfull _Graph;
cluster -> loopfull for removeParallelEdges of G;
cluster -> loopfull for removeDParallelEdges of G;
end;
:: removeLoops is loopless, hence non loopfull
registration
let G be non loopfull _Graph;
cluster -> non loopfull for removeParallelEdges of G;
cluster -> non loopfull for removeDParallelEdges of G;
end;
definition
let GF be Graph-yielding Function;
attr GF is loopfull means
:: GLIB_012:def 2
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is loopfull;
end;
registration
let G be loopfull _Graph;
cluster <* G *> -> loopfull;
cluster NAT --> G -> loopfull;
end;
definition
let GF be non empty Graph-yielding Function;
redefine attr GF is loopfull means
:: GLIB_012:def 3
for x being Element of dom GF holds GF.x is loopfull;
end;
definition
let GSq be GraphSeq;
redefine attr GSq is loopfull means
:: GLIB_012:def 4
for n being Nat holds GSq.n is loopfull;
end;
registration
cluster empty -> loopfull for Graph-yielding Function;
cluster non empty loopfull -> non loopless for Graph-yielding Function;
end;
registration
cluster loopfull for GraphSeq;
cluster non empty loopfull for Graph-yielding FinSequence;
end;
registration
let GF be loopfull non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> loopfull;
end;
registration
let GSq be loopfull GraphSeq, x be Nat;
cluster GSq.x -> loopfull;
end;
registration
let p be loopfull Graph-yielding FinSequence, n be Nat;
cluster p | n -> loopfull;
cluster p /^ n -> loopfull;
let m be Nat;
cluster smid(p,m,n) -> loopfull;
cluster (m,n)-cut p -> loopfull;
end;
registration
let p, q be loopfull Graph-yielding FinSequence;
cluster p ^ q -> loopfull;
cluster p ^' q -> loopfull;
end;
registration
let G1, G2 be loopfull _Graph;
cluster <* G1, G2 *> -> loopfull;
let G3 be loopfull _Graph;
cluster <* G1, G2, G3 *> -> loopfull;
end;
begin :: Adding Loops to a Graph
:: a loop is added to each vertex in V, regardless if that
:: vertex has a loop already or not
definition
let G be _Graph, V be set;
mode addLoops of G, V -> Supergraph of G means
:: GLIB_012:def 5
the_Vertices_of it = the_Vertices_of G &
ex E being set, f being one-to-one Function
st E misses the_Edges_of G & the_Edges_of it = the_Edges_of G \/ E &
dom f = E & rng f = V & the_Source_of it = the_Source_of G +* f &
the_Target_of it = the_Target_of G +* f if V c= the_Vertices_of G
otherwise it == G;
end;
definition
let G be _Graph;
mode addLoops of G is addLoops of G, the_Vertices_of G;
end;
theorem :: GLIB_012:15
for G2 being _Graph, V being set, G1 being addLoops of G2, V
holds the_Vertices_of G1 = the_Vertices_of G2;
theorem :: GLIB_012:16
for G2 being _Graph, V being set, G1 being addLoops of G2, V
for e,v,w being object st v <> w holds e DJoins v,w,G1 iff e DJoins v,w,G2;
theorem :: GLIB_012:17
for G2 being _Graph, V being set, G1 being addLoops of G2, V
for e,v,w being object st v <> w holds e Joins v,w,G1 iff e Joins v,w,G2;
theorem :: GLIB_012:18
for G2 being _Graph, V being Subset of the_Vertices_of G2
for G1 being addLoops of G2, V for v being Vertex of G1
st v in V holds v,v are_adjacent;
theorem :: GLIB_012:19
for G2 being _Graph, V being set
for G1 being addLoops of G2, V holds G1.order() = G2.order();
theorem :: GLIB_012:20
for G2 being _Graph, V being Subset of the_Vertices_of G2
for G1 being addLoops of G2, V holds G1.size() = G2.size() +` card V;
theorem :: GLIB_012:21
for G1, G2 being _Graph holds G1 is addLoops of G2, {} iff G1 == G2;
theorem :: GLIB_012:22
for G being _Graph holds G is addLoops of G, {};
theorem :: GLIB_012:23
for G being _Graph, V1, V2 being Subset of the_Vertices_of G
for G1 being addLoops of G, V1, G2 being addLoops of G1, V2
st V1 misses V2 holds G2 is addLoops of G, V1 \/ V2;
theorem :: GLIB_012:24
for G3 being _Graph, V1, V2 being Subset of the_Vertices_of G3
for G1 being addLoops of G3, V1 \/ V2 st V1 misses V2
ex G2 being addLoops of G3, V1 st G1 is addLoops of G2, V2;
theorem :: GLIB_012:25
for G2 being loopless _Graph, V being Subset of the_Vertices_of G2
for G1 being addLoops of G2, V
holds the_Edges_of G2 misses G1.loops() &
the_Edges_of G1 = the_Edges_of G2 \/ G1.loops();
theorem :: GLIB_012:26
for G1 being loopless _Graph, V being set
for G2 being addLoops of G1, V, G3 being removeLoops of G2
holds G1 == G3;
theorem :: GLIB_012:27
for G1, G2 being _Graph, v being Vertex of G2
holds G1 is addLoops of G2, {v} iff ex e being object
st not e in the_Edges_of G2 & G1 is addEdge of G2,v,e,v;
:: finite addition of loops can be finitely constructed with one loop at a time
theorem :: GLIB_012:28
for G2 being _Graph, V being finite Subset of the_Vertices_of G2
for G1 being addLoops of G2, V
ex p being non empty Graph-yielding FinSequence
st p.1 == G2 & p.len p = G1 & len p = card V + 1 &
for n being Element of dom p st n <= len p - 1 holds
ex v being Vertex of G2, e being object
st p.(n+1) is addEdge of p.n, v,e,v & v in V & not e in the_Edges_of p.n;
theorem :: GLIB_012:29
for G3, G4 being _Graph, V1, V2 being set
for G1 being addLoops of G3, V1, G2 being addLoops of G4, V2
for F0 being PGraphMapping of G3, G4
st V1 c= the_Vertices_of G3 & V2 c= the_Vertices_of G4 &
F0_V | V1 is one-to-one & dom(F0_V | V1) = V1 & rng(F0_V | V1) = V2
ex F being PGraphMapping of G1, G2 st
F_V = F0_V & F_E | dom F0_E = F0_E &
(F0 is non empty implies F is non empty) &
(F0 is total implies F is total) &
(F0 is onto implies F is onto) &
(F0 is one-to-one implies F is one-to-one) &
(F0 is directed implies F is directed) &
(F0 is weak_SG-embedding implies F is weak_SG-embedding) &
(F0 is isomorphism implies F is isomorphism) &
(F0 is Disomorphism implies F is Disomorphism);
theorem :: GLIB_012:30
for G3 being _Graph, G4 being G3-isomorphic _Graph
for G1 being addLoops of G3 for G2 being addLoops of G4
holds G2 is G1-isomorphic;
theorem :: GLIB_012:31
for G3 being _Graph, G4 being G3-Disomorphic _Graph
for G1 being addLoops of G3 for G2 being addLoops of G4
holds G2 is G1-Disomorphic;
theorem :: GLIB_012:32
for G3, G4 being _Graph, V being set
for G1 being addLoops of G3, V, G2 being addLoops of G4, V
st G3 == G4 holds G2 is G1-Disomorphic;
theorem :: GLIB_012:33
for G3 being _Graph, V, E being set, G4 being reverseEdgeDirections of G3, E
for G1 being addLoops of G3, V, G2 being addLoops of G4, V
holds G2 is G1-isomorphic;
theorem :: GLIB_012:34
for G3 being _Graph, E, V being set, G4 being reverseEdgeDirections of G3, E
for G1 being addLoops of G3, V, G2 being reverseEdgeDirections of G1, E
st E c= the_Edges_of G3 holds G2 is addLoops of G4, V;
theorem :: GLIB_012:35
for G3 being _Graph, V1 being Subset of the_Vertices_of G3
for V2 being non empty Subset of the_Vertices_of G3
for G4 being inducedSubgraph of G3, V2
for G1 being addLoops of G3, V1, G2 being inducedSubgraph of G1, V2
holds G2 is addLoops of G4, V1 /\ V2;
theorem :: GLIB_012:36
for G2 being _Graph, V being set, G1 being addLoops of G2, V
for v1 being Vertex of G1, v2 being Vertex of G2
st not v1 in V & v1 = v2 holds
(v1 is isolated iff v2 is isolated) &
(v1 is endvertex iff v2 is endvertex);
theorem :: GLIB_012:37
for G2 being _Graph, V being set, G1 being addLoops of G2, V
for P being Path of G1
holds P is Path of G2 or
ex v,e being object st e Joins v,v,G1 & P = G1.walkOf(v,e,v);
theorem :: GLIB_012:38
for G2 being _Graph, V being set, G1 being addLoops of G2, V
for W being Walk of G1 st W.edges() misses G1.loops() \ G2.loops()
holds W is Walk of G2;
registration
let G be _Graph;
cluster -> loopfull for addLoops of G;
let V be non empty Subset of the_Vertices_of G;
cluster -> non loopless for addLoops of G, V;
end;
theorem :: GLIB_012:39
for G2 being _Graph, V being set, G1 being addLoops of G2, V
holds G1 is _finite iff G2 is _finite;
registration
let G be _finite _Graph, V be set;
cluster -> _finite for addLoops of G, V;
end;
registration
let G be non _finite _Graph, V be set;
cluster -> non _finite for addLoops of G, V;
end;
theorem :: GLIB_012:40
for G2 being _Graph, V being set, G1 being addLoops of G2, V
holds G1 is connected iff G2 is connected;
registration
let G be connected _Graph, V be set;
cluster -> connected for addLoops of G, V;
end;
registration
let G be non connected _Graph, V be set;
cluster -> non connected for addLoops of G, V;
end;
theorem :: GLIB_012:41
for G2 being _Graph, V being set, G1 being addLoops of G2, V
holds G1 is chordal iff G2 is chordal;
registration
let G be chordal _Graph, V be set;
cluster -> chordal for addLoops of G, V;
end;
:: non chordal clustering will be done later
registration
let G be non edgeless _Graph, V be set;
cluster -> non edgeless for addLoops of G, V;
end;
registration
let G be loopfull _Graph, V be set;
cluster -> loopfull for addLoops of G, V;
end;
registration
let G be simple _Graph, V be set;
cluster -> non-multi for addLoops of G, V;
end;
registration
let G be Dsimple _Graph, V be set;
cluster -> non-Dmulti for addLoops of G, V;
end;
theorem :: GLIB_012:42
for G2 being _Graph, V being Subset of the_Vertices_of G2
for G1 being addLoops of G2, V, v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & v1 in V ex e being object
st e DJoins v1,v1,G1 & not e in the_Edges_of G2 &
v1.edgesIn() = v2.edgesIn()\/{e} & v1.edgesOut() = v2.edgesOut()\/{e} &
v1.edgesInOut() = v2.edgesInOut() \/ {e};
theorem :: GLIB_012:43
for G2 being _Graph, V being Subset of the_Vertices_of G2
for G1 being addLoops of G2, V, v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & v1 in V holds
v1.inDegree() = v2.inDegree() +` 1 & v1.outDegree() = v2.outDegree() +` 1 &
v1.degree() = v2.degree() +` 2;
theorem :: GLIB_012:44
for G2 being _Graph, V being Subset of the_Vertices_of G2
for G1 being addLoops of G2, V, v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & not v1 in V holds
v1.edgesIn() = v2.edgesIn() & v1.inDegree() = v2.inDegree() &
v1.edgesOut() = v2.edgesOut() & v1.outDegree() = v2.outDegree() &
v1.edgesInOut() = v2.edgesInOut() & v1.degree() = v2.degree();
begin :: Directed Graph Complement with Loops
definition
let G be _Graph;
mode DLGraphComplement of G -> non-Dmulti _Graph means
:: GLIB_012:def 6
the_Vertices_of it = the_Vertices_of G &
the_Edges_of it misses the_Edges_of G &
for v,w being Vertex of G holds
(ex e1 being object st e1 DJoins v,w,G) iff
(not ex e2 being object st e2 DJoins v,w,it);
end;
theorem :: GLIB_012:45
for G1, G2, G3 being _Graph, G4 being DLGraphComplement of G1
st G1 == G2 & G3 == G4 holds G3 is DLGraphComplement of G2;
registration
let G be _Graph;
cluster plain for DLGraphComplement of G;
end;
theorem :: GLIB_012:46
for G1 being _Graph, G2 being DLGraphComplement of G1, e1,e2,v,w being object
holds e1 DJoins v,w,G1 implies not e2 DJoins v,w,G2;
theorem :: GLIB_012:47
for G1 being _Graph, G2 being removeDParallelEdges of G1
for G3 being DLGraphComplement of G1
holds G3 is DLGraphComplement of G2;
theorem :: GLIB_012:48
for G1, G2 being _Graph
for G3 being removeDParallelEdges of G1, G4 being removeDParallelEdges of G2
for G5 being DLGraphComplement of G1, G6 being DLGraphComplement of G2
st G4 is G3-Disomorphic holds G6 is G5-Disomorphic;
theorem :: GLIB_012:49
for G1 being _Graph, G2 being G1-Disomorphic _Graph
for G3 being DLGraphComplement of G1, G4 being DLGraphComplement of G2
holds G4 is G3-Disomorphic;
theorem :: GLIB_012:50
for G1 being _Graph, G2, G3 being DLGraphComplement of G1
holds G3 is G2-Disomorphic;
theorem :: GLIB_012:51
for G1 being _Graph, G2 being reverseEdgeDirections of G1
for G3 being DLGraphComplement of G1, G4 being reverseEdgeDirections of G3
holds G4 is DLGraphComplement of G2;
theorem :: GLIB_012:52
for G1 being _Graph, V being non empty Subset of the_Vertices_of G1
for G2 being inducedSubgraph of G1, V
for G3 being DLGraphComplement of G1, G4 being inducedSubgraph of G3, V
holds G4 is DLGraphComplement of G2;
theorem :: GLIB_012:53
for G1 being _Graph, V being proper Subset of the_Vertices_of G1
for G2 being removeVertices of G1, V
for G3 being DLGraphComplement of G1, G4 being removeVertices of G3, V
holds G4 is DLGraphComplement of G2;
:: involutiveness of graph complement (DLC case)
theorem :: GLIB_012:54
for G1 being non-Dmulti _Graph, G2 being DLGraphComplement of G1
holds G1 is DLGraphComplement of G2;
theorem :: GLIB_012:55
for G1 being _Graph, G2 being DLGraphComplement of G1
holds G1.order() = G2.order();
theorem :: GLIB_012:56
for G1 being _Graph, G2 being DLGraphComplement of G1 holds
(G1 is _trivial iff G2 is _trivial) &
(G1 is loopfull iff G2 is loopless) &
(G1 is loopless iff G2 is loopfull);
registration
let G be _trivial _Graph;
cluster -> _trivial for DLGraphComplement of G;
end;
registration
let G be non _trivial _Graph;
cluster -> non _trivial for DLGraphComplement of G;
end;
registration
let G be loopfull _Graph;
cluster -> loopless for DLGraphComplement of G;
end;
registration
let G be non loopfull _Graph;
cluster -> non loopless for DLGraphComplement of G;
end;
registration
let G be loopless _Graph;
cluster -> loopfull for DLGraphComplement of G;
end;
registration
let G be non loopless _Graph;
cluster -> non loopfull for DLGraphComplement of G;
end;
theorem :: GLIB_012:57
for G1 being _Graph, G2 being DLGraphComplement of G1
st the_Edges_of G1 = G1.loops() holds G2 is complete;
registration
let G be edgeless _Graph;
cluster -> complete for DLGraphComplement of G;
end;
registration
let G be non connected _Graph;
cluster -> connected for DLGraphComplement of G;
end;
theorem :: GLIB_012:58
for G1 being _Graph, G2 being DLGraphComplement of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 holds
(v1 is isolated implies v2 is non isolated) &
(v1 is endvertex implies v2 is non endvertex);
theorem :: GLIB_012:59
for G1 being _Graph, G2 being DLGraphComplement of G1
for v,w being Vertex of G1 holds
(not ex e being object st e Joins v,w,G1) implies
(ex e being object st e Joins v,w,G2);
theorem :: GLIB_012:60
for G1 being _Graph, G2 being DLGraphComplement of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds
v2.inNeighbors() = the_Vertices_of G2 \ v1.inNeighbors() &
v2.outNeighbors() = the_Vertices_of G2 \ v1.outNeighbors();
theorem :: GLIB_012:61
for G1 being _Graph, G2 being DLGraphComplement of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & v1 is isolated holds
v2.inNeighbors() = the_Vertices_of G2 &
v2.outNeighbors() = the_Vertices_of G2 &
v2.allNeighbors() = the_Vertices_of G2;
begin :: Undirected Graph Complement with Loops
definition
let G be _Graph;
mode LGraphComplement of G -> non-multi _Graph means
:: GLIB_012:def 7
the_Vertices_of it = the_Vertices_of G &
the_Edges_of it misses the_Edges_of G &
for v,w being Vertex of G holds
(ex e1 being object st e1 Joins v,w,G) iff
(not ex e2 being object st e2 Joins v,w,it);
end;
theorem :: GLIB_012:62
for G1, G2, G3 being _Graph, G4 being LGraphComplement of G1
st G1 == G2 & G3 == G4 holds G3 is LGraphComplement of G2;
registration
let G be _Graph;
cluster plain for LGraphComplement of G;
end;
theorem :: GLIB_012:63
for G1 being _Graph, G2 being non-multi _Graph
holds G2 is LGraphComplement of G1 iff
the_Vertices_of G2 = the_Vertices_of G1 &
the_Edges_of G2 misses the_Edges_of G1 &
for v1,w1 being Vertex of G1, v2,w2 being Vertex of G2 st v1 = v2 & w1 = w2
holds v1,w1 are_adjacent iff not v2,w2 are_adjacent;
theorem :: GLIB_012:64
for G1 being _Graph, G2 being LGraphComplement of G1, e1,e2,v,w being object
holds e1 Joins v,w,G1 implies not e2 Joins v,w,G2;
theorem :: GLIB_012:65
for G1 being _Graph, G2 being removeParallelEdges of G1
for G3 being LGraphComplement of G1
holds G3 is LGraphComplement of G2;
theorem :: GLIB_012:66
for G1, G2 being _Graph
for G3 being removeParallelEdges of G1, G4 being removeParallelEdges of G2
for G5 being LGraphComplement of G1, G6 being LGraphComplement of G2
st G4 is G3-isomorphic holds G6 is G5-isomorphic;
theorem :: GLIB_012:67
for G1 being _Graph, G2 being G1-isomorphic _Graph
for G3 being LGraphComplement of G1, G4 being LGraphComplement of G2
holds G4 is G3-isomorphic;
theorem :: GLIB_012:68
for G1 being _Graph, G2, G3 being LGraphComplement of G1
holds G3 is G2-isomorphic;
theorem :: GLIB_012:69
for G1 being _Graph, V being non empty Subset of the_Vertices_of G1
for G2 being inducedSubgraph of G1, V
for G3 being LGraphComplement of G1, G4 being inducedSubgraph of G3, V
holds G4 is LGraphComplement of G2;
theorem :: GLIB_012:70
for G1 being _Graph, V being proper Subset of the_Vertices_of G1
for G2 being removeVertices of G1, V
for G3 being LGraphComplement of G1, G4 being removeVertices of G3, V
holds G4 is LGraphComplement of G2;
:: involutiveness of graph complement (LC case)
theorem :: GLIB_012:71
for G1 being non-multi _Graph, G2 being LGraphComplement of G1
holds G1 is LGraphComplement of G2;
theorem :: GLIB_012:72
for G1 being _Graph, G2 being LGraphComplement of G1
holds G1.order() = G2.order();
theorem :: GLIB_012:73
for G1 being _Graph, G2 being LGraphComplement of G1 holds
(G1 is _trivial iff G2 is _trivial) &
(G1 is loopfull iff G2 is loopless) &
(G1 is loopless iff G2 is loopfull);
registration
let G be _trivial _Graph;
cluster -> _trivial for LGraphComplement of G;
end;
registration
let G be non _trivial _Graph;
cluster -> non _trivial for LGraphComplement of G;
end;
registration
let G be loopfull _Graph;
cluster -> loopless for LGraphComplement of G;
end;
registration
let G be non loopfull _Graph;
cluster -> non loopless for LGraphComplement of G;
end;
registration
let G be loopless _Graph;
cluster -> loopfull for LGraphComplement of G;
end;
registration
let G be non loopless _Graph;
cluster -> non loopfull for LGraphComplement of G;
end;
theorem :: GLIB_012:74
for G1 being _Graph, G2 being LGraphComplement of G1
st the_Edges_of G1 = G1.loops() holds G2 is complete;
registration
let G be edgeless _Graph;
cluster -> complete for LGraphComplement of G;
end;
theorem :: GLIB_012:75
for G1 being complete _Graph, G2 being LGraphComplement of G1
holds the_Edges_of G2 = G2.loops();
registration
let G be complete loopfull _Graph;
cluster -> edgeless for LGraphComplement of G;
end;
registration
let G be non connected _Graph;
cluster -> connected for LGraphComplement of G;
end;
theorem :: GLIB_012:76
for G1 being _Graph, G2 being LGraphComplement of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 holds
(v1 is isolated implies v2 is non isolated) &
(v1 is endvertex implies v2 is non endvertex);
theorem :: GLIB_012:77
for G1 being _Graph, G2 being LGraphComplement of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds v2.allNeighbors() = the_Vertices_of G2 \ v1.allNeighbors();
theorem :: GLIB_012:78
for G1 being _Graph, G2 being LGraphComplement of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & v1 is isolated
holds v2.allNeighbors() = the_Vertices_of G2;
begin :: Directed Graph Complement without Loops
definition
let G be _Graph;
mode DGraphComplement of G -> Dsimple _Graph means
:: GLIB_012:def 8
ex G9 being DLGraphComplement of G st it is removeLoops of G9;
end;
theorem :: GLIB_012:79
for G1, G2, G3 being _Graph, G4 being DGraphComplement of G1
st G1 == G2 & G3 == G4 holds G3 is DGraphComplement of G2;
registration
let G be _Graph;
cluster plain for DGraphComplement of G;
end;
theorem :: GLIB_012:80
for G1 being _Graph, G2 being Dsimple _Graph
holds G2 is DGraphComplement of G1 iff
the_Vertices_of G2 = the_Vertices_of G1 &
the_Edges_of G2 misses the_Edges_of G1 &
for v,w being Vertex of G1 st v <> w holds
(ex e1 being object st e1 DJoins v,w,G1) iff
(not ex e2 being object st e2 DJoins v,w,G2);
theorem :: GLIB_012:81
for G1 being _Graph, G2 being DGraphComplement of G1, e1,e2,v,w being object
holds e1 DJoins v,w,G1 implies not e2 DJoins v,w,G2;
theorem :: GLIB_012:82
for G1 being _Graph, G2 being DSimpleGraph of G1
for G3 being DGraphComplement of G1
holds G3 is DGraphComplement of G2;
theorem :: GLIB_012:83
for G1, G2 being _Graph
for G3 being DSimpleGraph of G1, G4 being DSimpleGraph of G2
for G5 being DGraphComplement of G1, G6 being DGraphComplement of G2
st G4 is G3-Disomorphic holds G6 is G5-Disomorphic;
theorem :: GLIB_012:84
for G1 being _Graph, G2 being G1-Disomorphic _Graph
for G3 being DGraphComplement of G1, G4 being DGraphComplement of G2
holds G4 is G3-Disomorphic;
theorem :: GLIB_012:85
for G1 being _Graph, G2, G3 being DGraphComplement of G1
holds G3 is G2-Disomorphic;
theorem :: GLIB_012:86
for G1 being _Graph, G2 being reverseEdgeDirections of G1
for G3 being DGraphComplement of G1, G4 being reverseEdgeDirections of G3
holds G4 is DGraphComplement of G2;
theorem :: GLIB_012:87
for G1 being _Graph, V being non empty Subset of the_Vertices_of G1
for G2 being inducedSubgraph of G1, V
for G3 being DGraphComplement of G1, G4 being inducedSubgraph of G3, V
holds G4 is DGraphComplement of G2;
theorem :: GLIB_012:88
for G1 being _Graph, V being proper Subset of the_Vertices_of G1
for G2 being removeVertices of G1, V
for G3 being DGraphComplement of G1, G4 being removeVertices of G3, V
holds G4 is DGraphComplement of G2;
:: involutiveness of graph complement (DC case)
theorem :: GLIB_012:89
for G1 being Dsimple _Graph, G2 being DGraphComplement of G1
holds G1 is DGraphComplement of G2;
theorem :: GLIB_012:90
for G1 being _Graph, G2 being DGraphComplement of G1
holds G1.order() = G2.order();
theorem :: GLIB_012:91
for G1 being _Graph, G2 being DGraphComplement of G1
holds G1 is _trivial iff G2 is _trivial;
registration
let G be _trivial _Graph;
cluster -> _trivial for DGraphComplement of G;
end;
registration
let G be non _trivial _Graph;
cluster -> non _trivial for DGraphComplement of G;
end;
theorem :: GLIB_012:92
for G1 being _Graph, G2 being DGraphComplement of G1
st the_Edges_of G1 = G1.loops() holds G2 is complete;
registration
let G be edgeless _Graph;
cluster -> complete for DGraphComplement of G;
end;
registration
let G be _trivial edgeless _Graph;
cluster -> edgeless for DGraphComplement of G;
end;
registration
let G be non connected _Graph;
cluster -> connected for DGraphComplement of G;
end;
theorem :: GLIB_012:93
for G1 being non _trivial _Graph, G2 being DGraphComplement of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds v1 is isolated implies v2 is non isolated;
theorem :: GLIB_012:94
for G1 being _Graph, G2 being DGraphComplement of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & 3 c= G1.order()
holds v1 is endvertex implies v2 is non endvertex;
theorem :: GLIB_012:95
for G1 being _Graph, G2 being DGraphComplement of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds
v2.inNeighbors() = the_Vertices_of G2 \ (v1.inNeighbors() \/ {v2}) &
v2.outNeighbors() = the_Vertices_of G2 \ (v1.outNeighbors() \/ {v2});
theorem :: GLIB_012:96
for G1 being _Graph, G2 being DGraphComplement of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & v1 is isolated holds
v2.inNeighbors() = the_Vertices_of G2 \ {v2} &
v2.outNeighbors() = the_Vertices_of G2 \ {v2} &
v2.allNeighbors() = the_Vertices_of G2 \ {v2};
begin :: Undirected Graph Complement without Loops
definition
let G be _Graph;
mode GraphComplement of G -> simple _Graph means
:: GLIB_012:def 9
ex G9 being LGraphComplement of G st it is removeLoops of G9;
end;
theorem :: GLIB_012:97
for G1, G2, G3 being _Graph, G4 being GraphComplement of G1
st G1 == G2 & G3 == G4 holds G3 is GraphComplement of G2;
registration
let G be _Graph;
cluster plain for GraphComplement of G;
end;
theorem :: GLIB_012:98
for G1 being _Graph, G2 being simple _Graph
holds G2 is GraphComplement of G1 iff
the_Vertices_of G2 = the_Vertices_of G1 &
the_Edges_of G2 misses the_Edges_of G1 &
for v,w being Vertex of G1 st v <> w holds
(ex e1 being object st e1 Joins v,w,G1) iff
(not ex e2 being object st e2 Joins v,w,G2);
theorem :: GLIB_012:99
for G1 being _Graph, G2 being simple _Graph
holds G2 is GraphComplement of G1 iff
the_Vertices_of G2 = the_Vertices_of G1 &
the_Edges_of G2 misses the_Edges_of G1 &
for v1,w1 being Vertex of G1, v2,w2 being Vertex of G2
st v1 = v2 & w1 = w2 & v1 <> w1
holds v1,w1 are_adjacent iff not v2,w2 are_adjacent;
theorem :: GLIB_012:100
for G1 being _Graph, G2 being GraphComplement of G1, e1,e2,v,w being object
holds e1 Joins v,w,G1 implies not e2 Joins v,w,G2;
theorem :: GLIB_012:101
for G1 being _Graph, G2 being SimpleGraph of G1
for G3 being GraphComplement of G1 holds G3 is GraphComplement of G2;
theorem :: GLIB_012:102
for G1, G2 being _Graph
for G3 being SimpleGraph of G1, G4 being SimpleGraph of G2
for G5 being GraphComplement of G1, G6 being GraphComplement of G2
st G4 is G3-isomorphic holds G6 is G5-isomorphic;
theorem :: GLIB_012:103
for G1 being _Graph, G2 being G1-isomorphic _Graph
for G3 being GraphComplement of G1, G4 being GraphComplement of G2
holds G4 is G3-isomorphic;
theorem :: GLIB_012:104
for G1 being _Graph, G2, G3 being GraphComplement of G1
holds G3 is G2-isomorphic;
theorem :: GLIB_012:105
for G1 being _Graph, v being object, V being Subset of the_Vertices_of G1
for G2 being addAdjVertexAll of G1,v,V
for G3 being GraphComplement of G1
st not v in the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G3
ex G4 being addAdjVertexAll of G3,v,the_Vertices_of G1 \ V
st G4 is GraphComplement of G2;
theorem :: GLIB_012:106
for G1 being _Graph, v being object, G2 being addVertex of G1,v
for G3 being GraphComplement of G1 st not v in the_Vertices_of G1
ex G4 being addAdjVertexAll of G3,v st G4 is GraphComplement of G2;
theorem :: GLIB_012:107
for G1 being _Graph, v being object, G2 being addAdjVertexAll of G1,v
for G3 being GraphComplement of G1, G4 being addVertex of G3,v
st not v in the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G3
holds G4 is GraphComplement of G2;
theorem :: GLIB_012:108
for G1 being _Graph, V being non empty Subset of the_Vertices_of G1
for G2 being inducedSubgraph of G1, V
for G3 being GraphComplement of G1, G4 being inducedSubgraph of G3, V
holds G4 is GraphComplement of G2;
theorem :: GLIB_012:109
for G1 being _Graph, V being proper Subset of the_Vertices_of G1
for G2 being removeVertices of G1, V
for G3 being GraphComplement of G1, G4 being removeVertices of G3, V
holds G4 is GraphComplement of G2;
:: involutiveness of graph complement (C case)
theorem :: GLIB_012:110
for G1 being simple _Graph, G2 being GraphComplement of G1
holds G1 is GraphComplement of G2;
theorem :: GLIB_012:111
for G1 being _Graph, G2 being GraphComplement of G1
holds G1.order() = G2.order();
theorem :: GLIB_012:112
for G1 being _Graph, G2 being GraphComplement of G1 holds
(G1 is _trivial iff G2 is _trivial);
registration
let G be _trivial _Graph;
cluster -> _trivial for GraphComplement of G;
end;
registration
let G be non _trivial _Graph;
cluster -> non _trivial for GraphComplement of G;
end;
theorem :: GLIB_012:113
for G1 being _Graph, G2 being GraphComplement of G1 holds
(G1 is complete iff G2 is edgeless) &
(the_Edges_of G1 = G1.loops() iff G2 is complete);
registration
let G be complete _Graph;
cluster -> edgeless for GraphComplement of G;
end;
registration
let G be non complete _Graph;
cluster -> non edgeless for GraphComplement of G;
end;
registration
let G be edgeless _Graph;
cluster -> complete for GraphComplement of G;
end;
registration
let G be non connected _Graph;
cluster -> connected for GraphComplement of G;
end;
theorem :: GLIB_012:114
for G1 being non _trivial _Graph, G2 being GraphComplement of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds v1 is isolated implies v2 is non isolated;
theorem :: GLIB_012:115
for G1 being _Graph, G2 being GraphComplement of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & G1.order() = 2 holds
(v1 is endvertex implies v2 is isolated) &
(v1 is isolated implies v2 is endvertex);
theorem :: GLIB_012:116
for G1 being simple _Graph, G2 being GraphComplement of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & G1.order() = 2 holds
(v1 is endvertex iff v2 is isolated) &
(v1 is isolated iff v2 is endvertex);
:: in case G.order() = 3 we have the endvertices of P3 with complement K2+K1
theorem :: GLIB_012:117
for G1 being _Graph, G2 being GraphComplement of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & 4 c= G1.order()
holds v1 is endvertex implies v2 is non endvertex;
theorem :: GLIB_012:118
for G1 being _Graph, G2 being GraphComplement of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds v2.allNeighbors() = the_Vertices_of G2 \ (v1.allNeighbors() \/ {v2});
theorem :: GLIB_012:119
for G1 being _Graph, G2 being GraphComplement of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & v1 is isolated
holds v2.allNeighbors() = the_Vertices_of G2 \ {v2};
begin :: Self-complementary Graphs
definition
let G be _Graph;
attr G is self-DLcomplementary means
:: GLIB_012:def 10
for H being DLGraphComplement of G holds H is G-Disomorphic;
attr G is self-Lcomplementary means
:: GLIB_012:def 11
for H being LGraphComplement of G holds H is G-isomorphic;
attr G is self-Dcomplementary means
:: GLIB_012:def 12
for H being DGraphComplement of G holds H is G-Disomorphic;
attr G is self-complementary means
:: GLIB_012:def 13
for H being GraphComplement of G holds H is G-isomorphic;
end;
theorem :: GLIB_012:120
for G being _Graph holds G is self-DLcomplementary iff
ex H being DLGraphComplement of G st H is G-Disomorphic;
theorem :: GLIB_012:121
for G being _Graph holds G is self-Lcomplementary iff
ex H being LGraphComplement of G st H is G-isomorphic;
theorem :: GLIB_012:122
for G being _Graph holds G is self-Dcomplementary iff
ex H being DGraphComplement of G st H is G-Disomorphic;
theorem :: GLIB_012:123
for G being _Graph holds G is self-complementary iff
ex H being GraphComplement of G st H is G-isomorphic;
registration
cluster self-DLcomplementary -> non loopless non loopfull non-Dmulti
connected for _Graph;
cluster self-Lcomplementary -> non loopless non loopfull non-multi
connected for _Graph;
cluster self-Dcomplementary -> Dsimple connected for _Graph;
cluster self-complementary -> simple connected for _Graph;
end;
:: K2 with an added loop is self-DLcomplementary and
:: P4 with loops at the endvertices or the other two vertices
:: is self-Lcomplementary, but both won't be clustered here
:: hence no existence cluster for the attributes here
registration
cluster _trivial edgeless -> self-Dcomplementary self-complementary
for _Graph;
cluster self-Dcomplementary self-complementary -> _trivial edgeless
for _Graph;
cluster self-DLcomplementary -> non _trivial non self-Lcomplementary
non self-Dcomplementary non self-complementary for _Graph;
cluster self-Lcomplementary -> non _trivial non self-DLcomplementary
non self-Dcomplementary non self-complementary for _Graph;
end;
registration
cluster self-Dcomplementary self-complementary for _Graph;
end;