:: About Supergraphs, Part {II}
:: by Sebastian Koch
::
:: Received June 29, 2018
:: Copyright (c) 2018-2021 Association of Mizar Users

definition

let G be _Graph;
let E be set ;

mode reverseEdgeDirections of G,E -> _Graph means :Def1: :: GLIB_007:def 1
( the_Vertices_of it = the_Vertices_of G & the_Edges_of it = the_Edges_of G & the_Source_of it = (the_Source_of G) +* ((the_Target_of G) | E) & the_Target_of it = (the_Target_of G) +* ((the_Source_of G) | E) ) if E c= the_Edges_of G
otherwise it == G;

existence
( ( E c= the_Edges_of G implies ex b₁ being _Graph st
( the_Vertices_of b₁ = the_Vertices_of G & the_Edges_of b₁ = the_Edges_of G & the_Source_of b₁ = (the_Source_of G) +* ((the_Target_of G) | E) & the_Target_of b₁ = (the_Target_of G) +* ((the_Source_of G) | E) ) ) & ( not E c= the_Edges_of G implies ex b₁ being _Graph st b₁ == G ) )

proof end;

consistency
for b₁ being _Graph holds verum ;

end;

:: deftheorem Def1 defines reverseEdgeDirections GLIB_007:def 1 :
for G being _Graph
for E being set
for b₃ being _Graph holds
( ( E c= the_Edges_of G implies ( b₃ is reverseEdgeDirections of G,E iff ( the_Vertices_of b₃ = the_Vertices_of G & the_Edges_of b₃ = the_Edges_of G & the_Source_of b₃ = (the_Source_of G) +* ((the_Target_of G) | E) & the_Target_of b₃ = (the_Target_of G) +* ((the_Source_of G) | E) ) ) ) & ( not E c= the_Edges_of G implies ( b₃ is reverseEdgeDirections of G,E iff b₃ == G ) ) );

definition

let G be _Graph;
mode reverseEdgeDirections of G is reverseEdgeDirections of G, the_Edges_of G;

end;

theorem :: GLIB_007:1

for G being _Graph
for E being set
for G1, G2 being reverseEdgeDirections of G,E holds G1 == G2

proof end;

theorem Th2: :: GLIB_007:2

for G, G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G,E st G1 == G2 holds
G2 is reverseEdgeDirections of G,E

proof end;

theorem Th3: :: GLIB_007:3

for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E holds G2 is reverseEdgeDirections of G1,E

proof end;

theorem Th4: :: GLIB_007:4

for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E holds
( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 )

proof end;

theorem Th5: :: GLIB_007:5

for G2 being _Graph
for G1 being reverseEdgeDirections of G2 holds G2 is reverseEdgeDirections of G1

proof end;

theorem Th6: :: GLIB_007:6

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

proof end;

Lm1: for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for v1, e, v2 being object st E c= the_Edges_of G2 & e in E & e DJoins v1,v2,G2 holds
e DJoins v2,v1,G1

proof end;

theorem Th7: :: GLIB_007:7

for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for v1, e, v2 being object st E c= the_Edges_of G2 & e in E holds
( e DJoins v1,v2,G2 iff e DJoins v2,v1,G1 )

proof end;

Lm2: for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for v1, e, v2 being object st E c= the_Edges_of G2 & not e in E & e DJoins v1,v2,G2 holds
e DJoins v1,v2,G1

proof end;

theorem Th8: :: GLIB_007:8

for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for v1, e, v2 being object st E c= the_Edges_of G2 & not e in E holds
( e DJoins v1,v2,G2 iff e DJoins v1,v2,G1 )

proof end;

Lm3: for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E st E c= the_Edges_of G2 holds
for v1, e, v2 being object st e Joins v1,v2,G2 holds
e Joins v1,v2,G1

proof end;

theorem Th9: :: GLIB_007:9

for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for v1, e, v2 being object holds
( e Joins v1,v2,G2 iff e Joins v1,v2,G1 )

proof end;

theorem Th10: :: GLIB_007:10

for G2 being _Graph
for E being set
for v being object
for G1 being reverseEdgeDirections of G2,E holds
( v is Vertex of G1 iff v is Vertex of G2 ) by Th4;

theorem Th11: :: GLIB_007:11

for G2 being _Graph
for E, V being set
for G1 being reverseEdgeDirections of G2,E holds G1 .edgesBetween V = G2 .edgesBetween V

proof end;

theorem Th12: :: GLIB_007:12

for G2 being _Graph
for E, V being set
for G1 being reverseEdgeDirections of G2,E holds G1 .edgesInOut V = G2 .edgesInOut V

proof end;

theorem Th13: :: GLIB_007:13

for G2 being _Graph
for E, V being set
for G1 being reverseEdgeDirections of G2,E
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
v1 .edgesInOut() = v2 .edgesInOut()

proof end;

theorem Th14: :: GLIB_007:14

for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for W2 being Walk of G2 holds W2 is Walk of G1

proof end;

theorem Th15: :: GLIB_007:15

for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for W1 being Walk of G1 holds W1 is Walk of G2

proof end;

theorem Th16: :: GLIB_007:16

for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for W2 being Walk of G2
for W1 being Walk of G1 st E c= the_Edges_of G2 & W1 = W2 & W2 .edges() c= E holds
( W1 is directed iff W2 .reverse() is directed )

proof end;

theorem :: GLIB_007:17

for G2 being _Graph
for G1 being reverseEdgeDirections of G2
for W2 being Walk of G2
for W1 being Walk of G1 st W1 = W2 holds
( W1 is directed iff W2 .reverse() is directed )

proof end;

Lm4: for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for W2 being Walk of G2
for W1 being Walk of G1 st W1 = W2 & W1 is chordal holds
W2 is chordal

proof end;

theorem Th18: :: GLIB_007:18

for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for W2 being Walk of G2
for W1 being Walk of G1 st W1 = W2 holds
( W1 is chordal iff W2 is chordal )

proof end;

theorem Th19: :: GLIB_007:19

for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for v1, v2 being object holds
( ex W1 being Walk of G1 st W1 is_Walk_from v1,v2 iff ex W2 being Walk of G2 st W2 is_Walk_from v1,v2 )

proof end;

theorem Th20: :: GLIB_007:20

for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2

proof end;

theorem Th21: :: GLIB_007:21

for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E holds
( G1 .componentSet() = G2 .componentSet() & G1 .numComponents() = G2 .numComponents() )

proof end;

registration

let G be _trivial _Graph;
let E be set ;

cluster -> _trivial for reverseEdgeDirections of G,E;

coherence
for b₁ being reverseEdgeDirections of G,E holds b₁ is _trivial

proof end;

end;

registration

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

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

coherence
for b₁ being reverseEdgeDirections of G,E holds not b₁ is _trivial

proof end;

end;

:: More theorems of this kind can be produced with other
:: subgraph modes. This particular example was needed
:: to show that the cut-vertex property prevails in graphs
:: with (partially) reversed edge directions

theorem Th22: :: GLIB_007:22

for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for v being set
for G3 being removeVertex of G1,v
for G4 being removeVertex of G2,v holds G4 is reverseEdgeDirections of G3,E \ (G1 .edgesInOut {v})

proof end;

Lm5: for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( ( v1 is isolated implies v2 is isolated ) & ( v1 is endvertex implies v2 is endvertex ) & ( v1 is cut-vertex implies v2 is cut-vertex ) )

proof end;

theorem :: GLIB_007:23

for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E
for v1 being Vertex of G1
for v2 being Vertex of G2 st 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 ) & ( v1 is cut-vertex implies v2 is cut-vertex ) & ( v2 is cut-vertex implies v1 is cut-vertex ) )

proof end;

theorem :: GLIB_007:24

for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E holds
( G1 .order() = G2 .order() & G1 .size() = G2 .size() )

proof end;

theorem Th25: :: GLIB_007:25

for G2 being _Graph
for E being set
for G1 being reverseEdgeDirections of G2,E st E c= the_Edges_of G2 & G2 is non-Dmulti & ( for e1, e2, v1, v2 being object st e1 Joins v1,v2,G2 & e2 Joins v1,v2,G2 & not ( e1 in E & e2 in E ) holds
( not e1 in E & not e2 in E ) ) holds
G1 is non-Dmulti

proof end;

registration

let G be non-Dmulti _Graph;

cluster -> non-Dmulti for reverseEdgeDirections of G, the_Edges_of G;

coherence
for b₁ being reverseEdgeDirections of G holds b₁ is non-Dmulti

proof end;

end;

registration

let G be non non-Dmulti _Graph;

cluster -> non non-Dmulti for reverseEdgeDirections of G, the_Edges_of G;

coherence
for b₁ being reverseEdgeDirections of G holds not b₁ is non-Dmulti

proof end;

end;

registration

let G be non-multi _Graph;
let E be set ;

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

coherence
for b₁ being reverseEdgeDirections of G,E holds b₁ is non-multi

proof end;

end;

registration

let G be non non-multi _Graph;
let E be set ;

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

coherence
for b₁ being reverseEdgeDirections of G,E holds not b₁ is non-multi

proof end;

end;

registration

let G be loopless _Graph;
let E be set ;

cluster -> loopless for reverseEdgeDirections of G,E;

coherence
for b₁ being reverseEdgeDirections of G,E holds b₁ is loopless

proof end;

end;

registration

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

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

coherence
for b₁ being reverseEdgeDirections of G,E holds not b₁ is loopless

proof end;

end;

registration

let G be connected _Graph;
let E be set ;

cluster -> connected for reverseEdgeDirections of G,E;

coherence
for b₁ being reverseEdgeDirections of G,E holds b₁ is connected

proof end;

end;

registration

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

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

coherence
for b₁ being reverseEdgeDirections of G,E holds not b₁ is connected

proof end;

end;

registration

let G be acyclic _Graph;
let E be set ;

cluster -> acyclic for reverseEdgeDirections of G,E;

coherence
for b₁ being reverseEdgeDirections of G,E holds b₁ is acyclic

proof end;

end;

registration

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

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

coherence
for b₁ being reverseEdgeDirections of G,E holds not b₁ is acyclic

proof end;

end;

registration

let G be complete _Graph;
let E be set ;

cluster -> complete for reverseEdgeDirections of G,E;

coherence
for b₁ being reverseEdgeDirections of G,E holds b₁ is complete

proof end;

end;

registration

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

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

coherence
for b₁ being reverseEdgeDirections of G,E holds not b₁ is complete

proof end;

end;

registration

let G be chordal _Graph;
let E be set ;

cluster -> chordal for reverseEdgeDirections of G,E;

coherence
for b₁ being reverseEdgeDirections of G,E holds b₁ is chordal

proof end;

end;

:: "non"-version of this cluster has to wait
:: because non chordal existence will be proven with cycle graphs

registration

let G be _finite _Graph;
let E be set ;

cluster -> _finite for reverseEdgeDirections of G,E;

coherence
for b₁ being reverseEdgeDirections of G,E holds b₁ is _finite

proof end;

end;

registration

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

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

coherence
for b₁ being reverseEdgeDirections of G,E holds not b₁ is _finite

proof end;

end;

theorem Th26: :: GLIB_007:26

for G2 being _Graph
for G1 being reverseEdgeDirections of G2 holds
( the_Source_of G1 = the_Target_of G2 & the_Target_of G1 = the_Source_of G2 )

proof end;

theorem :: GLIB_007:27

for G2 being _Graph
for G1 being reverseEdgeDirections of G2
for v1, e, v2 being object holds
( e DJoins v1,v2,G2 iff e DJoins v2,v1,G1 )

proof end;

Lm6: for X, Y being set holds X /\ (Y --> X) = {}

proof end;

Lm7: for X, Y being set
for x being object st X /\ Y = {} & x in X holds
not x in Y
by XBOOLE_0:def 4;

:: we need a lot of edges, so we take the freedom
:: to specify them within the definition

definition

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

mode addAdjVertexToAll of G,v,V -> Supergraph of G means :Def2: :: GLIB_007:def 2
( the_Vertices_of it = (the_Vertices_of G) \/ {v} & the_Edges_of it = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of it = (the_Source_of G) +* ((V --> (the_Edges_of G)) --> v) & the_Target_of it = (the_Target_of G) +* (pr1 (V,{(the_Edges_of G)})) ) if ( V c= the_Vertices_of G & not v in the_Vertices_of G )
otherwise it == G;

existence
( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ex b₁ being Supergraph of G st
( the_Vertices_of b₁ = (the_Vertices_of G) \/ {v} & the_Edges_of b₁ = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of b₁ = (the_Source_of G) +* ((V --> (the_Edges_of G)) --> v) & the_Target_of b₁ = (the_Target_of G) +* (pr1 (V,{(the_Edges_of G)})) ) ) & ( ( not V c= the_Vertices_of G or v in 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 Def2 defines addAdjVertexToAll GLIB_007:def 2 :
for G being _Graph
for v being object
for V being set
for b₄ being Supergraph of G holds
( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ( b₄ is addAdjVertexToAll of G,v,V iff ( the_Vertices_of b₄ = (the_Vertices_of G) \/ {v} & the_Edges_of b₄ = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of b₄ = (the_Source_of G) +* ((V --> (the_Edges_of G)) --> v) & the_Target_of b₄ = (the_Target_of G) +* (pr1 (V,{(the_Edges_of G)})) ) ) ) & ( ( not V c= the_Vertices_of G or v in the_Vertices_of G ) implies ( b₄ is addAdjVertexToAll of G,v,V iff b₄ == G ) ) );

definition

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

mode addAdjVertexFromAll of G,v,V -> Supergraph of G means :Def3: :: GLIB_007:def 3
( the_Vertices_of it = (the_Vertices_of G) \/ {v} & the_Edges_of it = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of it = (the_Source_of G) +* (pr1 (V,{(the_Edges_of G)})) & the_Target_of it = (the_Target_of G) +* ((V --> (the_Edges_of G)) --> v) ) if ( V c= the_Vertices_of G & not v in the_Vertices_of G )
otherwise it == G;

existence
( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ex b₁ being Supergraph of G st
( the_Vertices_of b₁ = (the_Vertices_of G) \/ {v} & the_Edges_of b₁ = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of b₁ = (the_Source_of G) +* (pr1 (V,{(the_Edges_of G)})) & the_Target_of b₁ = (the_Target_of G) +* ((V --> (the_Edges_of G)) --> v) ) ) & ( ( not V c= the_Vertices_of G or v in 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 Def3 defines addAdjVertexFromAll GLIB_007:def 3 :
for G being _Graph
for v being object
for V being set
for b₄ being Supergraph of G holds
( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ( b₄ is addAdjVertexFromAll of G,v,V iff ( the_Vertices_of b₄ = (the_Vertices_of G) \/ {v} & the_Edges_of b₄ = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of b₄ = (the_Source_of G) +* (pr1 (V,{(the_Edges_of G)})) & the_Target_of b₄ = (the_Target_of G) +* ((V --> (the_Edges_of G)) --> v) ) ) ) & ( ( not V c= the_Vertices_of G or v in the_Vertices_of G ) implies ( b₄ is addAdjVertexFromAll of G,v,V iff b₄ == G ) ) );

definition

let G be _Graph;
let v be object ;
mode addAdjVertexToAll of G,v is addAdjVertexToAll of G,v, the_Vertices_of G;
correctness
;
mode addAdjVertexFromAll of G,v is addAdjVertexFromAll of G,v, the_Vertices_of G;
correctness
;

end;

theorem :: GLIB_007:28

for G being _Graph
for v being object
for V being set
for G1, G2 being addAdjVertexToAll of G,v,V holds G1 == G2

proof end;

theorem :: GLIB_007:29

for G being _Graph
for v being object
for V being set
for G1, G2 being addAdjVertexFromAll of G,v,V holds G1 == G2

proof end;

theorem :: GLIB_007:30

for G, G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexToAll of G,v,V st G1 == G2 holds
G2 is addAdjVertexToAll of G,v,V

proof end;

theorem :: GLIB_007:31

for G, G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexFromAll of G,v,V st G1 == G2 holds
G2 is addAdjVertexFromAll of G,v,V

proof end;

theorem Th32: :: GLIB_007:32

for G being _Graph
for v being object
for V being set
for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V holds
( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 )

proof end;

theorem Th33: :: GLIB_007:33

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G1 .edgesOutOf {v} = V --> (the_Edges_of G2)

proof end;

theorem Th34: :: GLIB_007:34

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexFromAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G1 .edgesInto {v} = V --> (the_Edges_of G2)

proof end;

theorem Th35: :: GLIB_007:35

for G being _Graph
for v being object
for V being set
for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V st V c= the_Vertices_of G & not v in the_Vertices_of G holds
( G2 is reverseEdgeDirections of G1,G1 .edgesOutOf {v} & G1 is reverseEdgeDirections of G2,G2 .edgesInto {v} )

proof end;

theorem :: GLIB_007:36

for G being _Graph
for v being object
for V being set
for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V
for v1, e, v2 being object holds
( e Joins v1,v2,G1 iff e Joins v1,v2,G2 )

proof end;

theorem :: GLIB_007:37

for G being _Graph
for v being object
for V being set
for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V
for w being object holds
( w is Vertex of G1 iff w is Vertex of G2 ) by Th32;

theorem Th38: :: GLIB_007:38

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
for e1, u being object holds
( not e1 DJoins u,v,G1 & ( not u in V implies not e1 DJoins v,u,G1 ) & ( for e2 being object st e1 DJoins v,u,G1 & e2 DJoins v,u,G1 holds
e1 = e2 ) )

proof end;

theorem Th39: :: GLIB_007:39

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexFromAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
for e1, u being object holds
( not e1 DJoins v,u,G1 & ( not u in V implies not e1 DJoins u,v,G1 ) & ( for e2 being object st e1 DJoins u,v,G1 & e2 DJoins u,v,G1 holds
e1 = e2 ) )

proof end;

theorem Th40: :: GLIB_007:40

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
for e, v1, v2 being object st v1 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G2

proof end;

theorem Th41: :: GLIB_007:41

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexFromAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
for e, v1, v2 being object st v2 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G2

proof end;

theorem Th42: :: GLIB_007:42

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexToAll of G2,v,V
for v1 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V holds
[v1,(the_Edges_of G2)] DJoins v,v1,G1

proof end;

theorem Th43: :: GLIB_007:43

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexFromAll of G2,v,V
for v1 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 in V holds
[v1,(the_Edges_of G2)] DJoins v1,v,G1

proof end;

theorem :: GLIB_007:44

for G being _Graph
for v being object
for V being set
for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V
for W1 being Walk of G1 holds W1 is Walk of G2

proof end;

theorem :: GLIB_007:45

for G being _Graph
for v being object
for V being set
for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V
for W2 being Walk of G2 holds W2 is Walk of G1

proof end;

Lm8: for V, E being set holds card V = card (V --> E)

proof end;

Lm9: for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( ( for e being object holds
( not e Joins v,v,G1 & ( for v1 being object holds
( ( not v1 in V implies not e Joins v1,v,G1 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G2 ) ) ) ) ) & ex E being set st
( card V = card E & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) ) ) )

proof end;

Lm10: for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexFromAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( ( for e being object holds
( not e Joins v,v,G1 & ( for v1 being object holds
( ( not v1 in V implies not e Joins v1,v,G1 ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,G1 holds
e DJoins v1,v2,G2 ) ) ) ) ) & ex E being set st
( card V = card E & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) ) ) )

proof end;

:: If someone could come up with an easier redefinition
:: without using isomorphisms, it would be appreciated.
:: Note that each property of the definition is used within
:: the next three theorems.
:: Also note that about half the definition is implied when V is finite
:: because of the card-property. However, this will not be proved here.
:: We need this general form (as opposed to addAdjVertexTo/FromAll)
:: to give a constructive characterization of star and wheel graphs
:: without having to use isomorphisms.

definition

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

mode addAdjVertexAll of G,v,V -> Supergraph of G means :Def4: :: GLIB_007:def 4
( the_Vertices_of it = (the_Vertices_of G) \/ {v} & ( for e being object holds
( not e Joins v,v,it & ( for v1 being object holds
( ( not v1 in V implies not e Joins v1,v,it ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,it holds
e DJoins v1,v2,G ) ) ) ) ) & ex E being set st
( card V = card E & E misses the_Edges_of G & the_Edges_of it = (the_Edges_of G) \/ E & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,it & ( for e2 being object st e2 Joins v1,v,it holds
e1 = e2 ) ) ) ) ) if ( V c= the_Vertices_of G & not v in the_Vertices_of G )
otherwise it == G;

existence
( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ex b₁ being Supergraph of G st
( the_Vertices_of b₁ = (the_Vertices_of G) \/ {v} & ( for e being object holds
( not e Joins v,v,b₁ & ( for v1 being object holds
( ( not v1 in V implies not e Joins v1,v,b₁ ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,b₁ holds
e DJoins v1,v2,G ) ) ) ) ) & ex E being set st
( card V = card E & E misses the_Edges_of G & the_Edges_of b₁ = (the_Edges_of G) \/ E & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,b₁ & ( for e2 being object st e2 Joins v1,v,b₁ holds
e1 = e2 ) ) ) ) ) ) & ( ( not V c= the_Vertices_of G or v in 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 Def4 defines addAdjVertexAll GLIB_007:def 4 :
for G being _Graph
for v being object
for V being set
for b₄ being Supergraph of G holds
( ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ( b₄ is addAdjVertexAll of G,v,V iff ( the_Vertices_of b₄ = (the_Vertices_of G) \/ {v} & ( for e being object holds
( not e Joins v,v,b₄ & ( for v1 being object holds
( ( not v1 in V implies not e Joins v1,v,b₄ ) & ( for v2 being object st v1 <> v & v2 <> v & e DJoins v1,v2,b₄ holds
e DJoins v1,v2,G ) ) ) ) ) & ex E being set st
( card V = card E & E misses the_Edges_of G & the_Edges_of b₄ = (the_Edges_of G) \/ E & ( for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,b₄ & ( for e2 being object st e2 Joins v1,v,b₄ holds
e1 = e2 ) ) ) ) ) ) ) & ( ( not V c= the_Vertices_of G or v in the_Vertices_of G ) implies ( b₄ is addAdjVertexAll of G,v,V iff b₄ == G ) ) );

definition

let G be _Graph;
let v be object ;
mode addAdjVertexAll of G,v is addAdjVertexAll of G,v, the_Vertices_of G;
correctness
;
let V be set ;
:: original: addAdjVertexToAll
redefine mode addAdjVertexToAll of G,v,V -> addAdjVertexAll of G,v,V;
coherence
for b₁ being addAdjVertexToAll of G,v,V holds b₁ is addAdjVertexAll of G,v,V

proof end;

:: original: addAdjVertexFromAll
redefine mode addAdjVertexFromAll of G,v,V -> addAdjVertexAll of G,v,V;
coherence
for b₁ being addAdjVertexFromAll of G,v,V holds b₁ is addAdjVertexAll of G,v,V

proof end;

end;

theorem Th46: :: GLIB_007:46

for G2 being _Graph
for v being object
for G1 being addAdjVertexAll of G2,v, {} holds the_Edges_of G2 = the_Edges_of G1

proof end;

Lm11: for G2 being _Graph
for v being object
for G1 being addAdjVertexAll of G2,v, {} st the_Edges_of G2 = {} holds
the_Edges_of G1 = {}
by Th46;

theorem Th47: :: GLIB_007:47

for G2 being _Graph
for v being object
for V being non empty set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
the_Edges_of G1 <> {}

proof end;

theorem :: GLIB_007:48

for G, G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G,v,V st G1 == G2 holds
G2 is addAdjVertexAll of G,v,V

proof end;

theorem Th49: :: GLIB_007:49

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V
for v1, e, v2 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v1 <> v & v2 <> v & e Joins v1,v2,G1 holds
e Joins v1,v2,G2

proof end;

theorem Th50: :: GLIB_007:50

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
v is Vertex of G1

proof end;

theorem Th51: :: GLIB_007:51

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V
for E being set
for v1, e, v2 being object st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & E misses the_Edges_of G2 & e Joins v1,v2,G1 & not e in the_Edges_of G2 holds
( e in E & ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) )

proof end;

theorem Th52: :: GLIB_007:52

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V
for E being set st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & E misses the_Edges_of G2 holds
ex f, g being Function of E,(V \/ {v}) st
( the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* g & ( for e being object st e in E holds
( e DJoins f . e,g . e,G1 & ( f . e = v implies g . e <> v ) & ( g . e <> v implies f . e = v ) ) ) )

proof end;

theorem Th53: :: GLIB_007:53

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
the_Edges_of G2 = G1 .edgesBetween (the_Vertices_of G2)

proof end;

theorem :: GLIB_007:54

for G2 being _Graph
for v, V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G2 is removeVertex of G1,v

proof end;

theorem Th55: :: GLIB_007:55

for G2 being _Graph
for v being object
for G1 being addAdjVertexAll of G2,v, {} holds G1 is addVertex of G2,v

proof end;

:: TODO other direction

theorem :: GLIB_007:56

for G2 being _Graph
for v, v1 being object
for G1 being addAdjVertexAll of G2,v,{v1} st v1 in the_Vertices_of G2 & not v in the_Vertices_of G2 holds
ex e being object st
( not e in the_Edges_of G2 & ( G1 is addAdjVertex of G2,v,e,v1 or G1 is addAdjVertex of G2,v1,e,v ) )

proof end;

Lm12: for G2 being _Graph
for v being object
for V being set
for W being Subset of V
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & G1 .edgesBetween (W,{v}) = {} holds
W = {}

proof end;

theorem Th57: :: GLIB_007:57

for G2 being _Graph
for v being object
for V being set
for W being Subset of V
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
ex f being Function of W,(G1 .edgesBetween (W,{v})) st
( f is one-to-one & f is onto & ( for w being object st w in W holds
f . w Joins w,v,G1 ) )

proof end;

theorem Th58: :: GLIB_007:58

for G2 being _Graph
for v being object
for V, E being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E holds
E = G1 .edgesBetween (V,{v})

proof end;

theorem :: GLIB_007:59

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( G1 .edgesBetween (V,{v}) misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ (G1 .edgesBetween (V,{v})) )

proof end;

theorem Th60: :: GLIB_007:60

for G3 being _Graph
for v being object
for V1, V2 being set
for G1 being addAdjVertexAll of G3,v,V1 \/ V2
for G2 being removeEdges of G1,(G1 .edgesBetween (V2,{v})) st V1 \/ V2 c= the_Vertices_of G3 & not v in the_Vertices_of G3 & V1 misses V2 holds
G2 is addAdjVertexAll of G3,v,V1

proof end;

theorem :: GLIB_007:61

for G3 being _Graph
for v being object
for V being set
for v1 being Vertex of G3
for G1 being addAdjVertexAll of G3,v,V \/ {v1} st V c= the_Vertices_of G3 & not v in the_Vertices_of G3 & not v1 in V holds
ex G2 being addAdjVertexAll of G3,v,V ex e being object st
( not e in the_Edges_of G2 & ( G1 is addEdge of G2,v,e,v1 or G1 is addEdge of G2,v1,e,v ) )

proof end;

theorem :: GLIB_007:62

for G3 being _Graph
for v being object
for V being set
for v1 being Vertex of G3
for e being object
for G2 being addAdjVertexAll of G3,v,V st V c= the_Vertices_of G3 & not v in the_Vertices_of G3 & not v1 in V & not e in the_Edges_of G2 holds
for G1 being _Graph st ( G1 is addEdge of G2,v1,e,v or G1 is addEdge of G2,v,e,v1 ) holds
G1 is addAdjVertexAll of G3,v,V \/ {v1}

proof end;

Lm13: for k being odd Element of NAT st 1 < k holds
k - 2 is odd Element of NAT

proof end;

theorem Th63: :: GLIB_007:63

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V
for W being Walk of G1 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( ( W .edges() c= the_Edges_of G2 & W is V5() implies not v in W .vertices() ) & ( not v in W .vertices() implies W .edges() c= the_Edges_of G2 ) )

proof end;

theorem Th64: :: GLIB_007:64

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V
for W being Walk of G1 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ( ( W .edges() c= the_Edges_of G2 & W is V5() ) or not v in W .vertices() ) holds
W is Walk of G2

proof end;

theorem Th65: :: GLIB_007:65

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V
for W being Walk of G1 st W .vertices() c= the_Vertices_of G2 holds
W .edges() c= the_Edges_of G2

proof end;

theorem :: GLIB_007:66

for G being _Graph
for v being object
for V being set
for G1, G2 being addAdjVertexAll of G,v,V holds
( the_Vertices_of G1 = the_Vertices_of G2 & ( for v1 being Vertex of G1 holds v1 is Vertex of G2 ) )

proof end;

theorem Th67: :: GLIB_007:67

for G being _Graph
for v being object
for V being set
for G1, G2 being addAdjVertexAll of G,v,V
for v1, e1, v2 being object st e1 Joins v1,v2,G1 holds
ex e2 being object st e2 Joins v1,v2,G2

proof end;

:: The closest analogon we can get for
:: theorem for G, v, V for G1, G2 being addAdjVertexToAll of G,v,V
:: holds G1 == G2
:: but also preparation for
:: registration let G, v, V; let G1 being addAdjVertexAll of G,v,V;
:: cluster -> G1-isomorphic for addAdjVertexAll of G,v,V;
:: coming soon

theorem :: GLIB_007:68

for G being _Graph
for v being object
for V being set
for G1, G2 being addAdjVertexAll of G,v,V ex f being Function of (the_Edges_of G1),(the_Edges_of G2) st
( f | (the_Edges_of G) = id (the_Edges_of G) & f is one-to-one & f is onto & ( for v1, e, v2 being object st e Joins v1,v2,G1 holds
f . e Joins v1,v2,G2 ) )

proof end;

registration

let G be loopless _Graph;
let v be object ;
let V be set ;

cluster -> loopless for addAdjVertexAll of G,v,V;

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

proof end;

end;

registration

let G be non-Dmulti _Graph;
let v be object ;
let V be set ;

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

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

proof end;

end;

registration

let G be non-multi _Graph;
let v be object ;
let V be set ;

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

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

proof end;

end;

registration

let G be Dsimple _Graph;
let v be object ;
let V be set ;

cluster -> Dsimple for addAdjVertexAll of G,v,V;

coherence
for b₁ being addAdjVertexAll of G,v,V holds b₁ is Dsimple ;

end;

registration

let G be simple _Graph;
let v be object ;
let V be set ;

cluster -> simple for addAdjVertexAll of G,v,V;

coherence
for b₁ being addAdjVertexAll of G,v,V holds b₁ is simple ;

end;

theorem Th69: :: GLIB_007:69

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V
for W being Walk of G1
for v1, v2 being Vertex of G2 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & W .first() = v1 & W .last() = v2 & not v2 in G2 .reachableFrom v1 holds
v in W .vertices()

proof end;

Lm14: for k being odd Element of NAT holds
( (k -' 1) + 1 = k & ( for n being Element of NAT st k <= n holds
k -' 1 < n ) )

proof end;

Lm15: for k, n being odd Element of NAT holds n + (k -' 1) is odd Element of NAT

proof end;

Lm16: ( 1 is odd Element of NAT & 3 is odd Element of NAT )
by POLYFORM:4, POLYFORM:6;

:: this means that in each component there is at most one
:: vertex connecting to the new one

theorem :: GLIB_007:70

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & G2 is acyclic & ( for G3 being Component of G2
for w1, w2 being Vertex of G3 st w1 in V & w2 in V holds
w1 = w2 ) holds
G1 is acyclic

proof end;

theorem :: GLIB_007:71

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ( not G2 is acyclic or ex G3 being Component of G2 ex w1, w2 being Vertex of G3 st
( w1 in V & w2 in V & w1 <> w2 ) ) holds
not G1 is acyclic

proof end;

:: this means that in each component there is at least one
:: vertex connecting to the new one

theorem Th72: :: GLIB_007:72

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ( for G3 being Component of G2 ex w being Vertex of G3 st w in V ) holds
G1 is connected

proof end;

registration

let G be connected _Graph;
let v be object ;
let V be non empty set ;

cluster -> connected for addAdjVertexAll of G,v,V;

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

proof end;

end;

theorem Th73: :: GLIB_007:73

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ex G3 being Component of G2 st
for w being Vertex of G3 holds not w in V holds
not G1 is connected

proof end;

theorem :: GLIB_007:74

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & ex G3 being Component of G2 st the_Vertices_of G3 misses V holds
not G1 is connected

proof end;

registration

let G be non connected _Graph;
let v be object ;

cluster -> non connected for addAdjVertexAll of G,v, {} ;

coherence
for b₁ being addAdjVertexAll of G,v, {} holds not b₁ is connected

proof end;

end;

theorem Th75: :: GLIB_007:75

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( G1 is complete iff ( G2 is complete & V = the_Vertices_of G2 ) )

proof end;

registration

let G be complete _Graph;

cluster -> complete for addAdjVertexAll of G, the_Vertices_of G, the_Vertices_of G;

coherence
for b₁ being addAdjVertexAll of G, the_Vertices_of G holds b₁ is complete

proof end;

end;

theorem :: GLIB_007:76

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
( G1 .order() = (G2 .order()) +` 1 & G1 .size() = (G2 .size()) +` (card V) )

proof end;

theorem :: GLIB_007:77

for G2 being _finite _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G1 .order() = (G2 .order()) + 1

proof end;

theorem :: GLIB_007:78

for G2 being _finite _Graph
for v being object
for V being finite set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
G1 .size() = (G2 .size()) + (card V)

proof end;

registration

let G be _finite _Graph;
let v be object ;
let V be set ;

cluster -> _finite for addAdjVertexAll of G,v,V;

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

proof end;

end;