:: Unification of Graphs and Relations in {M}izar
:: by Sebastian Koch
::
:: Received May 31, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FINSET_1, RELAT_1, FUNCT_1, XBOOLE_0, TARSKI, SUBSET_1,
FINSEQ_1, FUNCT_4, ZFMISC_1, CARD_1, ARYTM_3, XXREAL_0, PBOOLE, GLIB_000,
RING_3, GLIB_002, PARTFUN1, FUNCT_2, CHORD, SCMYCIEL, REWRITE1, GLIB_006,
GLIB_007, GLIB_009, GLIB_010, GLIB_012, MCART_1, WAYBEL_0, MOD_4,
RELAT_2, GLIB_001, SGRAPH1, GLUNIR00, EQREL_1, GLIB_013;
notations TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
RELAT_2, RELSET_1, PARTFUN1, BINOP_1, DOMAIN_1, EQREL_1, FUNCT_3,
FUNCT_4, FINSET_1, CARD_1, XCMPLX_0, XXREAL_0, FINSEQ_1, GLIB_000,
GLIB_001, GLIB_002, CHORD, GLIB_006, GLIB_007, GLIB_008, GLIB_009,
GLIB_010, GLIB_012, GLIB_013;
constructors DOMAIN_1, FUNCT_4, CHORD, GLIB_002, GLIB_007, GLIB_008, GLIB_009,
GLIB_010, GLIB_012, COMPUT_1, EQREL_1, GLIB_013;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XREAL_0,
PARTFUN1, RELSET_1, GLIB_000, GLIB_002, GLIB_007, GLIB_009, GLIB_008,
GLIB_010, XTUPLE_0, GLIB_012, ZFMISC_1, RELAT_2, GLIBPRE0, GLIB_013;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
begin :: The Adjacency Relation
reserve G for _Graph;
definition
let G;
func VertexDomRel(G) -> Relation of the_Vertices_of G equals
:: GLUNIR00:def 1
(the_Source_of G qua Relation)~ * (the_Target_of G);
end;
theorem :: GLUNIR00:1
for v,w being object holds [v,w] in VertexDomRel(G) iff
ex e being object st e DJoins v,w,G;
theorem :: GLUNIR00:2
for v,w being object holds [v,w] in (VertexDomRel(G))~ iff
ex e being object st e DJoins w,v,G;
theorem :: GLUNIR00:3
G is loopless iff VertexDomRel(G) is irreflexive;
registration
let G be loopless _Graph;
cluster VertexDomRel(G) -> irreflexive;
end;
registration
let G be non loopless _Graph;
cluster VertexDomRel(G) -> non irreflexive;
end;
registration
let G be non-multi _Graph;
cluster VertexDomRel(G) -> antisymmetric;
end;
registration
let G be simple _Graph;
cluster VertexDomRel(G) -> asymmetric;
end;
theorem :: GLUNIR00:4
for G being _Graph
st ex e1,e2,x,y being object st e1 DJoins x,y,G & e2 DJoins y,x,G
holds VertexDomRel(G) is non asymmetric;
registration
let G be non non-multi non-Dmulti _Graph;
cluster VertexDomRel(G) -> non asymmetric;
end;
:: means G is then without isolated vertices
theorem :: GLUNIR00:5
for G being loopless _Graph
st field VertexDomRel(G) = the_Vertices_of G
holds for C being Component of G holds C is non _trivial;
:: means if G is without isolated vertices
theorem :: GLUNIR00:6
for G being _Graph st for C being Component of G holds C is non _trivial
holds field VertexDomRel(G) = the_Vertices_of G;
theorem :: GLUNIR00:7
for G being non _trivial connected _Graph
holds field VertexDomRel(G) = the_Vertices_of G;
registration
let G be complete _Graph;
cluster VertexDomRel(G) -> connected;
end;
::registration
:: let G be non complete without_isolated_vertices _Graph;
:: cluster VertexDomRel(G) -> non connected;
:: coherence;
::end;
theorem :: GLUNIR00:8
G is edgeless iff VertexDomRel(G) is empty;
registration
let G be edgeless _Graph;
cluster VertexDomRel(G) -> empty;
end;
registration
let G be non edgeless _Graph;
cluster VertexDomRel(G) -> non empty;
end;
theorem :: GLUNIR00:9
G is loopfull iff VertexDomRel(G) is total reflexive;
registration
let G be loopfull _Graph;
cluster VertexDomRel(G) -> reflexive total;
end;
::registration
:: let G be non loopfull without_isolated_vertices _Graph;
:: cluster VertexDomRel(G) -> non reflexive;
:: coherence;
::end;
registration
let G be vertex-finite _Graph;
cluster VertexDomRel(G) -> finite;
end;
theorem :: GLUNIR00:10
card VertexDomRel(G) = card Class DEdgeAdjEqRel(G);
theorem :: GLUNIR00:11
card VertexDomRel(G) c= G.size();
theorem :: GLUNIR00:12
for G being non-Dmulti _Graph holds G.size() = card VertexDomRel(G);
theorem :: GLUNIR00:13
for v being Vertex of G holds Im(VertexDomRel(G),v) = v.outNeighbors();
theorem :: GLUNIR00:14
for v being Vertex of G holds Coim(VertexDomRel(G),v) = v.inNeighbors();
theorem :: GLUNIR00:15
for H being Subgraph of G holds VertexDomRel(H) c= VertexDomRel(G);
theorem :: GLUNIR00:16
for H being removeDParallelEdges of G
holds VertexDomRel(H) = VertexDomRel(G);
theorem :: GLUNIR00:17
for H being removeLoops of G
holds VertexDomRel(H) = VertexDomRel(G) \ id the_Vertices_of G;
theorem :: GLUNIR00:18
for H being DSimpleGraph of G
holds VertexDomRel(H) = VertexDomRel(G) \ id the_Vertices_of G;
theorem :: GLUNIR00:19
for G1, G2 being _Graph st G1 == G2
holds VertexDomRel(G1) = VertexDomRel(G2);
theorem :: GLUNIR00:20
for H being reverseEdgeDirections of G
holds VertexDomRel(H) = (VertexDomRel(G))~;
theorem :: GLUNIR00:21
for V being non empty Subset of the_Vertices_of G
for H being inducedSubgraph of G, V
holds VertexDomRel(H) = VertexDomRel(G) /\ [: V, V :];
theorem :: GLUNIR00:22
for V being set, H being removeVertices of G, V st V c< the_Vertices_of G
holds VertexDomRel(H) = VertexDomRel(G)
\ ([: V, the_Vertices_of G :] \/ [: the_Vertices_of G, V :]);
theorem :: GLUNIR00:23
for G being non _trivial _Graph, v being Vertex of G
for H being removeVertex of G, v
holds VertexDomRel(H) = VertexDomRel(G)
\ ([: {v}, the_Vertices_of G :] \/ [: the_Vertices_of G, {v} :]);
theorem :: GLUNIR00:24
for G being non _trivial _Graph, v being Vertex of G
for H being removeVertex of G, v st v is isolated
holds VertexDomRel(H) = VertexDomRel(G);
theorem :: GLUNIR00:25
for V being set, H being addVertices of G, V
holds VertexDomRel(H) = VertexDomRel(G);
theorem :: GLUNIR00:26
for v, e, w being object, H being addEdge of G,v,e,w
st ex e0 being object st e0 DJoins v,w,G
holds VertexDomRel(H) = VertexDomRel(G);
theorem :: GLUNIR00:27
for v, w being Vertex of G, e being object, H being addEdge of G,v,e,w
st not e in the_Edges_of G holds VertexDomRel(H) = VertexDomRel(G) \/ {[v,w]}
;
theorem :: GLUNIR00:28
for v being Vertex of G, e,w being object, H being addAdjVertex of G,v,e,w
st not e in the_Edges_of G & not w in the_Vertices_of G
holds VertexDomRel(H) = VertexDomRel(G) \/ {[v,w]};
theorem :: GLUNIR00:29
for v,e being object, w being Vertex of G, H being addAdjVertex of G,v,e,w
st not e in the_Edges_of G & not v in the_Vertices_of G
holds VertexDomRel(H) = VertexDomRel(G) \/ {[v,w]};
:: In their current form addAdjVertexTo/FromAll seem like their definition
:: will be changed in the future to allow a more general edge set.
:: Therefore the following theorems will not be proven here at the the moment.
:: theorem
:: for v being object, V being Subset of the_Vertices_of G
:: for H being addAdjVertexToAll of G,v,V st not v in the_Vertices_of G
:: holds VertexDomRel(H) = VertexDomRel(G) \/ [: {v},V :];
::
:: theorem
:: for v being object, V being Subset of the_Vertices_of G
:: for H being addAdjVertexFromAll of G,v,V st not v in the_Vertices_of G
:: holds VertexDomRel(H) = VertexDomRel(G) \/ [: V,{v} :];
theorem :: GLUNIR00:30
for V being Subset of the_Vertices_of G, H being addLoops of G, V
holds VertexDomRel(H) = VertexDomRel(G) \/ id V;
theorem :: GLUNIR00:31
for H being DLGraphComplement of G holds VertexDomRel(H)
= [: the_Vertices_of G, the_Vertices_of G :] \ VertexDomRel(G);
definition
let G;
func VertexAdjSymRel(G) -> Relation of the_Vertices_of G equals
:: GLUNIR00:def 2
VertexDomRel(G) \/ ((VertexDomRel(G))~);
end;
theorem :: GLUNIR00:32
for v, w being object
holds [v,w] in VertexAdjSymRel(G) iff ex e being object st e Joins v,w,G;
theorem :: GLUNIR00:33
for v, w being Vertex of G
holds [v,w] in VertexAdjSymRel(G) iff v, w are_adjacent;
theorem :: GLUNIR00:34
VertexDomRel(G) c= VertexAdjSymRel(G);
theorem :: GLUNIR00:35
VertexAdjSymRel(G) = ((the_Source_of G qua Relation)~ * (the_Target_of G))
\/ ((the_Target_of G qua Relation)~ * (the_Source_of G));
registration
let G;
cluster VertexAdjSymRel(G) -> symmetric;
end;
theorem :: GLUNIR00:36
G is loopless iff VertexAdjSymRel(G) is irreflexive;
registration
let G be loopless _Graph;
cluster VertexAdjSymRel(G) -> irreflexive;
end;
registration
let G be non loopless _Graph;
cluster VertexAdjSymRel(G) -> non irreflexive;
end;
:: means G is then without isolated vertices
theorem :: GLUNIR00:37
for G being loopless _Graph st VertexAdjSymRel(G) is total
holds for C being Component of G holds C is non _trivial;
:: means if G is without isolated vertices
theorem :: GLUNIR00:38
for G being _Graph st for C being Component of G holds C is non _trivial
holds VertexAdjSymRel(G) is total;
registration
let G be non _trivial connected _Graph;
cluster VertexAdjSymRel(G) -> total;
end;
registration
let G be complete _Graph;
cluster VertexAdjSymRel(G) -> connected;
end;
:: registration
:: let G be non complete without_isolated_vertices _Graph;
:: cluster VertexAdjSymRel(G) -> non connected;
:: coherence;
:: end;
theorem :: GLUNIR00:39
G is edgeless iff VertexAdjSymRel(G) is empty;
registration
let G be edgeless _Graph;
cluster VertexAdjSymRel(G) -> empty;
end;
registration
let G be non edgeless _Graph;
cluster VertexAdjSymRel(G) -> non empty;
end;
theorem :: GLUNIR00:40
G is loopfull iff VertexAdjSymRel(G) is total reflexive;
registration
let G be loopfull _Graph;
cluster VertexAdjSymRel(G) -> reflexive total;
end;
:: registration
:: let G be non loopfull without_isolated_vertices _Graph;
:: cluster VertexAdjSymRel(G) -> non reflexive;
:: coherence;
:: end;
registration
let G be vertex-finite _Graph;
cluster VertexAdjSymRel(G) -> finite;
end;
theorem :: GLUNIR00:41
card Class DEdgeAdjEqRel(G) c= card VertexAdjSymRel(G);
theorem :: GLUNIR00:42
card Class EdgeAdjEqRel(G) c= card VertexAdjSymRel(G);
theorem :: GLUNIR00:43
for G being non-Dmulti _Graph holds G.size() c= card VertexAdjSymRel(G);
theorem :: GLUNIR00:44
for v being Vertex of G holds Im(VertexAdjSymRel(G),v) = v.allNeighbors();
theorem :: GLUNIR00:45
for H being Subgraph of G holds VertexAdjSymRel(H) c= VertexAdjSymRel(G);
theorem :: GLUNIR00:46
for H being removeParallelEdges of G
holds VertexAdjSymRel(H) = VertexAdjSymRel(G);
theorem :: GLUNIR00:47
for H being removeLoops of G
holds VertexAdjSymRel(H) = VertexAdjSymRel(G) \ id the_Vertices_of G;
theorem :: GLUNIR00:48
for H being SimpleGraph of G
holds VertexAdjSymRel(H) = VertexAdjSymRel(G) \ id the_Vertices_of G;
theorem :: GLUNIR00:49
for G1, G2 being _Graph st G1 == G2
holds VertexAdjSymRel(G1) = VertexAdjSymRel(G2);
theorem :: GLUNIR00:50
for E being set, H being reverseEdgeDirections of G, E
holds VertexAdjSymRel(H) = VertexAdjSymRel(G);
theorem :: GLUNIR00:51
for V being non empty Subset of the_Vertices_of G
for H being inducedSubgraph of G, V
holds VertexAdjSymRel(H) = VertexAdjSymRel(G) /\ [: V, V :];
theorem :: GLUNIR00:52
for V being set, H being removeVertices of G, V st V c< the_Vertices_of G
holds VertexAdjSymRel(H) = VertexAdjSymRel(G)
\ ([: V, the_Vertices_of G :] \/ [: the_Vertices_of G, V :]);
theorem :: GLUNIR00:53
for G being non _trivial _Graph, v being Vertex of G
for H being removeVertex of G, v
holds VertexAdjSymRel(H) = VertexAdjSymRel(G)
\ ([: {v}, the_Vertices_of G :] \/ [: the_Vertices_of G, {v} :]);
theorem :: GLUNIR00:54
for G being non _trivial _Graph, v being Vertex of G
for H being removeVertex of G, v st v is isolated
holds VertexAdjSymRel(H) = VertexAdjSymRel(G);
theorem :: GLUNIR00:55
for V being set, H being addVertices of G, V
holds VertexAdjSymRel(H) = VertexAdjSymRel(G);
theorem :: GLUNIR00:56
for v, w being Vertex of G, e being object, H being addEdge of G,v,e,w
st v,w are_adjacent holds VertexAdjSymRel(H) = VertexAdjSymRel(G);
theorem :: GLUNIR00:57
for v, w being Vertex of G, e being object, H being addEdge of G,v,e,w
st not e in the_Edges_of G
holds VertexAdjSymRel(H) = VertexAdjSymRel(G) \/ {[v,w], [w,v]};
theorem :: GLUNIR00:58
for v being Vertex of G, e,w being object, H being addAdjVertex of G,v,e,w
st not e in the_Edges_of G & not w in the_Vertices_of G
holds VertexAdjSymRel(H) = VertexAdjSymRel(G) \/ {[v,w], [w,v]};
theorem :: GLUNIR00:59
for v,e being object, w being Vertex of G, H being addAdjVertex of G,v,e,w
st not e in the_Edges_of G & not v in the_Vertices_of G
holds VertexAdjSymRel(H) = VertexAdjSymRel(G) \/ {[v,w], [w,v]};
theorem :: GLUNIR00:60
for v being object, V being Subset of the_Vertices_of G
for H being addAdjVertexAll of G,v,V st not v in the_Vertices_of G
holds VertexAdjSymRel(H) = VertexAdjSymRel(G) \/ [: {v},V :] \/ [: V,{v} :];
theorem :: GLUNIR00:61
for V being Subset of the_Vertices_of G, H being addLoops of G, V
holds VertexAdjSymRel(H) = VertexAdjSymRel(G) \/ id V;
theorem :: GLUNIR00:62
for H being LGraphComplement of G holds VertexAdjSymRel(H)
= [: the_Vertices_of G, the_Vertices_of G :] \ VertexAdjSymRel(G);
begin :: Create non-Dmulti Graphs from Relations
reserve V for non empty set, E for Relation of V;
definition
let V, E;
func createGraph(V,E) -> _Graph equals
:: GLUNIR00:def 3
createGraph(V, E, pr1(V,V) | E, pr2(V,V) | E);
end;
registration
let V, E;
cluster the_Edges_of createGraph(V,E) -> Relation-like;
end;
theorem :: GLUNIR00:63
for v,w being object holds [v,w] in E iff [v,w] DJoins v,w,createGraph(V,E);
theorem :: GLUNIR00:64
for e,v,w being object st e DJoins v,w,createGraph(V,E) holds e = [v,w];
theorem :: GLUNIR00:65
VertexDomRel(createGraph(V,E)) = E;
registration let V, E;
reduce VertexDomRel createGraph(V,E) to E;
end;
registration
let V, E;
cluster createGraph(V,E) -> plain non-Dmulti;
end;
theorem :: GLUNIR00:66
V is trivial iff createGraph(V,E) is _trivial;
registration
let V be trivial non empty set; let E be Relation of V;
cluster createGraph(V,E) -> _trivial;
end;
registration
let V be non trivial set; let E be Relation of V;
cluster createGraph(V,E) -> non _trivial;
end;
theorem :: GLUNIR00:67
E is irreflexive iff createGraph(V,E) is loopless;
registration
let V; let E be irreflexive Relation of V;
cluster createGraph(V,E) -> loopless;
end;
registration
let V; let E be non irreflexive Relation of V;
cluster createGraph(V,E) -> non loopless;
end;
theorem :: GLUNIR00:68
E is antisymmetric iff createGraph(V,E) is non-multi;
registration
let V; let E be antisymmetric Relation of V;
cluster createGraph(V,E) -> non-multi;
end;
registration
let V be non trivial set; let E be non antisymmetric Relation of V;
cluster createGraph(V,E) -> non non-multi;
end;
registration
let V; let E be asymmetric Relation of V;
cluster createGraph(V,E) -> simple;
end;
theorem :: GLUNIR00:69
createGraph(V,E) is complete implies E is connected;
registration
let V be non trivial set; let E be non connected Relation of V;
cluster createGraph(V,E) -> non complete;
end;
theorem :: GLUNIR00:70
E is empty iff createGraph(V,E) is edgeless;
registration
let V; let E be empty Relation of V;
cluster createGraph(V,E) -> edgeless;
end;
registration
let V; let E be non empty Relation of V;
cluster createGraph(V,E) -> non edgeless;
end;
theorem :: GLUNIR00:71
E is total reflexive iff createGraph(V,E) is loopfull;
registration
let V; let E be total reflexive Relation of V;
cluster createGraph(V,E) -> loopfull;
end;
registration
let V; let E be non total Relation of V;
cluster createGraph(V,E) -> non loopfull;
end;
registration
let V be finite non empty set, E be Relation of V;
cluster createGraph(V,E) -> finite;
end;
registration
let V; let E be finite Relation of V;
cluster createGraph(V,E) -> edge-finite;
end;
theorem :: GLUNIR00:72
for v being Vertex of createGraph(V,E) holds Im(E,v) = v.outNeighbors();
theorem :: GLUNIR00:73
for v being Vertex of createGraph(V,E) holds Coim(E,v) = v.inNeighbors();
theorem :: GLUNIR00:74
for X being set holds E|X = createGraph(V,E).edgesOutOf(X);
theorem :: GLUNIR00:75
for Y being set holds Y|`E = createGraph(V,E).edgesInto(Y);
theorem :: GLUNIR00:76
for X,Y being set holds Y|`E|X = createGraph(V,E).edgesDBetween(X,Y);
theorem :: GLUNIR00:77
for X,Y being set
holds Y|`E|X \/ X|`E|Y = createGraph(V,E).edgesBetween(X,Y);
theorem :: GLUNIR00:78
for v being Vertex of createGraph(V,E) holds E|{v} = v.edgesOut();
theorem :: GLUNIR00:79
for v being Vertex of createGraph(V,E) holds {v}|`E = v.edgesIn();
theorem :: GLUNIR00:80
for X being set holds E|X \/ X|`E = createGraph(V,E).edgesInOut(X);
theorem :: GLUNIR00:81
dom E = rng the_Source_of createGraph(V,E);
theorem :: GLUNIR00:82
rng E = rng the_Target_of createGraph(V,E);
theorem :: GLUNIR00:83
for v being Vertex of createGraph(V,E)
holds v is isolated iff not v in field E;
theorem :: GLUNIR00:84
E is symmetric iff VertexAdjSymRel(createGraph(V,E)) = E;
theorem :: GLUNIR00:85
for V1 being non empty set, V2 being non empty Subset of V1
for E1 being (Relation of V1), E2 being Relation of V2 st E2 c= E1
holds createGraph(V2,E2) is inducedSubgraph of createGraph(V1,E1),V2,E2;
theorem :: GLUNIR00:86
for G being non-Dmulti _Graph
ex F being PGraphMapping of G, createGraph(the_Vertices_of G,VertexDomRel(G))
st F is Disomorphism & F_V = id the_Vertices_of G &
for e being object st e in the_Edges_of G
holds F_E.e = [(the_Source_of G).e,(the_Target_of G).e];
theorem :: GLUNIR00:87
for G being non-Dmulti _Graph
holds createGraph(the_Vertices_of G,VertexDomRel(G)) is G-Disomorphic;
:: Using the isomorphism predicate from WELLORD1:def 8 we could
:: also write something like the graphs created from isomorphic relations
:: are Disomorphic. However, since the relations can only capture edges
:: the number of isolated vertices in both graphs may differ, depending
:: the underlying sets V1 and V2 of which E1 and E2 are relations of.
:: Therefore, such a theorem is better written after functors
:: changing RelStrs to _Graphs are introduced in a later article.
begin :: create non-multi Graphs from symmetric Relations
reserve E for symmetric Relation of V;
definition
let V, E;
mode GraphFromSymRel of V, E is removeParallelEdges of createGraph(V,E);
end;
reserve G for GraphFromSymRel of V, E;
theorem :: GLUNIR00:88
for v,w being object
holds [v,w] in E iff [v,w] DJoins v,w,G or [w,v] DJoins w,v,G;
theorem :: GLUNIR00:89
for v, w being Vertex of G holds [v,w] in E iff v,w are_adjacent;
registration
let V, E;
cluster -> non-multi for GraphFromSymRel of V, E;
end;
theorem :: GLUNIR00:90
the_Edges_of G c= E;
theorem :: GLUNIR00:91
for G1, G2 being GraphFromSymRel of V, E
holds the_Vertices_of G1 = the_Vertices_of G2;
theorem :: GLUNIR00:92
for G1, G2 being GraphFromSymRel of V, E holds G2 is G1-isomorphic;
theorem :: GLUNIR00:93
V is trivial iff G is _trivial;
registration
let V be trivial non empty set; let E be symmetric Relation of V;
cluster -> _trivial for GraphFromSymRel of V, E;
end;
registration
let V be non trivial set; let E be symmetric Relation of V;
cluster -> non _trivial for GraphFromSymRel of V, E;
end;
theorem :: GLUNIR00:94
E is irreflexive iff G is loopless;
registration
let V; let E be symmetric irreflexive Relation of V;
cluster -> loopless for GraphFromSymRel of V, E;
end;
registration
let V; let E be symmetric non irreflexive Relation of V;
cluster -> non loopless for GraphFromSymRel of V, E;
end;
theorem :: GLUNIR00:95
G is complete implies E is connected;
registration
let V be non trivial set; let E be symmetric non connected Relation of V;
cluster -> non complete for GraphFromSymRel of V, E;
end;
theorem :: GLUNIR00:96
E is empty iff G is edgeless;
registration
let V; let E be empty Relation of V;
cluster -> edgeless for GraphFromSymRel of V, E;
end;
registration
let V; let E be symmetric non empty Relation of V;
cluster -> non edgeless for GraphFromSymRel of V, E;
end;
theorem :: GLUNIR00:97
E is total reflexive iff G is loopfull;
registration
let V; let E be total reflexive symmetric Relation of V;
cluster -> loopfull for GraphFromSymRel of V, E;
end;
registration
let V; let E be symmetric non total Relation of V;
cluster -> non loopfull for GraphFromSymRel of V, E;
end;
registration
let V be finite non empty set, E be symmetric Relation of V;
cluster -> finite for GraphFromSymRel of V, E;
end;
theorem :: GLUNIR00:98
for v being Vertex of G holds Im(E,v) = v.allNeighbors();
theorem :: GLUNIR00:99
for X being set holds G.edgesInOut(X) c= (E|X) \/ (X|`E);
theorem :: GLUNIR00:100
for X, Y being set holds G.edgesBetween(X,Y) c= Y|`E|X \/ X|`E|Y;
::theorem
:: for v being Vertex of G holds card(E|{v}) = card(v.edgesInOut());
theorem :: GLUNIR00:101
for v being Vertex of G holds v.edgesOut() c= E|{v};
theorem :: GLUNIR00:102
for v being Vertex of G holds v.edgesIn() c= {v}|`E;
theorem :: GLUNIR00:103
for v being Vertex of G holds v is isolated iff not v in field E;
theorem :: GLUNIR00:104
for G being GraphFromSymRel of V, E holds VertexAdjSymRel(G) = E;
theorem :: GLUNIR00:105
for V1 being non empty set, V2 being non empty Subset of V1
for E1 being symmetric Relation of V1 for E2 being symmetric Relation of V2
for G1 being GraphFromSymRel of V1, E1, G2 being GraphFromSymRel of V2, E2
st E2 c= E1
ex F being PGraphMapping of G2, G1
st F is weak_SG-embedding & F_V = id V2 &
for v,w being object st [v,w] in the_Edges_of G2
holds F_E.[v,w] = [v,w] or F_E.[v,w] = [w,v];
theorem :: GLUNIR00:106
for G1 being non-multi _Graph
for G2 being GraphFromSymRel of the_Vertices_of G1, VertexAdjSymRel(G1)
ex F being PGraphMapping of G1, G2
st F is isomorphism & F_V = id the_Vertices_of G1 &
for e being object st e in the_Edges_of G1
holds F_E.e = [(the_Source_of G1).e,(the_Target_of G1).e] or
F_E.e = [(the_Target_of G1).e,(the_Source_of G1).e];
theorem :: GLUNIR00:107
for G1 being non-multi _Graph
for G2 being GraphFromSymRel of the_Vertices_of G1, VertexAdjSymRel(G1)
holds G2 is G1-isomorphic;