:: About Graph Complements
:: by Sebastian Koch
::
:: Received December 30, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users

definition

let G be _Graph;

attr G is loopfull means :Def1: :: GLIB_012:def 1
for v being Vertex of G ex e being object st e Joins v,v,G;

end;

:: deftheorem Def1 defines loopfull GLIB_012:def 1 :
for G being _Graph holds
( G is loopfull iff for v being Vertex of G ex e being object st e Joins v,v,G );

theorem Th1: :: 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 )

proof end;

theorem :: GLIB_012:2

for G being _Graph holds
( G is loopfull iff for v being Vertex of G holds v,v are_adjacent )

proof end;

registration

cluster Relation-like NAT -defined Function-like finite [Graph-like] loopfull -> non loopless for set ;

coherence
for b₁ being _Graph st b₁ is loopfull holds
not b₁ is loopless

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] non loopless _trivial -> loopfull for set ;

coherence
for b₁ being _Graph st b₁ is _trivial & not b₁ is loopless holds
b₁ is loopfull

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] complete loopfull for set ;

existence
ex b₁ being _Graph st
( b₁ is loopfull & b₁ is complete )

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] non loopfull for set ;

existence
not for b₁ being _Graph holds b₁ is loopfull

proof end;

end;

theorem Th3: :: GLIB_012:3

for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E holds
( G1 is loopfull iff G2 is loopfull )

proof end;

registration

let G be loopfull _Graph;
let E be set ;

cluster -> loopfull for reverseEdgeDirections of G,E;

coherence
for b₁ being reverseEdgeDirections of G,E holds b₁ is loopfull by Th3;

end;

registration

let G be non loopfull _Graph;
let E be set ;

cluster -> non loopfull for reverseEdgeDirections of G,E;

coherence
for b₁ being reverseEdgeDirections of G,E holds not b₁ is loopfull by Th3;

end;

theorem Th4: :: GLIB_012:4

for G1, G2 being _Graph st G1 == G2 & G1 is loopfull holds
G2 is loopfull

proof end;

theorem Th5: :: GLIB_012:5

for G2 being loopfull _Graph
for G1 being Supergraph of G2 st the_Vertices_of G1 = the_Vertices_of G2 holds
G1 is loopfull

proof end;

theorem Th6: :: GLIB_012:6

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st rng (F _V) = the_Vertices_of G2 & G1 .loops() c= dom (F _E) & G1 is loopfull holds
G2 is loopfull

proof end;

theorem Th7: :: GLIB_012:7

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is total & F is onto & G1 is loopfull holds
G2 is loopfull

proof end;

theorem Th8: :: GLIB_012:8

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is semi-continuous & dom (F _V) = the_Vertices_of G1 & G2 .loops() c= rng (F _E) & G2 is loopfull holds
G1 is loopfull

proof end;

theorem Th9: :: GLIB_012:9

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is total & F is onto & F is semi-continuous & G2 is loopfull holds
G1 is loopfull

proof end;

theorem :: GLIB_012:10

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
( G1 is loopfull iff G2 is loopfull ) by Th7, Th9;

registration

let G be loopfull _Graph;
let V be set ;

cluster -> loopfull for inducedSubgraph of G,V,G .edgesBetween V;

coherence
for b₁ being inducedSubgraph of G,V holds b₁ is loopfull

proof end;

cluster -> loopfull for inducedSubgraph of G,(the_Vertices_of G) \ V,G .edgesBetween ((the_Vertices_of G) \ V);

coherence
for b₁ being removeVertices of G,V holds b₁ is loopfull ;

cluster -> loopfull for inducedSubgraph of G,(the_Vertices_of G) \ {V},G .edgesBetween ((the_Vertices_of G) \ {V});

coherence
for b₁ being removeVertex of G,V holds b₁ is loopfull ;

end;

registration

let G be non loopfull _Graph;

cluster spanning -> spanning non loopfull for Subgraph of G;

coherence
for b₁ being spanning Subgraph of G holds not b₁ is loopfull

proof end;

let E be set ;

cluster -> non loopfull for inducedSubgraph of G, the_Vertices_of G,E;

coherence
for b₁ being inducedSubgraph of G, the_Vertices_of G,E holds not b₁ is loopfull

proof end;

cluster -> non loopfull for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ E;

coherence
for b₁ being removeEdges of G,E holds not b₁ is loopfull ;

cluster -> non loopfull for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ {E};

coherence
for b₁ being removeEdge of G,E holds not b₁ is loopfull ;

end;

theorem Th11: :: GLIB_012:11

for G2 being _Graph
for V being set
for G1 being addVertices of G2,V st V \ (the_Vertices_of G2) <> {} holds
not G1 is loopfull

proof end;

registration

let G be non loopfull _Graph;
let V be set ;

cluster -> non loopfull for addVertices of G,V;

coherence
for b₁ being addVertices of G,V holds not b₁ is loopfull

proof end;

end;

registration

let G be loopfull _Graph;
let v, e, w be object ;

cluster -> loopfull for addEdge of G,v,e,w;

coherence
for b₁ being addEdge of G,v,e,w holds b₁ is loopfull

proof end;

end;

theorem Th12: :: GLIB_012:12

for G2 being _Graph
for v being Vertex of G2
for 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
not G1 is loopfull

proof end;

theorem Th13: :: GLIB_012:13

for G2 being _Graph
for v, e being object
for 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
not G1 is loopfull

proof end;

registration

let G be non loopfull _Graph;
let v, e, w be object ;

cluster -> non loopfull for addAdjVertex of G,v,e,w;

coherence
for b₁ being addAdjVertex of G,v,e,w holds not b₁ is loopfull

proof end;

end;

theorem Th14: :: GLIB_012:14

for G2 being _Graph
for v being object
for 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
not G1 is loopfull

proof end;

registration

let G be non loopfull _Graph;
let v be object ;
let V be set ;

cluster -> non loopfull for addAdjVertexAll of G,v,V;

coherence
for b₁ being addAdjVertexAll of G,v,V holds not b₁ is loopfull

proof end;

end;

registration

let G be loopfull _Graph;

cluster -> loopfull for removeParallelEdges of G;

coherence
for b₁ being removeParallelEdges of G holds b₁ is loopfull

proof end;

cluster -> loopfull for removeDParallelEdges of G;

coherence
for b₁ being removeDParallelEdges of G holds b₁ is loopfull

proof end;

end;

:: removeLoops is loopless, hence non loopfull

registration

let G be non loopfull _Graph;

cluster -> non loopfull for removeParallelEdges of G;

coherence
for b₁ being removeParallelEdges of G holds not b₁ is loopfull ;

cluster -> non loopfull for removeDParallelEdges of G;

coherence
for b₁ being removeDParallelEdges of G holds not b₁ is loopfull ;

end;

definition

let GF be Graph-yielding Function;

attr GF is loopfull means :Def2: :: GLIB_012:def 2
for x being object st x in dom GF holds
ex G being _Graph st
( GF . x = G & G is loopfull );

end;

:: deftheorem Def2 defines loopfull GLIB_012:def 2 :
for GF being Graph-yielding Function holds
( GF is loopfull iff for x being object st x in dom GF holds
ex G being _Graph st
( GF . x = G & G is loopfull ) );

registration

let G be loopfull _Graph;

cluster <*G*> -> loopfull ;

coherence
<*G*> is loopfull

proof end;

cluster NAT --> G -> loopfull ;

coherence
NAT --> G is loopfull by FUNCOP_1:7;

end;

definition

let GF be non empty Graph-yielding Function;

redefine attr GF is loopfull means :Def3: :: GLIB_012:def 3
for x being Element of dom GF holds GF . x is loopfull ;

compatibility
( GF is loopfull iff for x being Element of dom GF holds GF . x is loopfull )

proof end;

end;

:: deftheorem Def3 defines loopfull GLIB_012:def 3 :
for GF being non empty Graph-yielding Function holds
( GF is loopfull iff for x being Element of dom GF holds GF . x is loopfull );

Lm1: for F being ManySortedSet of NAT
for n being object holds
( n is Nat iff n in dom F )

proof end;

definition

let GSq be GraphSeq;

redefine attr GSq is loopfull means :Def4: :: GLIB_012:def 4
for n being Nat holds GSq . n is loopfull ;

compatibility
( GSq is loopfull iff for n being Nat holds GSq . n is loopfull )

proof end;

end;

:: deftheorem Def4 defines loopfull GLIB_012:def 4 :
for GSq being GraphSeq holds
( GSq is loopfull iff for n being Nat holds GSq . n is loopfull );

registration

cluster empty Relation-like Function-like Graph-yielding -> Graph-yielding loopfull for set ;

coherence
for b₁ being Graph-yielding Function st b₁ is empty holds
b₁ is loopfull ;

cluster non empty Relation-like Function-like Graph-yielding loopfull -> Graph-yielding non loopless for set ;

coherence
for b₁ being Graph-yielding Function st not b₁ is empty & b₁ is loopfull holds
not b₁ is loopless

proof end;

end;

registration

cluster non empty Relation-like NAT -defined Function-like total Graph-yielding loopfull for set ;

existence
ex b₁ being GraphSeq st b₁ is loopfull

proof end;

cluster non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Graph-yielding loopfull for set ;

existence
ex b₁ being Graph-yielding FinSequence st
( not b₁ is empty & b₁ is loopfull )

proof end;

end;

registration

let GF be non empty Graph-yielding loopfull Function;
let x be Element of dom GF;

cluster GF . x -> loopfull ;

coherence
GF . x is loopfull by Def3;

end;

registration

let GSq be loopfull GraphSeq;
let x be Nat;

cluster GSq . x -> loopfull ;

coherence
GSq . x is loopfull by Def4;

end;

registration

let p be Graph-yielding loopfull FinSequence;
let n be Nat;

cluster p | n -> loopfull ;

coherence
p | n is loopfull

proof end;

cluster p /^ n -> loopfull ;

coherence
p /^ n is loopfull

proof end;

let m be Nat;

cluster smid (p,m,n) -> loopfull ;

coherence
smid (p,m,n) is loopfull

proof end;

cluster (m,n) -cut p -> loopfull ;

coherence
(m,n) -cut p is loopfull

proof end;

end;

registration

let p, q be Graph-yielding loopfull FinSequence;

cluster p ^ q -> loopfull ;

coherence
p ^ q is loopfull

proof end;

cluster p ^' q -> loopfull ;

coherence
p ^' q is loopfull

proof end;

end;

registration

let G1, G2 be loopfull _Graph;

cluster <*G1,G2*> -> loopfull ;

coherence
<*G1,G2*> is loopfull

proof end;

let G3 be loopfull _Graph;

cluster <*G1,G2,G3*> -> loopfull ;

coherence
<*G1,G2,G3*> is loopfull

proof end;

end;

:: a loop is added to each vertex in V, regardless if that
:: vertex has a loop already or not

definition

let G be _Graph;
let V be set ;

mode addLoops of G,V -> Supergraph of G means :Def5: :: GLIB_012:def 5
( the_Vertices_of it = the_Vertices_of G & ex E being set ex 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;

existence
( ( V c= the_Vertices_of G implies ex b₁ being Supergraph of G st
( the_Vertices_of b₁ = the_Vertices_of G & ex E being set ex f being one-to-one Function st
( E misses the_Edges_of G & the_Edges_of b₁ = (the_Edges_of G) \/ E & dom f = E & rng f = V & the_Source_of b₁ = (the_Source_of G) +* f & the_Target_of b₁ = (the_Target_of G) +* f ) ) ) & ( not V c= the_Vertices_of G implies ex b₁ being Supergraph of G st b₁ == G ) )

proof end;

consistency
for b₁ being Supergraph of G holds verum ;

end;

:: deftheorem Def5 defines addLoops GLIB_012:def 5 :
for G being _Graph
for V being set
for b₃ being Supergraph of G holds
( ( V c= the_Vertices_of G implies ( b₃ is addLoops of G,V iff ( the_Vertices_of b₃ = the_Vertices_of G & ex E being set ex f being one-to-one Function st
( E misses the_Edges_of G & the_Edges_of b₃ = (the_Edges_of G) \/ E & dom f = E & rng f = V & the_Source_of b₃ = (the_Source_of G) +* f & the_Target_of b₃ = (the_Target_of G) +* f ) ) ) ) & ( not V c= the_Vertices_of G implies ( b₃ is addLoops of G,V iff b₃ == G ) ) );

definition

let G be _Graph;
mode addLoops of G is addLoops of G, the_Vertices_of G;

end;

theorem Th15: :: GLIB_012:15

for G2 being _Graph
for V being set
for G1 being addLoops of G2,V holds the_Vertices_of G1 = the_Vertices_of G2

proof end;

theorem Th16: :: GLIB_012:16

for G2 being _Graph
for V being set
for 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 )

proof end;

theorem Th17: :: GLIB_012:17

for G2 being _Graph
for V being set
for 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 )

proof end;

theorem :: GLIB_012:18

for G2 being _Graph
for 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

proof end;

theorem :: GLIB_012:19

for G2 being _Graph
for V being set
for G1 being addLoops of G2,V holds G1 .order() = G2 .order() by Th15;

theorem :: GLIB_012:20

for G2 being _Graph
for V being Subset of (the_Vertices_of G2)
for G1 being addLoops of G2,V holds G1 .size() = (G2 .size()) +` (card V)

proof end;

theorem Th21: :: GLIB_012:21

for G1, G2 being _Graph holds
( G1 is addLoops of G2, {} iff G1 == G2 )

proof end;

theorem :: GLIB_012:22

for G being _Graph holds G is addLoops of G, {}

proof end;

theorem :: GLIB_012:23

for G being _Graph
for V1, V2 being Subset of (the_Vertices_of G)
for G1 being addLoops of G,V1
for G2 being addLoops of G1,V2 st V1 misses V2 holds
G2 is addLoops of G,V1 \/ V2

proof end;

theorem Th24: :: GLIB_012:24

for G3 being _Graph
for V1, V2 being Subset of (the_Vertices_of G3)
for G1 being addLoops of G3,V1 \/ V2 st V1 misses V2 holds
ex G2 being addLoops of G3,V1 st G1 is addLoops of G2,V2

proof end;

theorem Th25: :: GLIB_012:25

for G2 being loopless _Graph
for 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()) )

proof end;

theorem Th26: :: GLIB_012:26

for G1 being loopless _Graph
for V being set
for G2 being addLoops of G1,V
for G3 being removeLoops of G2 holds G1 == G3

proof end;

theorem Th27: :: GLIB_012:27

for G1, G2 being _Graph
for 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 ) )

proof end;

Lm2: for p being non empty FinSequence
for x being object
for n being Element of dom (p ^ <*x*>) holds
( not n <= (len (p ^ <*x*>)) - 1 or n = (len (p ^ <*x*>)) - 1 or n <= (len p) - 1 )

proof end;

:: finite addition of loops can be finitely constructed with one loop at a time

theorem :: GLIB_012:28

for G2 being _Graph
for 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 ex 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) ) ) )

proof end;

theorem Th29: :: GLIB_012:29

for G3, G4 being _Graph
for V1, V2 being set
for G1 being addLoops of G3,V1
for 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 holds
ex F being PGraphMapping of G1,G2 st
( F _V = F0 _V & (F _E) | (dom (F0 _E)) = F0 _E & ( not F0 is empty implies not F is 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 ) )

proof end;

theorem :: GLIB_012:30

for G3 being _Graph
for G4 being b₁ -isomorphic _Graph
for G1 being addLoops of G3
for G2 being addLoops of G4 holds G2 is G1 -isomorphic

proof end;

theorem :: GLIB_012:31

for G3 being _Graph
for G4 being b₁ -Disomorphic _Graph
for G1 being addLoops of G3
for G2 being addLoops of G4 holds G2 is G1 -Disomorphic

proof end;

theorem :: GLIB_012:32

for G3, G4 being _Graph
for V being set
for G1 being addLoops of G3,V
for G2 being addLoops of G4,V st G3 == G4 holds
G2 is G1 -Disomorphic

proof end;

theorem :: GLIB_012:33

for G3 being _Graph
for V, E being set
for G4 being reverseEdgeDirections of G3,E
for G1 being addLoops of G3,V
for G2 being addLoops of G4,V holds G2 is G1 -isomorphic

proof end;

theorem :: GLIB_012:34

for G3 being _Graph
for E, V being set
for G4 being reverseEdgeDirections of G3,E
for G1 being addLoops of G3,V
for G2 being reverseEdgeDirections of G1,E st E c= the_Edges_of G3 holds
G2 is addLoops of G4,V

proof end;

theorem :: GLIB_012:35

for G3 being _Graph
for 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
for G2 being inducedSubgraph of G1,V2 holds G2 is addLoops of G4,V1 /\ V2

proof end;

theorem :: GLIB_012:36

for G2 being _Graph
for V being set
for G1 being addLoops of G2,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st not v1 in V & v1 = v2 holds
( ( v1 is isolated implies v2 is isolated ) & ( v2 is isolated implies v1 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v2 is endvertex implies v1 is endvertex ) )

proof end;

theorem Th37: :: GLIB_012:37

for G2 being _Graph
for V being set
for 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) ) )

proof end;

theorem :: GLIB_012:38

for G2 being _Graph
for V being set
for 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

proof end;

registration

let G be _Graph;

cluster -> loopfull for addLoops of G, the_Vertices_of G;

coherence
for b₁ being addLoops of G holds b₁ is loopfull

proof end;

let V be non empty Subset of (the_Vertices_of G);

cluster -> non loopless for addLoops of G,V;

coherence
for b₁ being addLoops of G,V holds not b₁ is loopless

proof end;

end;

theorem Th39: :: GLIB_012:39

for G2 being _Graph
for V being set
for G1 being addLoops of G2,V holds
( G1 is _finite iff G2 is _finite )

proof end;

registration

let G be _finite _Graph;
let V be set ;

cluster -> _finite for addLoops of G,V;

coherence
for b₁ being addLoops of G,V holds b₁ is _finite by Th39;

end;

registration

let G be non _finite _Graph;
let V be set ;

cluster -> non _finite for addLoops of G,V;

coherence
for b₁ being addLoops of G,V holds not b₁ is _finite ;

end;

theorem Th40: :: GLIB_012:40

for G2 being _Graph
for V being set
for G1 being addLoops of G2,V holds
( G1 is connected iff G2 is connected )

proof end;

registration

let G be connected _Graph;
let V be set ;

cluster -> connected for addLoops of G,V;

coherence
for b₁ being addLoops of G,V holds b₁ is connected by Th40;

end;

registration

let G be non connected _Graph;
let V be set ;

cluster -> non connected for addLoops of G,V;

coherence
for b₁ being addLoops of G,V holds not b₁ is connected by Th40;

end;

theorem Th41: :: GLIB_012:41

for G2 being _Graph
for V being set
for G1 being addLoops of G2,V holds
( G1 is chordal iff G2 is chordal )

proof end;

registration

let G be chordal _Graph;
let V be set ;

cluster -> chordal for addLoops of G,V;

coherence
for b₁ being addLoops of G,V holds b₁ is chordal by Th41;

end;

:: non chordal clustering will be done later

registration

let G be non edgeless _Graph;
let V be set ;

cluster -> non edgeless for addLoops of G,V;

coherence
for b₁ being addLoops of G,V holds not b₁ is edgeless ;

end;

registration

let G be loopfull _Graph;
let V be set ;

cluster -> loopfull for addLoops of G,V;

coherence
for b₁ being addLoops of G,V holds b₁ is loopfull

proof end;

end;

registration

let G be simple _Graph;
let V be set ;

cluster -> non-multi for addLoops of G,V;

coherence
for b₁ being addLoops of G,V holds b₁ is non-multi

proof end;

end;

registration

let G be Dsimple _Graph;
let V be set ;

cluster -> non-Dmulti for addLoops of G,V;

coherence
for b₁ being addLoops of G,V holds b₁ is non-Dmulti

proof end;

end;

theorem Th42: :: GLIB_012:42

for G2 being _Graph
for V being Subset of (the_Vertices_of G2)
for G1 being addLoops of G2,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 in V holds
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} )

proof end;

theorem :: GLIB_012:43

for G2 being _Graph
for V being Subset of (the_Vertices_of G2)
for G1 being addLoops of G2,V
for v1 being Vertex of G1
for 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 )

proof end;

theorem :: GLIB_012:44

for G2 being _Graph
for V being Subset of (the_Vertices_of G2)
for G1 being addLoops of G2,V
for v1 being Vertex of G1
for 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() )

proof end;

definition

let G be _Graph;

mode DLGraphComplement of G -> non-Dmulti _Graph means :Def6: :: 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 for e2 being object holds not e2 DJoins v,w,it ) ) );

existence
ex b₁ being non-Dmulti _Graph st
( the_Vertices_of b₁ = the_Vertices_of G & the_Edges_of b₁ misses the_Edges_of G & ( for v, w being Vertex of G holds
( ex e1 being object st e1 DJoins v,w,G iff for e2 being object holds not e2 DJoins v,w,b₁ ) ) )

proof end;

end;

:: deftheorem Def6 defines DLGraphComplement GLIB_012:def 6 :
for G being _Graph
for b₂ being non-Dmulti _Graph holds
( b₂ is DLGraphComplement of G iff ( the_Vertices_of b₂ = the_Vertices_of G & the_Edges_of b₂ misses the_Edges_of G & ( for v, w being Vertex of G holds
( ex e1 being object st e1 DJoins v,w,G iff for e2 being object holds not e2 DJoins v,w,b₂ ) ) ) );

theorem Th45: :: GLIB_012:45

for G1, G2, G3 being _Graph
for G4 being DLGraphComplement of G1 st G1 == G2 & G3 == G4 holds
G3 is DLGraphComplement of G2

proof end;

registration

let G be _Graph;

cluster Relation-like NAT -defined Function-like finite [Graph-like] non-Dmulti plain for DLGraphComplement of G;

existence
ex b₁ being DLGraphComplement of G st b₁ is plain

proof end;

end;

theorem Th46: :: GLIB_012:46

for G1 being _Graph
for G2 being DLGraphComplement of G1
for e1, e2, v, w being object st e1 DJoins v,w,G1 holds
not e2 DJoins v,w,G2

proof end;

theorem Th47: :: GLIB_012:47

for G1 being _Graph
for G2 being removeDParallelEdges of G1
for G3 being DLGraphComplement of G1 holds G3 is DLGraphComplement of G2

proof end;

theorem Th48: :: GLIB_012:48

for G1, G2 being _Graph
for G3 being removeDParallelEdges of G1
for G4 being removeDParallelEdges of G2
for G5 being DLGraphComplement of G1
for G6 being DLGraphComplement of G2 st G4 is G3 -Disomorphic holds
G6 is G5 -Disomorphic

proof end;

theorem Th49: :: GLIB_012:49

for G1 being _Graph
for G2 being b₁ -Disomorphic _Graph
for G3 being DLGraphComplement of G1
for G4 being DLGraphComplement of G2 holds G4 is G3 -Disomorphic

proof end;

theorem Th50: :: GLIB_012:50

for G1 being _Graph
for G2, G3 being DLGraphComplement of G1 holds G3 is G2 -Disomorphic

proof end;

theorem :: GLIB_012:51

for G1 being _Graph
for G2 being reverseEdgeDirections of G1
for G3 being DLGraphComplement of G1
for G4 being reverseEdgeDirections of G3 holds G4 is DLGraphComplement of G2

proof end;

theorem Th52: :: GLIB_012:52

for G1 being _Graph
for V being non empty Subset of (the_Vertices_of G1)
for G2 being inducedSubgraph of G1,V
for G3 being DLGraphComplement of G1
for G4 being inducedSubgraph of G3,V holds G4 is DLGraphComplement of G2

proof end;

theorem :: GLIB_012:53

for G1 being _Graph
for V being proper Subset of (the_Vertices_of G1)
for G2 being removeVertices of G1,V
for G3 being DLGraphComplement of G1
for G4 being removeVertices of G3,V holds G4 is DLGraphComplement of G2

proof end;

:: involutiveness of graph complement (DLC case)

theorem :: GLIB_012:54

for G1 being non-Dmulti _Graph
for G2 being DLGraphComplement of G1 holds G1 is DLGraphComplement of G2

proof end;

theorem Th55: :: GLIB_012:55

for G1 being _Graph
for G2 being DLGraphComplement of G1 holds G1 .order() = G2 .order() by Def6;

theorem Th56: :: GLIB_012:56

for G1 being _Graph
for G2 being DLGraphComplement of G1 holds
( ( G1 is _trivial implies G2 is _trivial ) & ( G2 is _trivial implies G1 is _trivial ) & ( G1 is loopfull implies G2 is loopless ) & ( G2 is loopless implies G1 is loopfull ) & ( G1 is loopless implies G2 is loopfull ) & ( G2 is loopfull implies G1 is loopless ) )

proof end;

registration

let G be _trivial _Graph;

cluster -> _trivial for DLGraphComplement of G;

coherence
for b₁ being DLGraphComplement of G holds b₁ is _trivial by Th56;

end;

registration

let G be non _trivial _Graph;

cluster -> non _trivial for DLGraphComplement of G;

coherence
for b₁ being DLGraphComplement of G holds not b₁ is _trivial by Th56;

end;

registration

let G be loopfull _Graph;

cluster -> loopless for DLGraphComplement of G;

coherence
for b₁ being DLGraphComplement of G holds b₁ is loopless by Th56;

end;

registration

let G be non loopfull _Graph;

cluster -> non loopless for DLGraphComplement of G;

coherence
for b₁ being DLGraphComplement of G holds not b₁ is loopless by Th56;

end;

registration

let G be loopless _Graph;

cluster -> loopfull for DLGraphComplement of G;

coherence
for b₁ being DLGraphComplement of G holds b₁ is loopfull by Th56;

end;

registration

let G be non loopless _Graph;

cluster -> non loopfull for DLGraphComplement of G;

coherence
for b₁ being DLGraphComplement of G holds not b₁ is loopfull by Th56;

end;

theorem Th57: :: GLIB_012:57

for G1 being _Graph
for G2 being DLGraphComplement of G1 st the_Edges_of G1 = G1 .loops() holds
G2 is complete

proof end;

registration

let G be edgeless _Graph;

cluster -> complete for DLGraphComplement of G;

coherence
for b₁ being DLGraphComplement of G holds b₁ is complete

proof end;

end;

registration

let G be non connected _Graph;

cluster -> connected for DLGraphComplement of G;

coherence
for b₁ being DLGraphComplement of G holds b₁ is connected

proof end;

end;

theorem :: GLIB_012:58

for G1 being _Graph
for G2 being DLGraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( ( v1 is isolated implies not v2 is isolated ) & ( v1 is endvertex implies not v2 is endvertex ) )

proof end;

theorem :: GLIB_012:59

for G1 being _Graph
for G2 being DLGraphComplement of G1
for v, w being Vertex of G1 st ( for e being object holds not e Joins v,w,G1 ) holds
ex e being object st e Joins v,w,G2

proof end;

theorem Th60: :: GLIB_012:60

for G1 being _Graph
for G2 being DLGraphComplement of G1
for v1 being Vertex of G1
for 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()) )

proof end;

theorem :: GLIB_012:61

for G1 being _Graph
for G2 being DLGraphComplement of G1
for v1 being Vertex of G1
for 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 )

proof end;

definition

let G be _Graph;

mode LGraphComplement of G -> non-multi _Graph means :Def7: :: 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 for e2 being object holds not e2 Joins v,w,it ) ) );

existence
ex b₁ being non-multi _Graph st
( the_Vertices_of b₁ = the_Vertices_of G & the_Edges_of b₁ misses the_Edges_of G & ( for v, w being Vertex of G holds
( ex e1 being object st e1 Joins v,w,G iff for e2 being object holds not e2 Joins v,w,b₁ ) ) )

proof end;

end;

:: deftheorem Def7 defines LGraphComplement GLIB_012:def 7 :
for G being _Graph
for b₂ being non-multi _Graph holds
( b₂ is LGraphComplement of G iff ( the_Vertices_of b₂ = the_Vertices_of G & the_Edges_of b₂ misses the_Edges_of G & ( for v, w being Vertex of G holds
( ex e1 being object st e1 Joins v,w,G iff for e2 being object holds not e2 Joins v,w,b₂ ) ) ) );

theorem Th62: :: GLIB_012:62

for G1, G2, G3 being _Graph
for G4 being LGraphComplement of G1 st G1 == G2 & G3 == G4 holds
G3 is LGraphComplement of G2

proof end;

registration

let G be _Graph;

cluster Relation-like NAT -defined Function-like finite [Graph-like] non-multi non-Dmulti plain for LGraphComplement of G;

existence
ex b₁ being LGraphComplement of G st b₁ is plain

proof end;

end;

theorem :: GLIB_012:63

for G1 being _Graph
for 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
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 holds
( v1,w1 are_adjacent iff not v2,w2 are_adjacent ) ) ) )

proof end;

theorem Th64: :: GLIB_012:64

for G1 being _Graph
for G2 being LGraphComplement of G1
for e1, e2, v, w being object st e1 Joins v,w,G1 holds
not e2 Joins v,w,G2

proof end;

theorem Th65: :: GLIB_012:65

for G1 being _Graph
for G2 being removeParallelEdges of G1
for G3 being LGraphComplement of G1 holds G3 is LGraphComplement of G2

proof end;

theorem Th66: :: GLIB_012:66

for G1, G2 being _Graph
for G3 being removeParallelEdges of G1
for G4 being removeParallelEdges of G2
for G5 being LGraphComplement of G1
for G6 being LGraphComplement of G2 st G4 is G3 -isomorphic holds
G6 is G5 -isomorphic

proof end;

theorem Th67: :: GLIB_012:67

for G1 being _Graph
for G2 being b₁ -isomorphic _Graph
for G3 being LGraphComplement of G1
for G4 being LGraphComplement of G2 holds G4 is G3 -isomorphic

proof end;

theorem Th68: :: GLIB_012:68

for G1 being _Graph
for G2, G3 being LGraphComplement of G1 holds G3 is G2 -isomorphic

proof end;

theorem Th69: :: GLIB_012:69

for G1 being _Graph
for V being non empty Subset of (the_Vertices_of G1)
for G2 being inducedSubgraph of G1,V
for G3 being LGraphComplement of G1
for G4 being inducedSubgraph of G3,V holds G4 is LGraphComplement of G2

proof end;

theorem :: GLIB_012:70

for G1 being _Graph
for V being proper Subset of (the_Vertices_of G1)
for G2 being removeVertices of G1,V
for G3 being LGraphComplement of G1
for G4 being removeVertices of G3,V holds G4 is LGraphComplement of G2

proof end;

:: involutiveness of graph complement (LC case)

theorem :: GLIB_012:71

for G1 being non-multi _Graph
for G2 being LGraphComplement of G1 holds G1 is LGraphComplement of G2

proof end;

theorem Th72: :: GLIB_012:72

for G1 being _Graph
for G2 being LGraphComplement of G1 holds G1 .order() = G2 .order() by Def7;

theorem Th73: :: GLIB_012:73

for G1 being _Graph
for G2 being LGraphComplement of G1 holds
( ( G1 is _trivial implies G2 is _trivial ) & ( G2 is _trivial implies G1 is _trivial ) & ( G1 is loopfull implies G2 is loopless ) & ( G2 is loopless implies G1 is loopfull ) & ( G1 is loopless implies G2 is loopfull ) & ( G2 is loopfull implies G1 is loopless ) )

proof end;

registration

let G be _trivial _Graph;

cluster -> _trivial for LGraphComplement of G;

coherence
for b₁ being LGraphComplement of G holds b₁ is _trivial by Th73;

end;

registration

let G be non _trivial _Graph;

cluster -> non _trivial for LGraphComplement of G;

coherence
for b₁ being LGraphComplement of G holds not b₁ is _trivial by Th73;

end;

registration

let G be loopfull _Graph;

cluster -> loopless for LGraphComplement of G;

coherence
for b₁ being LGraphComplement of G holds b₁ is loopless by Th73;

end;

registration

let G be non loopfull _Graph;

cluster -> non loopless for LGraphComplement of G;

coherence
for b₁ being LGraphComplement of G holds not b₁ is loopless by Th73;

end;

registration

let G be loopless _Graph;

cluster -> loopfull for LGraphComplement of G;

coherence
for b₁ being LGraphComplement of G holds b₁ is loopfull by Th73;

end;

registration

let G be non loopless _Graph;

cluster -> non loopfull for LGraphComplement of G;

coherence
for b₁ being LGraphComplement of G holds not b₁ is loopfull by Th73;

end;

theorem Th74: :: GLIB_012:74

for G1 being _Graph
for G2 being LGraphComplement of G1 st the_Edges_of G1 = G1 .loops() holds
G2 is complete

proof end;

registration

let G be edgeless _Graph;

cluster -> complete for LGraphComplement of G;

coherence
for b₁ being LGraphComplement of G holds b₁ is complete

proof end;

end;

theorem Th75: :: GLIB_012:75

for G1 being complete _Graph
for G2 being LGraphComplement of G1 holds the_Edges_of G2 = G2 .loops()

proof end;

registration

let G be complete loopfull _Graph;

cluster -> edgeless for LGraphComplement of G;

coherence
for b₁ being LGraphComplement of G holds b₁ is edgeless

proof end;

end;

registration

let G be non connected _Graph;

cluster -> connected for LGraphComplement of G;

coherence
for b₁ being LGraphComplement of G holds b₁ is connected

proof end;

end;

theorem :: GLIB_012:76

for G1 being _Graph
for G2 being LGraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( ( v1 is isolated implies not v2 is isolated ) & ( v1 is endvertex implies not v2 is endvertex ) )

proof end;

theorem Th77: :: GLIB_012:77

for G1 being _Graph
for G2 being LGraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
v2 .allNeighbors() = (the_Vertices_of G2) \ (v1 .allNeighbors())

proof end;

theorem :: GLIB_012:78

for G1 being _Graph
for G2 being LGraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds
v2 .allNeighbors() = the_Vertices_of G2

proof end;

definition

let G be _Graph;

mode DGraphComplement of G -> Dsimple _Graph means :Def8: :: GLIB_012:def 8
ex G9 being DLGraphComplement of G st it is removeLoops of G9;

existence
ex b₁ being Dsimple _Graph ex G9 being DLGraphComplement of G st b₁ is removeLoops of G9

proof end;

end;

:: deftheorem Def8 defines DGraphComplement GLIB_012:def 8 :
for G being _Graph
for b₂ being Dsimple _Graph holds
( b₂ is DGraphComplement of G iff ex G9 being DLGraphComplement of G st b₂ is removeLoops of G9 );

theorem Th79: :: GLIB_012:79

for G1, G2, G3 being _Graph
for G4 being DGraphComplement of G1 st G1 == G2 & G3 == G4 holds
G3 is DGraphComplement of G2

proof end;

registration

let G be _Graph;

cluster Relation-like NAT -defined Function-like finite [Graph-like] loopless non-Dmulti Dsimple plain for DGraphComplement of G;

existence
ex b₁ being DGraphComplement of G st b₁ is plain

proof end;

end;

theorem Th80: :: GLIB_012:80

for G1 being _Graph
for 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 for e2 being object holds not e2 DJoins v,w,G2 ) ) ) )

proof end;

theorem Th81: :: GLIB_012:81

for G1 being _Graph
for G2 being DGraphComplement of G1
for e1, e2, v, w being object st e1 DJoins v,w,G1 holds
not e2 DJoins v,w,G2

proof end;

theorem Th82: :: GLIB_012:82

for G1 being _Graph
for G2 being DSimpleGraph of G1
for G3 being DGraphComplement of G1 holds G3 is DGraphComplement of G2

proof end;

theorem Th83: :: GLIB_012:83

for G1, G2 being _Graph
for G3 being DSimpleGraph of G1
for G4 being DSimpleGraph of G2
for G5 being DGraphComplement of G1
for G6 being DGraphComplement of G2 st G4 is G3 -Disomorphic holds
G6 is G5 -Disomorphic

proof end;

theorem Th84: :: GLIB_012:84

for G1 being _Graph
for G2 being b₁ -Disomorphic _Graph
for G3 being DGraphComplement of G1
for G4 being DGraphComplement of G2 holds G4 is G3 -Disomorphic

proof end;

theorem Th85: :: GLIB_012:85

for G1 being _Graph
for G2, G3 being DGraphComplement of G1 holds G3 is G2 -Disomorphic

proof end;

theorem :: GLIB_012:86

for G1 being _Graph
for G2 being reverseEdgeDirections of G1
for G3 being DGraphComplement of G1
for G4 being reverseEdgeDirections of G3 holds G4 is DGraphComplement of G2

proof end;

theorem Th87: :: GLIB_012:87

for G1 being _Graph
for V being non empty Subset of (the_Vertices_of G1)
for G2 being inducedSubgraph of G1,V
for G3 being DGraphComplement of G1
for G4 being inducedSubgraph of G3,V holds G4 is DGraphComplement of G2

proof end;

theorem :: GLIB_012:88

for G1 being _Graph
for V being proper Subset of (the_Vertices_of G1)
for G2 being removeVertices of G1,V
for G3 being DGraphComplement of G1
for G4 being removeVertices of G3,V holds G4 is DGraphComplement of G2

proof end;

:: involutiveness of graph complement (DC case)

theorem :: GLIB_012:89

for G1 being Dsimple _Graph
for G2 being DGraphComplement of G1 holds G1 is DGraphComplement of G2

proof end;

theorem Th90: :: GLIB_012:90

for G1 being _Graph
for G2 being DGraphComplement of G1 holds G1 .order() = G2 .order() by Th80;

theorem Th91: :: GLIB_012:91

for G1 being _Graph
for G2 being DGraphComplement of G1 holds
( G1 is _trivial iff G2 is _trivial )

proof end;

registration

let G be _trivial _Graph;

cluster -> _trivial for DGraphComplement of G;

coherence
for b₁ being DGraphComplement of G holds b₁ is _trivial by Th91;

end;

registration

let G be non _trivial _Graph;

cluster -> non _trivial for DGraphComplement of G;

coherence
for b₁ being DGraphComplement of G holds not b₁ is _trivial by Th91;

end;

theorem Th92: :: GLIB_012:92

for G1 being _Graph
for G2 being DGraphComplement of G1 st the_Edges_of G1 = G1 .loops() holds
G2 is complete

proof end;

registration

let G be edgeless _Graph;

cluster -> complete for DGraphComplement of G;

coherence
for b₁ being DGraphComplement of G holds b₁ is complete

proof end;

end;

registration

let G be _trivial edgeless _Graph;

cluster -> edgeless for DGraphComplement of G;

coherence
for b₁ being DGraphComplement of G holds b₁ is edgeless ;

end;

registration

let G be non connected _Graph;

cluster -> connected for DGraphComplement of G;

coherence
for b₁ being DGraphComplement of G holds b₁ is connected

proof end;

end;

theorem :: GLIB_012:93

for G1 being non _trivial _Graph
for G2 being DGraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds
not v2 is isolated

proof end;

theorem :: GLIB_012:94

for G1 being _Graph
for G2 being DGraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & 3 c= G1 .order() & v1 is endvertex holds
not v2 is endvertex

proof end;

theorem Th95: :: GLIB_012:95

for G1 being _Graph
for G2 being DGraphComplement of G1
for v1 being Vertex of G1
for 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}) )

proof end;

theorem :: GLIB_012:96

for G1 being _Graph
for G2 being DGraphComplement of G1
for v1 being Vertex of G1
for 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} )

proof end;

definition

let G be _Graph;

mode GraphComplement of G -> simple _Graph means :Def9: :: GLIB_012:def 9
ex G9 being LGraphComplement of G st it is removeLoops of G9;

existence
ex b₁ being simple _Graph ex G9 being LGraphComplement of G st b₁ is removeLoops of G9

proof end;

end;

:: deftheorem Def9 defines GraphComplement GLIB_012:def 9 :
for G being _Graph
for b₂ being simple _Graph holds
( b₂ is GraphComplement of G iff ex G9 being LGraphComplement of G st b₂ is removeLoops of G9 );

theorem Th97: :: GLIB_012:97

for G1, G2, G3 being _Graph
for G4 being GraphComplement of G1 st G1 == G2 & G3 == G4 holds
G3 is GraphComplement of G2

proof end;

registration

let G be _Graph;

cluster Relation-like NAT -defined Function-like finite [Graph-like] loopless non-multi non-Dmulti simple Dsimple plain for GraphComplement of G;

existence
ex b₁ being GraphComplement of G st b₁ is plain

proof end;

end;

theorem Th98: :: GLIB_012:98

for G1 being _Graph
for 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 for e2 being object holds not e2 Joins v,w,G2 ) ) ) )

proof end;

theorem Th99: :: GLIB_012:99

for G1 being _Graph
for 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
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( v1,w1 are_adjacent iff not v2,w2 are_adjacent ) ) ) )

proof end;

theorem Th100: :: GLIB_012:100

for G1 being _Graph
for G2 being GraphComplement of G1
for e1, e2, v, w being object st e1 Joins v,w,G1 holds
not e2 Joins v,w,G2

proof end;

theorem Th101: :: GLIB_012:101

for G1 being _Graph
for G2 being SimpleGraph of G1
for G3 being GraphComplement of G1 holds G3 is GraphComplement of G2

proof end;

theorem Th102: :: GLIB_012:102

for G1, G2 being _Graph
for G3 being SimpleGraph of G1
for G4 being SimpleGraph of G2
for G5 being GraphComplement of G1
for G6 being GraphComplement of G2 st G4 is G3 -isomorphic holds
G6 is G5 -isomorphic

proof end;

theorem Th103: :: GLIB_012:103

for G1 being _Graph
for G2 being b₁ -isomorphic _Graph
for G3 being GraphComplement of G1
for G4 being GraphComplement of G2 holds G4 is G3 -isomorphic

proof end;

theorem Th104: :: GLIB_012:104

for G1 being _Graph
for G2, G3 being GraphComplement of G1 holds G3 is G2 -isomorphic

proof end;

theorem Th105: :: GLIB_012:105

for G1 being _Graph
for v being object
for 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 holds
ex G4 being addAdjVertexAll of G3,v,(the_Vertices_of G1) \ V st G4 is GraphComplement of G2

proof end;

theorem :: GLIB_012:106

for G1 being _Graph
for v being object
for G2 being addVertex of G1,v
for G3 being GraphComplement of G1 st not v in the_Vertices_of G1 holds
ex G4 being addAdjVertexAll of G3,v st G4 is GraphComplement of G2

proof end;

theorem :: GLIB_012:107

for G1 being _Graph
for v being object
for G2 being addAdjVertexAll of G1,v
for G3 being GraphComplement of G1
for 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

proof end;

theorem Th108: :: GLIB_012:108

for G1 being _Graph
for V being non empty Subset of (the_Vertices_of G1)
for G2 being inducedSubgraph of G1,V
for G3 being GraphComplement of G1
for G4 being inducedSubgraph of G3,V holds G4 is GraphComplement of G2

proof end;

theorem :: GLIB_012:109

for G1 being _Graph
for V being proper Subset of (the_Vertices_of G1)
for G2 being removeVertices of G1,V
for G3 being GraphComplement of G1
for G4 being removeVertices of G3,V holds G4 is GraphComplement of G2

proof end;

:: involutiveness of graph complement (C case)

theorem Th110: :: GLIB_012:110

for G1 being simple _Graph
for G2 being GraphComplement of G1 holds G1 is GraphComplement of G2

proof end;

theorem Th111: :: GLIB_012:111

for G1 being _Graph
for G2 being GraphComplement of G1 holds G1 .order() = G2 .order() by Th98;

theorem Th112: :: GLIB_012:112

for G1 being _Graph
for G2 being GraphComplement of G1 holds
( G1 is _trivial iff G2 is _trivial )

proof end;

registration

let G be _trivial _Graph;

cluster -> _trivial for GraphComplement of G;

coherence
for b₁ being GraphComplement of G holds b₁ is _trivial by Th112;

end;

registration

let G be non _trivial _Graph;

cluster -> non _trivial for GraphComplement of G;

coherence
for b₁ being GraphComplement of G holds not b₁ is _trivial by Th112;

end;

theorem Th113: :: GLIB_012:113

for G1 being _Graph
for G2 being GraphComplement of G1 holds
( ( G1 is complete implies G2 is edgeless ) & ( G2 is edgeless implies G1 is complete ) & ( the_Edges_of G1 = G1 .loops() implies G2 is complete ) & ( G2 is complete implies the_Edges_of G1 = G1 .loops() ) )

proof end;

registration

let G be complete _Graph;

cluster -> edgeless for GraphComplement of G;

coherence
for b₁ being GraphComplement of G holds b₁ is edgeless by Th113;

end;

registration

let G be non complete _Graph;

cluster -> non edgeless for GraphComplement of G;

coherence
for b₁ being GraphComplement of G holds not b₁ is edgeless by Th113;

end;

registration

let G be edgeless _Graph;

cluster -> complete for GraphComplement of G;

coherence
for b₁ being GraphComplement of G holds b₁ is complete

proof end;

end;

registration

let G be non connected _Graph;

cluster -> connected for GraphComplement of G;

coherence
for b₁ being GraphComplement of G holds b₁ is connected

proof end;

end;

theorem :: GLIB_012:114

for G1 being non _trivial _Graph
for G2 being GraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds
not v2 is isolated

proof end;

theorem Th115: :: GLIB_012:115

for G1 being _Graph
for G2 being GraphComplement of G1
for v1 being Vertex of G1
for 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 ) )

proof end;

theorem :: GLIB_012:116

for G1 being simple _Graph
for G2 being GraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & G1 .order() = 2 holds
( ( v1 is endvertex implies v2 is isolated ) & ( v2 is isolated implies v1 is endvertex ) & ( v1 is isolated implies v2 is endvertex ) & ( v2 is endvertex implies v1 is isolated ) )

proof end;

:: in case G.order() = 3 we have the endvertices of P3 with complement K2+K1

theorem :: GLIB_012:117

for G1 being _Graph
for G2 being GraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & 4 c= G1 .order() & v1 is endvertex holds
not v2 is endvertex

proof end;

theorem Th118: :: GLIB_012:118

for G1 being _Graph
for G2 being GraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
v2 .allNeighbors() = (the_Vertices_of G2) \ ((v1 .allNeighbors()) \/ {v2})

proof end;

theorem :: GLIB_012:119

for G1 being _Graph
for G2 being GraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds
v2 .allNeighbors() = (the_Vertices_of G2) \ {v2}

proof end;

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;

:: deftheorem defines self-DLcomplementary GLIB_012:def 10 :
for G being _Graph holds
( G is self-DLcomplementary iff for H being DLGraphComplement of G holds H is G -Disomorphic );

:: deftheorem defines self-Lcomplementary GLIB_012:def 11 :
for G being _Graph holds
( G is self-Lcomplementary iff for H being LGraphComplement of G holds H is G -isomorphic );

:: deftheorem defines self-Dcomplementary GLIB_012:def 12 :
for G being _Graph holds
( G is self-Dcomplementary iff for H being DGraphComplement of G holds H is G -Disomorphic );

:: deftheorem defines self-complementary GLIB_012:def 13 :
for G being _Graph holds
( G is self-complementary iff for H being GraphComplement of G holds H is G -isomorphic );

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 )

proof end;

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 )

proof end;

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 )

proof end;

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 )

proof end;

registration

cluster Relation-like NAT -defined Function-like finite [Graph-like] self-DLcomplementary -> non loopless non-Dmulti connected non loopfull for set ;

coherence
for b₁ being _Graph st b₁ is self-DLcomplementary holds
( not b₁ is loopless & not b₁ is loopfull & b₁ is non-Dmulti & b₁ is connected )

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] self-Lcomplementary -> non loopless non-multi connected non loopfull for set ;

coherence
for b₁ being _Graph st b₁ is self-Lcomplementary holds
( not b₁ is loopless & not b₁ is loopfull & b₁ is non-multi & b₁ is connected )

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] self-Dcomplementary -> Dsimple connected for set ;

coherence
for b₁ being _Graph st b₁ is self-Dcomplementary holds
( b₁ is Dsimple & b₁ is connected )

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] self-complementary -> simple connected for set ;

coherence
for b₁ being _Graph st b₁ is self-complementary holds
( b₁ is simple & b₁ is connected )

proof end;

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 Relation-like NAT -defined Function-like finite [Graph-like] _trivial edgeless -> self-Dcomplementary self-complementary for set ;

coherence
for b₁ being _Graph st b₁ is _trivial & b₁ is edgeless holds
( b₁ is self-Dcomplementary & b₁ is self-complementary ) by GLIB_010:178;

cluster Relation-like NAT -defined Function-like finite [Graph-like] self-Dcomplementary self-complementary -> _trivial edgeless for set ;

coherence
for b₁ being _Graph st b₁ is self-Dcomplementary & b₁ is self-complementary holds
( b₁ is _trivial & b₁ is edgeless )

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] self-DLcomplementary -> non _trivial non self-Lcomplementary non self-Dcomplementary non self-complementary for set ;

coherence
for b₁ being _Graph st b₁ is self-DLcomplementary holds
( not b₁ is _trivial & not b₁ is self-Lcomplementary & not b₁ is self-Dcomplementary & not b₁ is self-complementary )

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] self-Lcomplementary -> non _trivial non self-DLcomplementary non self-Dcomplementary non self-complementary for set ;

coherence
for b₁ being _Graph st b₁ is self-Lcomplementary holds
( not b₁ is _trivial & not b₁ is self-DLcomplementary & not b₁ is self-Dcomplementary & not b₁ is self-complementary ) ;

end;

registration

cluster Relation-like NAT -defined Function-like finite [Graph-like] self-Dcomplementary self-complementary for set ;

existence
ex b₁ being _Graph st
( b₁ is self-Dcomplementary & b₁ is self-complementary )

proof end;

end;