:: by Sebastian Koch

::

:: Received December 30, 2019

:: Copyright (c) 2019-2021 Association of Mizar Users

:: 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 );

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 )

( G is loopfull iff for v being Vertex of G ex e being object st e DJoins v,v,G )

proof end;

registration

for b_{1} being _Graph st b_{1} is loopfull holds

not b_{1} is loopless

for b_{1} being _Graph st b_{1} is _trivial & not b_{1} is loopless holds

b_{1} is loopfull

ex b_{1} being _Graph st

( b_{1} is loopfull & b_{1} is complete )

not for b_{1} being _Graph holds b_{1} is loopfull
end;

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

coherence for b

not b

proof end;

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

coherence for b

b

proof end;

existence ex b

( b

proof end;

existence not for b

proof 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 )

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 ;

coherence

for b_{1} being reverseEdgeDirections of G,E holds b_{1} is loopfull
by Th3;

end;
let E be set ;

coherence

for b

registration

let G be non loopfull _Graph;

let E be set ;

coherence

for b_{1} being reverseEdgeDirections of G,E holds not b_{1} is loopfull
by Th3;

end;
let E be set ;

coherence

for b

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

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

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

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

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

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;

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 ;

coherence

for b_{1} being inducedSubgraph of G,V holds b_{1} is loopfull

for b_{1} being removeVertices of G,V holds b_{1} is loopfull
;

for b_{1} being removeVertex of G,V holds b_{1} is loopfull
;

end;
let V be set ;

coherence

for b

proof end;

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

coherence for b

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

coherence for b

registration

let G be non loopfull _Graph;

coherence

for b_{1} being spanning Subgraph of G holds not b_{1} is loopfull

coherence

for b_{1} being inducedSubgraph of G, the_Vertices_of G,E holds not b_{1} is loopfull

for b_{1} being removeEdges of G,E holds not b_{1} is loopfull
;

coherence

for b_{1} being removeEdge of G,E holds not b_{1} is loopfull
;

end;
coherence

for b

proof end;

let E be set ;coherence

for b

proof end;

coherence for b

coherence

for b

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

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 ;

coherence

for b_{1} being addVertices of G,V holds not b_{1} is loopfull

end;
let V be set ;

coherence

for b

proof end;

registration

let G be loopfull _Graph;

let v, e, w be object ;

coherence

for b_{1} being addEdge of G,v,e,w holds b_{1} is loopfull

end;
let v, e, w be object ;

coherence

for b

proof 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

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

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 ;

coherence

for b_{1} being addAdjVertex of G,v,e,w holds not b_{1} is loopfull

end;
let v, e, w be object ;

coherence

for b

proof 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

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 ;

coherence

for b_{1} being addAdjVertexAll of G,v,V holds not b_{1} is loopfull

end;
let v be object ;

let V be set ;

coherence

for b

proof end;

registration

let G be loopfull _Graph;

coherence

for b_{1} being removeParallelEdges of G holds b_{1} is loopfull

for b_{1} being removeDParallelEdges of G holds b_{1} is loopfull

end;
coherence

for b

proof end;

coherence for b

proof end;

:: removeLoops is loopless, hence non loopfull

registration

let G be non loopfull _Graph;

coherence

for b_{1} being removeParallelEdges of G holds not b_{1} is loopfull
;

coherence

for b_{1} being removeDParallelEdges of G holds not b_{1} is loopfull
;

end;
coherence

for b

coherence

for b

:: 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 ) );

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;

coherence

<*G*> is loopfull

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

end;
coherence

<*G*> is loopfull

proof end;

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

definition

let GF be non empty Graph-yielding Function;

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

end;
redefine attr GF is loopfull means :Def3: :: GLIB_012:def 3

for x being Element of dom GF holds GF . x is loopfull ;

compatibility for x being Element of dom GF holds GF . x is loopfull ;

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

proof 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 );

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;

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

end;
redefine attr GSq is loopfull means :Def4: :: GLIB_012:def 4

for n being Nat holds GSq . n is loopfull ;

compatibility for n being Nat holds GSq . n is loopfull ;

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

proof 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 );

for GSq being GraphSeq holds

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

registration

coherence

for b_{1} being Graph-yielding Function st b_{1} is empty holds

b_{1} is loopfull
;

for b_{1} being Graph-yielding Function st not b_{1} is empty & b_{1} is loopfull holds

not b_{1} is loopless

end;
for b

b

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

coherence for b

not b

proof end;

registration

existence

ex b_{1} being GraphSeq st b_{1} is loopfull

ex b_{1} being Graph-yielding FinSequence st

( not b_{1} is empty & b_{1} is loopfull )

end;
ex b

proof end;

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

existence ex b

( not b

proof end;

registration

let GF be non empty Graph-yielding loopfull Function;

let x be Element of dom GF;

coherence

GF . x is loopfull by Def3;

end;
let x be Element of dom GF;

coherence

GF . x is loopfull by Def3;

registration

let p be Graph-yielding loopfull FinSequence;

let n be Nat;

coherence

p | n is loopfull

p /^ n is loopfull

coherence

smid (p,m,n) is loopfull

(m,n) -cut p is loopfull

end;
let n be Nat;

coherence

p | n is loopfull

proof end;

coherence p /^ n is loopfull

proof end;

let m be Nat;coherence

smid (p,m,n) is loopfull

proof end;

coherence (m,n) -cut p is loopfull

proof end;

registration

let p, q be Graph-yielding loopfull FinSequence;

coherence

p ^ q is loopfull

p ^' q is loopfull

end;
coherence

p ^ q is loopfull

proof end;

coherence p ^' q is loopfull

proof end;

registration

let G1, G2 be loopfull _Graph;

coherence

<*G1,G2*> is loopfull

coherence

<*G1,G2,G3*> is loopfull

end;
coherence

<*G1,G2*> is loopfull

proof end;

let G3 be loopfull _Graph;coherence

<*G1,G2,G3*> is loopfull

proof end;

:: a loop is added to each vertex in V, regardless if that

:: vertex has a loop already or not

:: vertex has a loop already or not

definition

let G be _Graph;

let V be set ;

( ( V c= the_Vertices_of G implies ex b_{1} being Supergraph of G st

( the_Vertices_of b_{1} = 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_{1} = (the_Edges_of G) \/ E & dom f = E & rng f = V & the_Source_of b_{1} = (the_Source_of G) +* f & the_Target_of b_{1} = (the_Target_of G) +* f ) ) ) & ( not V c= the_Vertices_of G implies ex b_{1} being Supergraph of G st b_{1} == G ) )

for b_{1} being Supergraph of G holds verum
;

end;
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 ( 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;

( ( V c= the_Vertices_of G implies ex b

( the_Vertices_of b

( E misses the_Edges_of G & the_Edges_of b

proof end;

consistency for b

:: deftheorem Def5 defines addLoops GLIB_012:def 5 :

for G being _Graph

for V being set

for b_{3} being Supergraph of G holds

( ( V c= the_Vertices_of G implies ( b_{3} is addLoops of G,V iff ( the_Vertices_of b_{3} = 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_{3} = (the_Edges_of G) \/ E & dom f = E & rng f = V & the_Source_of b_{3} = (the_Source_of G) +* f & the_Target_of b_{3} = (the_Target_of G) +* f ) ) ) ) & ( not V c= the_Vertices_of G implies ( b_{3} is addLoops of G,V iff b_{3} == G ) ) );

for G being _Graph

for V being set

for b

( ( V c= the_Vertices_of G implies ( b

( E misses the_Edges_of G & the_Edges_of b

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

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 )

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 )

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

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

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)

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 :: 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

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

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()) )

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

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 ) )

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) ) ) )

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 ) )

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_{1} -isomorphic _Graph

for G1 being addLoops of G3

for G2 being addLoops of G4 holds G2 is G1 -isomorphic

for G4 being b

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_{1} -Disomorphic _Graph

for G1 being addLoops of G3

for G2 being addLoops of G4 holds G2 is G1 -Disomorphic

for G4 being b

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

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

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

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

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 ) )

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) ) )

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

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;

coherence

for b_{1} being addLoops of G holds b_{1} is loopfull

coherence

for b_{1} being addLoops of G,V holds not b_{1} is loopless

end;
coherence

for b

proof end;

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

for b

proof 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 )

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 ;

coherence

for b_{1} being addLoops of G,V holds b_{1} is _finite
by Th39;

end;
let V be set ;

coherence

for b

registration

let G be non _finite _Graph;

let V be set ;

coherence

for b_{1} being addLoops of G,V holds not b_{1} is _finite
;

end;
let V be set ;

coherence

for b

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 )

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 ;

coherence

for b_{1} being addLoops of G,V holds b_{1} is connected
by Th40;

end;
let V be set ;

coherence

for b

registration

let G be non connected _Graph;

let V be set ;

coherence

for b_{1} being addLoops of G,V holds not b_{1} is connected
by Th40;

end;
let V be set ;

coherence

for b

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 )

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 ;

coherence

for b_{1} being addLoops of G,V holds b_{1} is chordal
by Th41;

end;
let V be set ;

coherence

for b

:: non chordal clustering will be done later

registration

let G be non edgeless _Graph;

let V be set ;

coherence

for b_{1} being addLoops of G,V holds not b_{1} is edgeless
;

end;
let V be set ;

coherence

for b

registration

let G be loopfull _Graph;

let V be set ;

coherence

for b_{1} being addLoops of G,V holds b_{1} is loopfull

end;
let V be set ;

coherence

for b

proof end;

registration

let G be simple _Graph;

let V be set ;

coherence

for b_{1} being addLoops of G,V holds b_{1} is non-multi

end;
let V be set ;

coherence

for b

proof end;

registration

let G be Dsimple _Graph;

let V be set ;

coherence

for b_{1} being addLoops of G,V holds b_{1} is non-Dmulti

end;
let V be set ;

coherence

for b

proof 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} )

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 )

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() )

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;

ex b_{1} being non-Dmulti _Graph st

( the_Vertices_of b_{1} = the_Vertices_of G & the_Edges_of b_{1} 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_{1} ) ) )

end;
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 ( 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 ) ) );

ex b

( the_Vertices_of b

( ex e1 being object st e1 DJoins v,w,G iff for e2 being object holds not e2 DJoins v,w,b

proof end;

:: deftheorem Def6 defines DLGraphComplement GLIB_012:def 6 :

for G being _Graph

for b_{2} being non-Dmulti _Graph holds

( b_{2} is DLGraphComplement of G iff ( the_Vertices_of b_{2} = the_Vertices_of G & the_Edges_of b_{2} 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_{2} ) ) ) );

for G being _Graph

for b

( b

( 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

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

G3 is DLGraphComplement of G2

proof end;

registration

let G be _Graph;

ex b_{1} being DLGraphComplement of G st b_{1} is plain

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

existence ex b

proof 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

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

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

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_{1} -Disomorphic _Graph

for G3 being DLGraphComplement of G1

for G4 being DLGraphComplement of G2 holds G4 is G3 -Disomorphic

for G2 being b

for G3 being DLGraphComplement of G1

for G4 being DLGraphComplement of G2 holds G4 is G3 -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

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

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

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

for G2 being DLGraphComplement of G1 holds G1 is DLGraphComplement of G2

proof end;

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 ) )

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;

coherence

for b_{1} being DLGraphComplement of G holds b_{1} is _trivial
by Th56;

end;
coherence

for b

registration

let G be non _trivial _Graph;

coherence

for b_{1} being DLGraphComplement of G holds not b_{1} is _trivial
by Th56;

end;
coherence

for b

registration

let G be loopfull _Graph;

coherence

for b_{1} being DLGraphComplement of G holds b_{1} is loopless
by Th56;

end;
coherence

for b

registration

let G be non loopfull _Graph;

coherence

for b_{1} being DLGraphComplement of G holds not b_{1} is loopless
by Th56;

end;
coherence

for b

registration

let G be loopless _Graph;

coherence

for b_{1} being DLGraphComplement of G holds b_{1} is loopfull
by Th56;

end;
coherence

for b

registration

let G be non loopless _Graph;

coherence

for b_{1} being DLGraphComplement of G holds not b_{1} is loopfull
by Th56;

end;
coherence

for b

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

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;

coherence

for b_{1} being DLGraphComplement of G holds b_{1} is complete

end;
coherence

for b

proof end;

registration

let G be non connected _Graph;

coherence

for b_{1} being DLGraphComplement of G holds b_{1} is connected

end;
coherence

for b

proof 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 ) )

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

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()) )

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 )

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;

ex b_{1} being non-multi _Graph st

( the_Vertices_of b_{1} = the_Vertices_of G & the_Edges_of b_{1} 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_{1} ) ) )

end;
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 ( 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 ) ) );

ex b

( the_Vertices_of b

( ex e1 being object st e1 Joins v,w,G iff for e2 being object holds not e2 Joins v,w,b

proof end;

:: deftheorem Def7 defines LGraphComplement GLIB_012:def 7 :

for G being _Graph

for b_{2} being non-multi _Graph holds

( b_{2} is LGraphComplement of G iff ( the_Vertices_of b_{2} = the_Vertices_of G & the_Edges_of b_{2} 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_{2} ) ) ) );

for G being _Graph

for b

( b

( 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

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

G3 is LGraphComplement of G2

proof end;

registration

let G be _Graph;

ex b_{1} being LGraphComplement of G st b_{1} is plain

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

existence ex b

proof 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 ) ) ) )

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

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

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

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_{1} -isomorphic _Graph

for G3 being LGraphComplement of G1

for G4 being LGraphComplement of G2 holds G4 is G3 -isomorphic

for G2 being b

for G3 being LGraphComplement of G1

for G4 being LGraphComplement of G2 holds G4 is G3 -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

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

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

for G2 being LGraphComplement of G1 holds G1 is LGraphComplement of G2

proof end;

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 ) )

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;

coherence

for b_{1} being LGraphComplement of G holds b_{1} is _trivial
by Th73;

end;
coherence

for b

registration

let G be non _trivial _Graph;

coherence

for b_{1} being LGraphComplement of G holds not b_{1} is _trivial
by Th73;

end;
coherence

for b

registration

let G be loopfull _Graph;

coherence

for b_{1} being LGraphComplement of G holds b_{1} is loopless
by Th73;

end;
coherence

for b

registration

let G be non loopfull _Graph;

coherence

for b_{1} being LGraphComplement of G holds not b_{1} is loopless
by Th73;

end;
coherence

for b

registration

let G be loopless _Graph;

coherence

for b_{1} being LGraphComplement of G holds b_{1} is loopfull
by Th73;

end;
coherence

for b

registration

let G be non loopless _Graph;

coherence

for b_{1} being LGraphComplement of G holds not b_{1} is loopfull
by Th73;

end;
coherence

for b

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

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;

coherence

for b_{1} being LGraphComplement of G holds b_{1} is complete

end;
coherence

for b

proof end;

theorem Th75: :: GLIB_012:75

for G1 being complete _Graph

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

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

proof end;

registration

let G be complete loopfull _Graph;

coherence

for b_{1} being LGraphComplement of G holds b_{1} is edgeless

end;
coherence

for b

proof end;

registration

let G be non connected _Graph;

coherence

for b_{1} being LGraphComplement of G holds b_{1} is connected

end;
coherence

for b

proof 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 ) )

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())

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

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;

ex b_{1} being Dsimple _Graph ex G9 being DLGraphComplement of G st b_{1} is removeLoops of G9

end;
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 G9 being DLGraphComplement of G st it is removeLoops of G9;

ex b

proof end;

:: deftheorem Def8 defines DGraphComplement GLIB_012:def 8 :

for G being _Graph

for b_{2} being Dsimple _Graph holds

( b_{2} is DGraphComplement of G iff ex G9 being DLGraphComplement of G st b_{2} is removeLoops of G9 );

for G being _Graph

for b

( b

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

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

G3 is DGraphComplement of G2

proof end;

registration

let G be _Graph;

ex b_{1} being DGraphComplement of G st b_{1} is plain

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

existence ex b

proof 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 ) ) ) )

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

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

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

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_{1} -Disomorphic _Graph

for G3 being DGraphComplement of G1

for G4 being DGraphComplement of G2 holds G4 is G3 -Disomorphic

for G2 being b

for G3 being DGraphComplement of G1

for G4 being DGraphComplement of G2 holds G4 is G3 -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

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

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

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)

registration

let G be _trivial _Graph;

coherence

for b_{1} being DGraphComplement of G holds b_{1} is _trivial
by Th91;

end;
coherence

for b

registration

let G be non _trivial _Graph;

coherence

for b_{1} being DGraphComplement of G holds not b_{1} is _trivial
by Th91;

end;
coherence

for b

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

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;

coherence

for b_{1} being DGraphComplement of G holds b_{1} is complete

end;
coherence

for b

proof end;

registration

let G be _trivial edgeless _Graph;

coherence

for b_{1} being DGraphComplement of G holds b_{1} is edgeless
;

end;
coherence

for b

registration

let G be non connected _Graph;

coherence

for b_{1} being DGraphComplement of G holds b_{1} is connected

end;
coherence

for b

proof 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

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

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}) )

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} )

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;

ex b_{1} being simple _Graph ex G9 being LGraphComplement of G st b_{1} is removeLoops of G9

end;
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 G9 being LGraphComplement of G st it is removeLoops of G9;

ex b

proof end;

:: deftheorem Def9 defines GraphComplement GLIB_012:def 9 :

for G being _Graph

for b_{2} being simple _Graph holds

( b_{2} is GraphComplement of G iff ex G9 being LGraphComplement of G st b_{2} is removeLoops of G9 );

for G being _Graph

for b

( b

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

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

G3 is GraphComplement of G2

proof end;

registration

let G be _Graph;

ex b_{1} being GraphComplement of G st b_{1} is plain

end;
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

proof 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 ) ) ) )

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 ) ) ) )

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

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

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

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_{1} -isomorphic _Graph

for G3 being GraphComplement of G1

for G4 being GraphComplement of G2 holds G4 is G3 -isomorphic

for G2 being b

for G3 being GraphComplement of G1

for G4 being GraphComplement of G2 holds G4 is G3 -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

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

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

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

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

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)

registration

let G be _trivial _Graph;

coherence

for b_{1} being GraphComplement of G holds b_{1} is _trivial
by Th112;

end;
coherence

for b

registration

let G be non _trivial _Graph;

coherence

for b_{1} being GraphComplement of G holds not b_{1} is _trivial
by Th112;

end;
coherence

for b

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() ) )

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;

coherence

for b_{1} being GraphComplement of G holds b_{1} is edgeless
by Th113;

end;
coherence

for b

registration

let G be non complete _Graph;

coherence

for b_{1} being GraphComplement of G holds not b_{1} is edgeless
by Th113;

end;
coherence

for b

registration

let G be edgeless _Graph;

coherence

for b_{1} being GraphComplement of G holds b_{1} is complete

end;
coherence

for b

proof end;

registration

let G be non connected _Graph;

coherence

for b_{1} being GraphComplement of G holds b_{1} is connected

end;
coherence

for b

proof 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

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 ) )

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 ) )

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

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})

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}

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;

end;
attr G is self-DLcomplementary means :: GLIB_012:def 10

for H being DLGraphComplement of G holds H is G -Disomorphic ;

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 ;

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 ;

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 ;

for H being GraphComplement of G holds H is G -isomorphic ;

:: 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 );

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 );

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 );

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 );

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 )

( 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 )

( 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 )

( 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 )

( G is self-complementary iff ex H being GraphComplement of G st H is G -isomorphic )

proof end;

registration

for b_{1} being _Graph st b_{1} is self-DLcomplementary holds

( not b_{1} is loopless & not b_{1} is loopfull & b_{1} is non-Dmulti & b_{1} is connected )

for b_{1} being _Graph st b_{1} is self-Lcomplementary holds

( not b_{1} is loopless & not b_{1} is loopfull & b_{1} is non-multi & b_{1} is connected )

for b_{1} being _Graph st b_{1} is self-Dcomplementary holds

( b_{1} is Dsimple & b_{1} is connected )

for b_{1} being _Graph st b_{1} is self-complementary holds

( b_{1} is simple & b_{1} is connected )
end;

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

coherence for b

( not b

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

( not b

proof end;

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

coherence for b

( b

proof end;

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

coherence for b

( b

proof 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

:: 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

for b_{1} being _Graph st b_{1} is _trivial & b_{1} is edgeless holds

( b_{1} is self-Dcomplementary & b_{1} is self-complementary )
by GLIB_010:178;

for b_{1} being _Graph st b_{1} is self-Dcomplementary & b_{1} is self-complementary holds

( b_{1} is _trivial & b_{1} is edgeless )

for b_{1} being _Graph st b_{1} is self-DLcomplementary holds

( not b_{1} is _trivial & not b_{1} is self-Lcomplementary & not b_{1} is self-Dcomplementary & not b_{1} is self-complementary )

for b_{1} being _Graph st b_{1} is self-Lcomplementary holds

( not b_{1} is _trivial & not b_{1} is self-DLcomplementary & not b_{1} is self-Dcomplementary & not b_{1} is self-complementary )
;

end;

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

coherence for b

( b

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

coherence for b

( b

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

( not b

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

( not b

registration

ex b_{1} being _Graph st

( b_{1} is self-Dcomplementary & b_{1} is self-complementary )
end;

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

existence ex b

( b

proof end;