:: About Supergraphs, Part {II} :: by Sebastian Koch :: :: Received June 29, 2018 :: Copyright (c) 2018-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, FINSEQ_1, SUBSET_1, RELAT_1, FUNCT_1, XXREAL_0, TARSKI, ARYTM_3, CARD_1, XBOOLE_0, NAT_1, ARYTM_1, GLIB_000, PBOOLE, FINSET_1, ZFMISC_1, RELAT_2, GLIB_002, FUNCOP_1, GLIB_001, FUNCT_4, GLIB_006, ABIAN, REWRITE1, CHORD, RCOMP_1, WAYBEL_0, MCART_1, GRAPH_1, CARD_2, FUNCT_2, GLIB_007; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCT_3, FUNCOP_1, FUNCT_4, FINSET_1, CARD_1, PBOOLE, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, VALUED_0, NAT_D, CARD_2, FINSEQ_1, RVSUM_1, FUNCT_7, ABIAN, GLIB_000, FINSEQ_8, GRAPH_2, GRAPH_5, GLIB_001, GLIB_002, CHORD, GLIB_006; constructors DOMAIN_1, BINOP_1, BINOP_2, FINSOP_1, RVSUM_1, FINSEQ_5, GRAPH_5, ABIAN, WELLORD2, FUNCT_2, FIB_NUM2, FINSEQ_8, GLIB_001, GLIB_002, RELSET_1, FUNCT_3, CHORD, NAT_D, GRAPH_2, RFINSEQ, FINSEQ_6, CARD_2, FUNCT_7, FINSEQ_1, SUBSET_1, GLIB_006; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, ABIAN, XREAL_0, NAT_1, GLIB_000, GLIB_001, GLIB_002, CHORD, INT_1, CARD_1, FUNCT_2, PARTFUN1, RELSET_1, FUNCT_4, SUBSET_1, GLIB_006; requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET; begin :: Reversing Edge Directions reserve G, G2 for _Graph, V, E for set, v for object; definition let G, E; mode reverseEdgeDirections of G, E -> _Graph means :: 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; end; definition let G; :: a.k.a. the transpose, converse or reverse of G mode reverseEdgeDirections of G is reverseEdgeDirections of G, the_Edges_of G; end; theorem :: GLIB_007:1 for G, E for G1, G2 being reverseEdgeDirections of G, E holds G1 == G2; theorem :: GLIB_007:2 for G, G2, E for G1 being reverseEdgeDirections of G, E st G1 == G2 holds G2 is reverseEdgeDirections of G, E; theorem :: GLIB_007:3 for G2, E for G1 being reverseEdgeDirections of G2, E holds G2 is reverseEdgeDirections of G1, E; theorem :: GLIB_007:4 for G2, E for G1 being reverseEdgeDirections of G2, E holds the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2; theorem :: GLIB_007:5 for G2 for G1 being reverseEdgeDirections of G2 holds G2 is reverseEdgeDirections of G1; theorem :: GLIB_007:6 for G2 being _trivial _Graph, E being set, G1 being _Graph holds G1 == G2 iff G1 is reverseEdgeDirections of G2, E; theorem :: GLIB_007:7 for G2, E for G1 being reverseEdgeDirections of G2, E, 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); theorem :: GLIB_007:8 for G2, E for G1 being reverseEdgeDirections of G2, E, 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); theorem :: GLIB_007:9 for G2, E for G1 being reverseEdgeDirections of G2, E, v1,e,v2 being object holds (e Joins v1,v2,G2 iff e Joins v1,v2,G1); theorem :: GLIB_007:10 for G2, E, v for G1 being reverseEdgeDirections of G2, E holds v is Vertex of G1 iff v is Vertex of G2; theorem :: GLIB_007:11 for G2, E, V for G1 being reverseEdgeDirections of G2, E holds G1.edgesBetween(V) = G2.edgesBetween(V); theorem :: GLIB_007:12 for G2, E, V for G1 being reverseEdgeDirections of G2, E holds G1.edgesInOut(V) = G2.edgesInOut(V); theorem :: GLIB_007:13 for G2, E, V for G1 being reverseEdgeDirections of G2, E for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 holds v1.edgesInOut() = v2.edgesInOut(); theorem :: GLIB_007:14 for G2, E for G1 being reverseEdgeDirections of G2, E, W2 being Walk of G2 holds W2 is Walk of G1; theorem :: GLIB_007:15 for G2, E for G1 being reverseEdgeDirections of G2, E, W1 being Walk of G1 holds W1 is Walk of G2; theorem :: GLIB_007:16 for G2, E for G1 being reverseEdgeDirections of G2, E for W2 being Walk of G2, 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); theorem :: GLIB_007:17 for G2 for G1 being reverseEdgeDirections of G2 for W2 being Walk of G2, W1 being Walk of G1 st W1 = W2 holds (W1 is directed iff W2.reverse() is directed); theorem :: GLIB_007:18 for G2, E for G1 being reverseEdgeDirections of G2, E for W2 being Walk of G2, W1 being Walk of G1 st W1 = W2 holds (W1 is chordal iff W2 is chordal); theorem :: GLIB_007:19 for G2, E for G1 being reverseEdgeDirections of G2, E, 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); theorem :: GLIB_007:20 for G2, E for G1 being reverseEdgeDirections of G2, E for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 holds G1.reachableFrom(v1) = G2.reachableFrom(v2); theorem :: GLIB_007:21 for G2, E for G1 being reverseEdgeDirections of G2, E holds G1.componentSet() = G2.componentSet() & G1.numComponents() = G2.numComponents(); registration let G be _trivial _Graph, E be set; cluster -> _trivial for reverseEdgeDirections of G, E; end; registration let G be non _trivial _Graph, E be set; cluster -> non _trivial for reverseEdgeDirections of G, E; 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 :: GLIB_007:22 for G2, E for G1 being reverseEdgeDirections of G2, E, v being set for G3 being removeVertex of G1, v, G4 being removeVertex of G2, v holds G4 is reverseEdgeDirections of G3, E \ G1.edgesInOut({v}); theorem :: GLIB_007:23 for G2, E for G1 being reverseEdgeDirections of G2, E for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 holds (v1 is isolated iff v2 is isolated) & (v1 is endvertex iff v2 is endvertex) & (v1 is cut-vertex iff v2 is cut-vertex); theorem :: GLIB_007:24 for G2, E for G1 being reverseEdgeDirections of G2, E holds G1.order() = G2.order() & G1.size() = G2.size(); theorem :: GLIB_007:25 for G2, E 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 holds (e1 in E & e2 in E) or (not e1 in E & not e2 in E) holds G1 is non-Dmulti; registration let G be non-Dmulti _Graph; cluster -> non-Dmulti for reverseEdgeDirections of G; end; registration let G be non non-Dmulti _Graph; cluster -> non non-Dmulti for reverseEdgeDirections of G; end; registration let G be non-multi _Graph, E be set; cluster -> non-multi for reverseEdgeDirections of G, E; end; registration let G be non non-multi _Graph, E be set; cluster -> non non-multi for reverseEdgeDirections of G, E; end; registration let G be loopless _Graph, E be set; cluster -> loopless for reverseEdgeDirections of G, E; end; registration let G be non loopless _Graph, E be set; cluster -> non loopless for reverseEdgeDirections of G, E; end; registration let G be connected _Graph, E be set; cluster -> connected for reverseEdgeDirections of G, E; end; registration let G be non connected _Graph, E be set; cluster -> non connected for reverseEdgeDirections of G, E; end; registration let G be acyclic _Graph, E be set; cluster -> acyclic for reverseEdgeDirections of G, E; end; registration let G be non acyclic _Graph, E be set; cluster -> non acyclic for reverseEdgeDirections of G, E; end; registration let G be complete _Graph, E be set; cluster -> complete for reverseEdgeDirections of G, E; end; registration let G be non complete _Graph, E be set; cluster -> non complete for reverseEdgeDirections of G, E; end; registration let G be chordal _Graph, E be set; cluster -> chordal for reverseEdgeDirections of G, E; 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, E be set; cluster -> _finite for reverseEdgeDirections of G, E; end; registration let G be non _finite _Graph, E be set; cluster -> non _finite for reverseEdgeDirections of G, E; end; theorem :: GLIB_007:26 for G2 for G1 being reverseEdgeDirections of G2 holds the_Source_of G1 = the_Target_of G2 & the_Target_of G1 = the_Source_of G2; theorem :: GLIB_007:27 for G2 for G1 being reverseEdgeDirections of G2 for v1,e,v2 being object holds (e DJoins v1,v2,G2 iff e DJoins v2,v1,G1); begin :: we need a lot of edges, so we take the freedom :: to specify them within the definition definition let G, v, V; mode addAdjVertexToAll of G,v,V -> Supergraph of G means :: 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; end; definition let G, v, V; mode addAdjVertexFromAll of G,v,V -> Supergraph of G means :: 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; end; definition let G, v; mode addAdjVertexToAll of G, v is addAdjVertexToAll of G, v, the_Vertices_of G; mode addAdjVertexFromAll of G, v is addAdjVertexFromAll of G,v, the_Vertices_of G; end; theorem :: GLIB_007:28 for G, v, V for G1, G2 being addAdjVertexToAll of G,v,V holds G1 == G2; theorem :: GLIB_007:29 for G, v, V for G1, G2 being addAdjVertexFromAll of G,v,V holds G1 == G2; theorem :: GLIB_007:30 for G, G2, v, V for G1 being addAdjVertexToAll of G,v,V st G1 == G2 holds G2 is addAdjVertexToAll of G,v,V; theorem :: GLIB_007:31 for G, G2, v, V for G1 being addAdjVertexFromAll of G,v,V st G1 == G2 holds G2 is addAdjVertexFromAll of G,v,V; theorem :: GLIB_007:32 for G, v, V 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; theorem :: GLIB_007:33 for G2, v, V 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; theorem :: GLIB_007:34 for G2, v, V 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; theorem :: GLIB_007:35 for G, v, V 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}); theorem :: GLIB_007:36 for G, v, V 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); theorem :: GLIB_007:37 for G, v, V for G1 being addAdjVertexToAll of G,v,V for G2 being addAdjVertexFromAll of G,v,V, w being object holds (w is Vertex of G1 iff w is Vertex of G2); theorem :: GLIB_007:38 for G2, v, V for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 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 holds e1 DJoins v,u,G1 & e2 DJoins v,u,G1 implies e1 = e2; theorem :: GLIB_007:39 for G2, v, V for G1 being addAdjVertexFromAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 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 holds e1 DJoins u,v,G1 & e2 DJoins u,v,G1 implies e1 = e2; theorem :: GLIB_007:40 for G2, v, V for G1 being addAdjVertexToAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 for e, v1, v2 being object st v1 <> v holds e DJoins v1,v2,G1 implies e DJoins v1,v2,G2; theorem :: GLIB_007:41 for G2, v, V for G1 being addAdjVertexFromAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 for e, v1, v2 being object st v2 <> v holds e DJoins v1,v2,G1 implies e DJoins v1,v2,G2; theorem :: GLIB_007:42 for G2, v, V for G1 being addAdjVertexToAll of G2,v,V, 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; theorem :: GLIB_007:43 for G2, v, V for G1 being addAdjVertexFromAll of G2,v,V, 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; theorem :: GLIB_007:44 for G, v, V 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; theorem :: GLIB_007:45 for G, v, V 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; :: 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, v, V; mode addAdjVertexAll of G,v,V -> Supergraph of G means :: 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 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; end; definition let G, v; mode addAdjVertexAll of G,v is addAdjVertexAll of G,v,the_Vertices_of G; let V; redefine mode addAdjVertexToAll of G,v,V -> addAdjVertexAll of G,v,V; redefine mode addAdjVertexFromAll of G,v,V -> addAdjVertexAll of G,v,V; end; theorem :: GLIB_007:46 for G2, v for G1 being addAdjVertexAll of G2,v,{} holds the_Edges_of G2 = the_Edges_of G1; theorem :: GLIB_007:47 for G2, v for V being non empty set, 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 <> {}; theorem :: GLIB_007:48 for G, G2, v, V for G1 being addAdjVertexAll of G,v,V st G1 == G2 holds G2 is addAdjVertexAll of G,v,V; theorem :: GLIB_007:49 for G2, v, V for G1 being addAdjVertexAll of G2,v,V, 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; theorem :: GLIB_007:50 for G2, v, V 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; theorem :: GLIB_007:51 for G2, v, V for G1 being addAdjVertexAll of G2,v,V for E being set, 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)); theorem :: GLIB_007:52 for G2, v, V for G1 being addAdjVertexAll of G2,v,V, 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 iff g.e <> v); theorem :: GLIB_007:53 for G2, v, V 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); theorem :: GLIB_007:54 for G2 being _Graph, v, V being set, 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; theorem :: GLIB_007:55 for G2, v for G1 being addAdjVertexAll of G2,v,{} holds G1 is addVertex of G2, v; :: TODO other direction theorem :: GLIB_007:56 for G2, v for v1 being object, G1 being addAdjVertexAll of G2,v,{v1} st v1 in the_Vertices_of G2 & not v in the_Vertices_of G2 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); theorem :: GLIB_007:57 for G2, v, V for W being Subset of V, G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ex f being Function of W, G1.edgesBetween(W,{v}) st f is one-to-one onto & for w being object st w in W holds f.w Joins w,v,G1; theorem :: GLIB_007:58 for G2, v, V, E 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}); theorem :: GLIB_007:59 for G2, v, V 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}); theorem :: GLIB_007:60 for G3 being _Graph, v being object, 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; theorem :: GLIB_007:61 for G3 being _Graph, v being object, V being set, 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 ex G2 being addAdjVertexAll of G3,v,V, 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); theorem :: GLIB_007:62 for G3 being _Graph, v being object, V being set, v1 being Vertex of G3 for e being object, 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 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}; theorem :: GLIB_007:63 for G2, v, V for G1 being addAdjVertexAll of G2,v,V, 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 non trivial implies not v in W.vertices()) & (not v in W.vertices() implies W.edges() c= the_Edges_of G2); theorem :: GLIB_007:64 for G2, v, V for G1 being addAdjVertexAll of G2,v,V, 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 non trivial) or not v in W.vertices()) holds W is Walk of G2; theorem :: GLIB_007:65 for G2, v, V for G1 being addAdjVertexAll of G2,v,V, W being Walk of G1 st W.vertices() c= the_Vertices_of G2 holds W.edges() c= the_Edges_of G2; theorem :: GLIB_007:66 for G, v, V 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; theorem :: GLIB_007:67 for G, v, V for G1, G2 being addAdjVertexAll of G,v,V for v1,e1,v2 being object st e1 Joins v1,v2,G1 ex e2 being object st e2 Joins v1,v2,G2; :: 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, v, V 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 onto & for v1,e,v2 being object st e Joins v1,v2,G1 holds f.e Joins v1,v2,G2; registration let G be loopless _Graph; let v,V; cluster -> loopless for addAdjVertexAll of G,v,V; end; registration let G be non-Dmulti _Graph; let v,V; cluster -> non-Dmulti for addAdjVertexAll of G,v,V; end; registration let G be non-multi _Graph; let v,V; cluster -> non-multi for addAdjVertexAll of G,v,V; end; registration let G be Dsimple _Graph; let v,V; cluster -> Dsimple for addAdjVertexAll of G,v,V; end; registration let G be simple _Graph; let v,V; cluster -> simple for addAdjVertexAll of G,v,V; end; theorem :: GLIB_007:69 for G2, v, V for G1 being addAdjVertexAll of G2, v, V, 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(); :: this means that in each component there is at most one :: vertex connecting to the new one theorem :: GLIB_007:70 for G2, v, V 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, w1, w2 being Vertex of G3 st w1 in V & w2 in V holds w1 = w2 holds G1 is acyclic; theorem :: GLIB_007:71 for G2, v, V for G1 being addAdjVertexAll of G2, v, V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & (G2 is non acyclic or ex G3 being Component of G2, w1, w2 being Vertex of G3 st w1 in V & w2 in V & w1 <> w2) holds G1 is non acyclic; :: this means that in each component there is at least one :: vertex connecting to the new one theorem :: GLIB_007:72 for G2, v, V 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; registration let G be connected _Graph, v be object, V be non empty set; cluster -> connected for addAdjVertexAll of G,v,V; end; theorem :: GLIB_007:73 for G2, v, V 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 G1 is non connected; theorem :: GLIB_007:74 for G2, v, V 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 G1 is non connected; registration let G be non connected _Graph, v be object; cluster -> non connected for addAdjVertexAll of G,v,{}; end; theorem :: GLIB_007:75 for G2, v, V 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; registration let G be complete _Graph; cluster -> complete for addAdjVertexAll of G, the_Vertices_of G; end; theorem :: GLIB_007:76 for G2, v, V 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; theorem :: GLIB_007:77 for G2 being _finite _Graph, v being object, 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; theorem :: GLIB_007:78 for G2 being _finite _Graph, v being object, 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; registration let G be _finite _Graph, v be object, V be set; cluster -> _finite for addAdjVertexAll of G,v,V; end;