:: by Sebastian Koch

::

:: Received May 31, 2020

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

definition

let G be _Graph;

((the_Source_of G) ~) * (the_Target_of G) is Relation of (the_Vertices_of G)

end;
func VertexDomRel G -> Relation of (the_Vertices_of G) equals :: GLUNIR00:def 1

((the_Source_of G) ~) * (the_Target_of G);

coherence ((the_Source_of G) ~) * (the_Target_of G);

((the_Source_of G) ~) * (the_Target_of G) is Relation of (the_Vertices_of G)

proof end;

:: deftheorem defines VertexDomRel GLUNIR00:def 1 :

for G being _Graph holds VertexDomRel G = ((the_Source_of G) ~) * (the_Target_of G);

for G being _Graph holds VertexDomRel G = ((the_Source_of G) ~) * (the_Target_of G);

theorem Th1: :: GLUNIR00:1

for G being _Graph

for v, w being object holds

( [v,w] in VertexDomRel G iff ex e being object st e DJoins v,w,G )

for v, w being object holds

( [v,w] in VertexDomRel G iff ex e being object st e DJoins v,w,G )

proof end;

theorem Th2: :: GLUNIR00:2

for G being _Graph

for v, w being object holds

( [v,w] in (VertexDomRel G) ~ iff ex e being object st e DJoins w,v,G )

for v, w being object holds

( [v,w] in (VertexDomRel G) ~ iff ex e being object st e DJoins w,v,G )

proof end;

Lm1: for G being _Graph holds

( G is loopless iff VertexDomRel G misses id (the_Vertices_of G) )

proof end;

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

not VertexDomRel G is asymmetric

( e1 DJoins x,y,G & e2 DJoins y,x,G ) holds

not VertexDomRel G is asymmetric

proof end;

registration
end;

:: means G is then without isolated vertices

theorem Th5: :: GLUNIR00:5

for G being loopless _Graph st field (VertexDomRel G) = the_Vertices_of G holds

for C being Component of G holds not C is _trivial

for C being Component of G holds not C is _trivial

proof end;

:: means if G is without isolated vertices

theorem Th6: :: GLUNIR00:6

for G being _Graph st ( for C being Component of G holds not C is _trivial ) holds

field (VertexDomRel G) = the_Vertices_of G

field (VertexDomRel G) = the_Vertices_of G

proof end;

::registration

:: let G be non complete without_isolated_vertices _Graph;

:: cluster VertexDomRel(G) -> non connected;

:: coherence;

::end;

:: let G be non complete without_isolated_vertices _Graph;

:: cluster VertexDomRel(G) -> non connected;

:: coherence;

::end;

registration
end;

Lm2: for G being _Graph holds

( G is loopfull iff id (the_Vertices_of G) c= VertexDomRel G )

proof end;

theorem Th9: :: GLUNIR00:9

for G being _Graph holds

( G is loopfull iff ( VertexDomRel G is total & VertexDomRel G is reflexive ) )

( G is loopfull iff ( VertexDomRel G is total & VertexDomRel G is reflexive ) )

proof end;

registration

let G be loopfull _Graph;

coherence

( VertexDomRel G is reflexive & VertexDomRel G is total ) by Th9;

end;
coherence

( VertexDomRel G is reflexive & VertexDomRel G is total ) by Th9;

::registration

:: let G be non loopfull without_isolated_vertices _Graph;

:: cluster VertexDomRel(G) -> non reflexive;

:: coherence;

::end;

:: let G be non loopfull without_isolated_vertices _Graph;

:: cluster VertexDomRel(G) -> non reflexive;

:: coherence;

::end;

theorem Th17: :: GLUNIR00:17

for G being _Graph

for H being removeLoops of G holds VertexDomRel H = (VertexDomRel G) \ (id (the_Vertices_of G))

for H being removeLoops of G holds VertexDomRel H = (VertexDomRel G) \ (id (the_Vertices_of G))

proof end;

theorem :: GLUNIR00:18

for G being _Graph

for H being DSimpleGraph of G holds VertexDomRel H = (VertexDomRel G) \ (id (the_Vertices_of G))

for H being DSimpleGraph of G holds VertexDomRel H = (VertexDomRel G) \ (id (the_Vertices_of G))

proof end;

theorem Th21: :: GLUNIR00:21

for G being _Graph

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

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

proof end;

theorem Th22: :: GLUNIR00:22

for G being _Graph

for V being set

for 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:])

for V being set

for 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:])

proof end;

theorem Th23: :: GLUNIR00:23

for G being non _trivial _Graph

for 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}:])

for 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}:])

proof end;

theorem Th24: :: GLUNIR00:24

for G being non _trivial _Graph

for v being Vertex of G

for H being removeVertex of G,v st v is isolated holds

VertexDomRel H = VertexDomRel G

for v being Vertex of G

for H being removeVertex of G,v st v is isolated holds

VertexDomRel H = VertexDomRel G

proof end;

theorem Th25: :: GLUNIR00:25

for G being _Graph

for V being set

for H being addVertices of G,V holds VertexDomRel H = VertexDomRel G

for V being set

for H being addVertices of G,V holds VertexDomRel H = VertexDomRel G

proof end;

theorem Th26: :: GLUNIR00:26

for G being _Graph

for v, e, w being object

for H being addEdge of G,v,e,w st ex e0 being object st e0 DJoins v,w,G holds

VertexDomRel H = VertexDomRel G

for v, e, w being object

for H being addEdge of G,v,e,w st ex e0 being object st e0 DJoins v,w,G holds

VertexDomRel H = VertexDomRel G

proof end;

theorem Th27: :: GLUNIR00:27

for G being _Graph

for v, w being Vertex of G

for e being object

for H being addEdge of G,v,e,w st not e in the_Edges_of G holds

VertexDomRel H = (VertexDomRel G) \/ {[v,w]}

for v, w being Vertex of G

for e being object

for H being addEdge of G,v,e,w st not e in the_Edges_of G holds

VertexDomRel H = (VertexDomRel G) \/ {[v,w]}

proof end;

theorem :: GLUNIR00:28

for G being _Graph

for v being Vertex of G

for e, w being object

for 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]}

for v being Vertex of G

for e, w being object

for 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]}

proof end;

theorem :: GLUNIR00:29

for G being _Graph

for v, e being object

for w being Vertex of G

for 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]}

for v, e being object

for w being Vertex of G

for 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]}

proof end;

:: 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} :];

:: 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 Th30: :: GLUNIR00:30

for G being _Graph

for V being Subset of (the_Vertices_of G)

for H being addLoops of G,V holds VertexDomRel H = (VertexDomRel G) \/ (id V)

for V being Subset of (the_Vertices_of G)

for H being addLoops of G,V holds VertexDomRel H = (VertexDomRel G) \/ (id V)

proof end;

theorem :: GLUNIR00:31

for G being _Graph

for H being DLGraphComplement of G holds VertexDomRel H = [:(the_Vertices_of G),(the_Vertices_of G):] \ (VertexDomRel G)

for H being DLGraphComplement of G holds VertexDomRel H = [:(the_Vertices_of G),(the_Vertices_of G):] \ (VertexDomRel G)

proof end;

definition

let G be _Graph;

(VertexDomRel G) \/ ((VertexDomRel G) ~) is Relation of (the_Vertices_of G) ;

end;
func VertexAdjSymRel G -> Relation of (the_Vertices_of G) equals :: GLUNIR00:def 2

(VertexDomRel G) \/ ((VertexDomRel G) ~);

coherence (VertexDomRel G) \/ ((VertexDomRel G) ~);

(VertexDomRel G) \/ ((VertexDomRel G) ~) is Relation of (the_Vertices_of G) ;

:: deftheorem defines VertexAdjSymRel GLUNIR00:def 2 :

for G being _Graph holds VertexAdjSymRel G = (VertexDomRel G) \/ ((VertexDomRel G) ~);

for G being _Graph holds VertexAdjSymRel G = (VertexDomRel G) \/ ((VertexDomRel G) ~);

theorem Th32: :: GLUNIR00:32

for G being _Graph

for v, w being object holds

( [v,w] in VertexAdjSymRel G iff ex e being object st e Joins v,w,G )

for v, w being object holds

( [v,w] in VertexAdjSymRel G iff ex e being object st e Joins v,w,G )

proof end;

theorem Th33: :: GLUNIR00:33

for G being _Graph

for v, w being Vertex of G holds

( [v,w] in VertexAdjSymRel G iff v,w are_adjacent )

for v, w being Vertex of G holds

( [v,w] in VertexAdjSymRel G iff v,w are_adjacent )

proof end;

theorem :: GLUNIR00:35

for G being _Graph holds VertexAdjSymRel G = (((the_Source_of G) ~) * (the_Target_of G)) \/ (((the_Target_of G) ~) * (the_Source_of G))

proof end;

Lm3: for G being _Graph holds

( G is loopless iff VertexAdjSymRel G misses id (the_Vertices_of G) )

proof end;

registration
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 not C is _trivial

for C being Component of G holds not C is _trivial

proof end;

:: means if G is without isolated vertices

theorem Th38: :: GLUNIR00:38

for G being _Graph st ( for C being Component of G holds not C is _trivial ) holds

VertexAdjSymRel G is total

VertexAdjSymRel G is total

proof end;

registration
end;

:: registration

:: let G be non complete without_isolated_vertices _Graph;

:: cluster VertexAdjSymRel(G) -> non connected;

:: coherence;

:: end;

:: let G be non complete without_isolated_vertices _Graph;

:: cluster VertexAdjSymRel(G) -> non connected;

:: coherence;

:: end;

Lm4: for G being _Graph holds

( G is loopfull iff id (the_Vertices_of G) c= VertexAdjSymRel G )

proof end;

theorem Th40: :: GLUNIR00:40

for G being _Graph holds

( G is loopfull iff ( VertexAdjSymRel G is total & VertexAdjSymRel G is reflexive ) )

( G is loopfull iff ( VertexAdjSymRel G is total & VertexAdjSymRel G is reflexive ) )

proof end;

registration

let G be loopfull _Graph;

coherence

( VertexAdjSymRel G is reflexive & VertexAdjSymRel G is total ) by Th40;

end;
coherence

( VertexAdjSymRel G is reflexive & VertexAdjSymRel G is total ) by Th40;

:: registration

:: let G be non loopfull without_isolated_vertices _Graph;

:: cluster VertexAdjSymRel(G) -> non reflexive;

:: coherence;

:: end;

:: let G be non loopfull without_isolated_vertices _Graph;

:: cluster VertexAdjSymRel(G) -> non reflexive;

:: coherence;

:: end;

theorem Th47: :: GLUNIR00:47

for G being _Graph

for H being removeLoops of G holds VertexAdjSymRel H = (VertexAdjSymRel G) \ (id (the_Vertices_of G))

for H being removeLoops of G holds VertexAdjSymRel H = (VertexAdjSymRel G) \ (id (the_Vertices_of G))

proof end;

theorem :: GLUNIR00:48

for G being _Graph

for H being SimpleGraph of G holds VertexAdjSymRel H = (VertexAdjSymRel G) \ (id (the_Vertices_of G))

for H being SimpleGraph of G holds VertexAdjSymRel H = (VertexAdjSymRel G) \ (id (the_Vertices_of G))

proof end;

theorem :: GLUNIR00:50

for G being _Graph

for E being set

for H being reverseEdgeDirections of G,E holds VertexAdjSymRel H = VertexAdjSymRel G

for E being set

for H being reverseEdgeDirections of G,E holds VertexAdjSymRel H = VertexAdjSymRel G

proof end;

theorem :: GLUNIR00:51

for G being _Graph

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

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

proof end;

theorem Th52: :: GLUNIR00:52

for G being _Graph

for V being set

for 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:])

for V being set

for 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:])

proof end;

theorem :: GLUNIR00:53

for G being non _trivial _Graph

for 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}:])

for 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}:])

proof end;

theorem :: GLUNIR00:54

for G being non _trivial _Graph

for v being Vertex of G

for H being removeVertex of G,v st v is isolated holds

VertexAdjSymRel H = VertexAdjSymRel G

for v being Vertex of G

for H being removeVertex of G,v st v is isolated holds

VertexAdjSymRel H = VertexAdjSymRel G

proof end;

theorem Th55: :: GLUNIR00:55

for G being _Graph

for V being set

for H being addVertices of G,V holds VertexAdjSymRel H = VertexAdjSymRel G

for V being set

for H being addVertices of G,V holds VertexAdjSymRel H = VertexAdjSymRel G

proof end;

theorem :: GLUNIR00:56

for G being _Graph

for v, w being Vertex of G

for e being object

for H being addEdge of G,v,e,w st v,w are_adjacent holds

VertexAdjSymRel H = VertexAdjSymRel G

for v, w being Vertex of G

for e being object

for H being addEdge of G,v,e,w st v,w are_adjacent holds

VertexAdjSymRel H = VertexAdjSymRel G

proof end;

theorem Th57: :: GLUNIR00:57

for G being _Graph

for v, w being Vertex of G

for e being object

for 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]}

for v, w being Vertex of G

for e being object

for 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]}

proof end;

theorem :: GLUNIR00:58

for G being _Graph

for v being Vertex of G

for e, w being object

for 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]}

for v being Vertex of G

for e, w being object

for 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]}

proof end;

theorem :: GLUNIR00:59

for G being _Graph

for v, e being object

for w being Vertex of G

for 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]}

for v, e being object

for w being Vertex of G

for 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]}

proof end;

theorem :: GLUNIR00:60

for G being _Graph

for v being object

for 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}:]

for v being object

for 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}:]

proof end;

theorem :: GLUNIR00:61

for G being _Graph

for V being Subset of (the_Vertices_of G)

for H being addLoops of G,V holds VertexAdjSymRel H = (VertexAdjSymRel G) \/ (id V)

for V being Subset of (the_Vertices_of G)

for H being addLoops of G,V holds VertexAdjSymRel H = (VertexAdjSymRel G) \/ (id V)

proof end;

theorem :: GLUNIR00:62

for G being _Graph

for H being LGraphComplement of G holds VertexAdjSymRel H = [:(the_Vertices_of G),(the_Vertices_of G):] \ (VertexAdjSymRel G)

for H being LGraphComplement of G holds VertexAdjSymRel H = [:(the_Vertices_of G),(the_Vertices_of G):] \ (VertexAdjSymRel G)

proof end;

definition

let V be non empty set ;

let E be Relation of V;

createGraph (V,E,((pr1 (V,V)) | E),((pr2 (V,V)) | E)) is _Graph ;

end;
let E be Relation of V;

func createGraph (V,E) -> _Graph equals :: GLUNIR00:def 3

createGraph (V,E,((pr1 (V,V)) | E),((pr2 (V,V)) | E));

coherence createGraph (V,E,((pr1 (V,V)) | E),((pr2 (V,V)) | E));

createGraph (V,E,((pr1 (V,V)) | E),((pr2 (V,V)) | E)) is _Graph ;

:: deftheorem defines createGraph GLUNIR00:def 3 :

for V being non empty set

for E being Relation of V holds createGraph (V,E) = createGraph (V,E,((pr1 (V,V)) | E),((pr2 (V,V)) | E));

for V being non empty set

for E being Relation of V holds createGraph (V,E) = createGraph (V,E,((pr1 (V,V)) | E),((pr2 (V,V)) | E));

registration

let V be non empty set ;

let E be Relation of V;

coherence

the_Edges_of (createGraph (V,E)) is Relation-like ;

end;
let E be Relation of V;

coherence

the_Edges_of (createGraph (V,E)) is Relation-like ;

theorem Th63: :: GLUNIR00:63

for V being non empty set

for E being Relation of V

for v, w being object holds

( [v,w] in E iff [v,w] DJoins v,w, createGraph (V,E) )

for E being Relation of V

for v, w being object holds

( [v,w] in E iff [v,w] DJoins v,w, createGraph (V,E) )

proof end;

theorem Th64: :: GLUNIR00:64

for V being non empty set

for E being Relation of V

for e, v, w being object st e DJoins v,w, createGraph (V,E) holds

e = [v,w]

for E being Relation of V

for e, v, w being object st e DJoins v,w, createGraph (V,E) holds

e = [v,w]

proof end;

registration

let V be non empty set ;

let E be Relation of V;

reducibility

VertexDomRel (createGraph (V,E)) = E by Th65;

end;
let E be Relation of V;

reducibility

VertexDomRel (createGraph (V,E)) = E by Th65;

registration

let V be non empty set ;

let E be Relation of V;

coherence

( createGraph (V,E) is plain & createGraph (V,E) is non-Dmulti )

end;
let E be Relation of V;

coherence

( createGraph (V,E) is plain & createGraph (V,E) is non-Dmulti )

proof end;

theorem Th66: :: GLUNIR00:66

for V being non empty set

for E being Relation of V holds

( V is trivial iff createGraph (V,E) is _trivial )

for E being Relation of V holds

( V is trivial iff createGraph (V,E) is _trivial )

proof end;

registration

let V be non empty trivial set ;

let E be Relation of V;

coherence

createGraph (V,E) is _trivial by Th66;

end;
let E be Relation of V;

coherence

createGraph (V,E) is _trivial by Th66;

registration

let V be non trivial set ;

let E be Relation of V;

coherence

not createGraph (V,E) is _trivial by Th66;

end;
let E be Relation of V;

coherence

not createGraph (V,E) is _trivial by Th66;

theorem Th67: :: GLUNIR00:67

for V being non empty set

for E being Relation of V holds

( E is irreflexive iff createGraph (V,E) is loopless )

for E being Relation of V holds

( E is irreflexive iff createGraph (V,E) is loopless )

proof end;

registration

let V be non empty set ;

let E be irreflexive Relation of V;

coherence

createGraph (V,E) is loopless by Th67;

end;
let E be irreflexive Relation of V;

coherence

createGraph (V,E) is loopless by Th67;

registration

let V be non empty set ;

let E be non irreflexive Relation of V;

coherence

not createGraph (V,E) is loopless by Th67;

end;
let E be non irreflexive Relation of V;

coherence

not createGraph (V,E) is loopless by Th67;

theorem Th68: :: GLUNIR00:68

for V being non empty set

for E being Relation of V holds

( E is antisymmetric iff createGraph (V,E) is non-multi )

for E being Relation of V holds

( E is antisymmetric iff createGraph (V,E) is non-multi )

proof end;

registration

let V be non empty set ;

let E be antisymmetric Relation of V;

coherence

createGraph (V,E) is non-multi by Th68;

end;
let E be antisymmetric Relation of V;

coherence

createGraph (V,E) is non-multi by Th68;

registration

let V be non trivial set ;

let E be non antisymmetric Relation of V;

coherence

not createGraph (V,E) is non-multi by Th68;

end;
let E be non antisymmetric Relation of V;

coherence

not createGraph (V,E) is non-multi by Th68;

registration
end;

theorem Th69: :: GLUNIR00:69

for V being non empty set

for E being Relation of V st createGraph (V,E) is complete holds

E is connected

for E being Relation of V st createGraph (V,E) is complete holds

E is connected

proof end;

registration

let V be non trivial set ;

let E be non connected Relation of V;

coherence

not createGraph (V,E) is complete by Th69;

end;
let E be non connected Relation of V;

coherence

not createGraph (V,E) is complete by Th69;

theorem Th70: :: GLUNIR00:70

for V being non empty set

for E being Relation of V holds

( E is empty iff createGraph (V,E) is edgeless )

for E being Relation of V holds

( E is empty iff createGraph (V,E) is edgeless )

proof end;

registration
end;

registration

let V be non empty set ;

let E be non empty Relation of V;

coherence

not createGraph (V,E) is edgeless by Th70;

end;
let E be non empty Relation of V;

coherence

not createGraph (V,E) is edgeless by Th70;

theorem Th71: :: GLUNIR00:71

for V being non empty set

for E being Relation of V holds

( ( E is total & E is reflexive ) iff createGraph (V,E) is loopfull )

for E being Relation of V holds

( ( E is total & E is reflexive ) iff createGraph (V,E) is loopfull )

proof end;

registration

let V be non empty set ;

let E be total reflexive Relation of V;

coherence

createGraph (V,E) is loopfull by Th71;

end;
let E be total reflexive Relation of V;

coherence

createGraph (V,E) is loopfull by Th71;

registration

let V be non empty set ;

let E be non total Relation of V;

coherence

not createGraph (V,E) is loopfull by Th71;

end;
let E be non total Relation of V;

coherence

not createGraph (V,E) is loopfull by Th71;

registration
end;

registration
end;

theorem Th72: :: GLUNIR00:72

for V being non empty set

for E being Relation of V

for v being Vertex of (createGraph (V,E)) holds Im (E,v) = v .outNeighbors()

for E being Relation of V

for v being Vertex of (createGraph (V,E)) holds Im (E,v) = v .outNeighbors()

proof end;

theorem Th73: :: GLUNIR00:73

for V being non empty set

for E being Relation of V

for v being Vertex of (createGraph (V,E)) holds Coim (E,v) = v .inNeighbors()

for E being Relation of V

for v being Vertex of (createGraph (V,E)) holds Coim (E,v) = v .inNeighbors()

proof end;

theorem Th74: :: GLUNIR00:74

for V being non empty set

for E being Relation of V

for X being set holds E | X = (createGraph (V,E)) .edgesOutOf X

for E being Relation of V

for X being set holds E | X = (createGraph (V,E)) .edgesOutOf X

proof end;

theorem Th75: :: GLUNIR00:75

for V being non empty set

for E being Relation of V

for Y being set holds Y |` E = (createGraph (V,E)) .edgesInto Y

for E being Relation of V

for Y being set holds Y |` E = (createGraph (V,E)) .edgesInto Y

proof end;

theorem Th76: :: GLUNIR00:76

for V being non empty set

for E being Relation of V

for X, Y being set holds (Y |` E) | X = (createGraph (V,E)) .edgesDBetween (X,Y)

for E being Relation of V

for X, Y being set holds (Y |` E) | X = (createGraph (V,E)) .edgesDBetween (X,Y)

proof end;

theorem Th77: :: GLUNIR00:77

for V being non empty set

for E being Relation of V

for X, Y being set holds ((Y |` E) | X) \/ ((X |` E) | Y) = (createGraph (V,E)) .edgesBetween (X,Y)

for E being Relation of V

for X, Y being set holds ((Y |` E) | X) \/ ((X |` E) | Y) = (createGraph (V,E)) .edgesBetween (X,Y)

proof end;

theorem Th78: :: GLUNIR00:78

for V being non empty set

for E being Relation of V

for v being Vertex of (createGraph (V,E)) holds E | {v} = v .edgesOut()

for E being Relation of V

for v being Vertex of (createGraph (V,E)) holds E | {v} = v .edgesOut()

proof end;

theorem Th79: :: GLUNIR00:79

for V being non empty set

for E being Relation of V

for v being Vertex of (createGraph (V,E)) holds {v} |` E = v .edgesIn()

for E being Relation of V

for v being Vertex of (createGraph (V,E)) holds {v} |` E = v .edgesIn()

proof end;

theorem Th80: :: GLUNIR00:80

for V being non empty set

for E being Relation of V

for X being set holds (E | X) \/ (X |` E) = (createGraph (V,E)) .edgesInOut X

for E being Relation of V

for X being set holds (E | X) \/ (X |` E) = (createGraph (V,E)) .edgesInOut X

proof end;

theorem :: GLUNIR00:81

for V being non empty set

for E being Relation of V holds dom E = rng (the_Source_of (createGraph (V,E)))

for E being Relation of V holds dom E = rng (the_Source_of (createGraph (V,E)))

proof end;

theorem :: GLUNIR00:82

for V being non empty set

for E being Relation of V holds rng E = rng (the_Target_of (createGraph (V,E)))

for E being Relation of V holds rng E = rng (the_Target_of (createGraph (V,E)))

proof end;

theorem Th83: :: GLUNIR00:83

for V being non empty set

for E being Relation of V

for v being Vertex of (createGraph (V,E)) holds

( v is isolated iff not v in field E )

for E being Relation of V

for v being Vertex of (createGraph (V,E)) holds

( v is isolated iff not v in field E )

proof end;

theorem :: GLUNIR00:84

for V being non empty set

for E being Relation of V holds

( E is symmetric iff VertexAdjSymRel (createGraph (V,E)) = E )

for E being Relation of V holds

( E is symmetric iff VertexAdjSymRel (createGraph (V,E)) = E )

proof end;

theorem :: GLUNIR00:85

for V1 being non empty set

for V2 being non empty Subset of V1

for E1 being Relation of V1

for E2 being Relation of V2 st E2 c= E1 holds

createGraph (V2,E2) is inducedSubgraph of createGraph (V1,E1),V2,E2

for V2 being non empty Subset of V1

for E1 being Relation of V1

for E2 being Relation of V2 st E2 c= E1 holds

createGraph (V2,E2) is inducedSubgraph of createGraph (V1,E1),V2,E2

proof end;

theorem Th86: :: 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)] ) )

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

proof end;

theorem :: GLUNIR00:87

for G being non-Dmulti _Graph holds createGraph ((the_Vertices_of G),(VertexDomRel G)) is G -Disomorphic

proof end;

definition

let V be non empty set ;

let E be symmetric Relation of V;

mode GraphFromSymRel of V,E is removeParallelEdges of createGraph (V,E);

end;
let E be symmetric Relation of V;

mode GraphFromSymRel of V,E is removeParallelEdges of createGraph (V,E);

theorem Th88: :: GLUNIR00:88

for V being non empty set

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E

for v, w being object holds

( [v,w] in E iff ( [v,w] DJoins v,w,G or [w,v] DJoins w,v,G ) )

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E

for v, w being object holds

( [v,w] in E iff ( [v,w] DJoins v,w,G or [w,v] DJoins w,v,G ) )

proof end;

theorem Th89: :: GLUNIR00:89

for V being non empty set

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E

for v, w being Vertex of G holds

( [v,w] in E iff v,w are_adjacent )

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E

for v, w being Vertex of G holds

( [v,w] in E iff v,w are_adjacent )

proof end;

registration

let V be non empty set ;

let E be symmetric Relation of V;

coherence

for b_{1} being GraphFromSymRel of V,E holds b_{1} is non-multi
;

end;
let E be symmetric Relation of V;

coherence

for b

theorem :: GLUNIR00:90

for V being non empty set

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E holds the_Edges_of G c= E ;

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E holds the_Edges_of G c= E ;

theorem :: GLUNIR00:91

for V being non empty set

for E being symmetric Relation of V

for G1, G2 being GraphFromSymRel of V,E holds the_Vertices_of G1 = the_Vertices_of G2

for E being symmetric Relation of V

for G1, G2 being GraphFromSymRel of V,E holds the_Vertices_of G1 = the_Vertices_of G2

proof end;

theorem :: GLUNIR00:92

for V being non empty set

for E being symmetric Relation of V

for G1, G2 being GraphFromSymRel of V,E holds G2 is G1 -isomorphic by GLIB_010:169;

for E being symmetric Relation of V

for G1, G2 being GraphFromSymRel of V,E holds G2 is G1 -isomorphic by GLIB_010:169;

theorem :: GLUNIR00:93

registration

let V be non empty trivial set ;

let E be symmetric Relation of V;

coherence

for b_{1} being GraphFromSymRel of V,E holds b_{1} is _trivial
;

end;
let E be symmetric Relation of V;

coherence

for b

registration

let V be non trivial set ;

let E be symmetric Relation of V;

coherence

for b_{1} being GraphFromSymRel of V,E holds not b_{1} is _trivial
;

end;
let E be symmetric Relation of V;

coherence

for b

theorem :: GLUNIR00:94

for V being non empty set

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E holds

( E is irreflexive iff G is loopless ) ;

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E holds

( E is irreflexive iff G is loopless ) ;

registration

let V be non empty set ;

let E be irreflexive symmetric Relation of V;

coherence

for b_{1} being GraphFromSymRel of V,E holds b_{1} is loopless
;

end;
let E be irreflexive symmetric Relation of V;

coherence

for b

registration

let V be non empty set ;

let E be non irreflexive symmetric Relation of V;

coherence

for b_{1} being GraphFromSymRel of V,E holds not b_{1} is loopless
;

end;
let E be non irreflexive symmetric Relation of V;

coherence

for b

theorem :: GLUNIR00:95

for V being non empty set

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E st G is complete holds

E is connected

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E st G is complete holds

E is connected

proof end;

registration

let V be non trivial set ;

let E be symmetric non connected Relation of V;

coherence

for b_{1} being GraphFromSymRel of V,E holds not b_{1} is complete
;

end;
let E be symmetric non connected Relation of V;

coherence

for b

theorem :: GLUNIR00:96

registration

let V be non empty set ;

let E be empty Relation of V;

coherence

for b_{1} being GraphFromSymRel of V,E holds b_{1} is edgeless
;

end;
let E be empty Relation of V;

coherence

for b

registration

let V be non empty set ;

let E be non empty symmetric Relation of V;

coherence

for b_{1} being GraphFromSymRel of V,E holds not b_{1} is edgeless
;

end;
let E be non empty symmetric Relation of V;

coherence

for b

theorem :: GLUNIR00:97

for V being non empty set

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E holds

( ( E is total & E is reflexive ) iff G is loopfull )

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E holds

( ( E is total & E is reflexive ) iff G is loopfull )

proof end;

registration

let V be non empty set ;

let E be total reflexive symmetric Relation of V;

coherence

for b_{1} being GraphFromSymRel of V,E holds b_{1} is loopfull
;

end;
let E be total reflexive symmetric Relation of V;

coherence

for b

registration

let V be non empty set ;

let E be non total symmetric Relation of V;

coherence

for b_{1} being GraphFromSymRel of V,E holds not b_{1} is loopfull
;

end;
let E be non total symmetric Relation of V;

coherence

for b

registration

let V be non empty finite set ;

let E be symmetric Relation of V;

coherence

for b_{1} being GraphFromSymRel of V,E holds b_{1} is finite
;

end;
let E be symmetric Relation of V;

coherence

for b

theorem :: GLUNIR00:98

for V being non empty set

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E

for v being Vertex of G holds Im (E,v) = v .allNeighbors()

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E

for v being Vertex of G holds Im (E,v) = v .allNeighbors()

proof end;

theorem :: GLUNIR00:99

for V being non empty set

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E

for X being set holds G .edgesInOut X c= (E | X) \/ (X |` E)

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E

for X being set holds G .edgesInOut X c= (E | X) \/ (X |` E)

proof end;

theorem :: GLUNIR00:100

for V being non empty set

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E

for X, Y being set holds G .edgesBetween (X,Y) c= ((Y |` E) | X) \/ ((X |` E) | Y)

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E

for X, Y being set holds G .edgesBetween (X,Y) c= ((Y |` E) | X) \/ ((X |` E) | Y)

proof end;

::theorem

:: for v being Vertex of G holds card(E|{v}) = card(v.edgesInOut());

:: for v being Vertex of G holds card(E|{v}) = card(v.edgesInOut());

theorem :: GLUNIR00:101

for V being non empty set

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E

for v being Vertex of G holds v .edgesOut() c= E | {v}

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E

for v being Vertex of G holds v .edgesOut() c= E | {v}

proof end;

theorem :: GLUNIR00:102

for V being non empty set

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E

for v being Vertex of G holds v .edgesIn() c= {v} |` E

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E

for v being Vertex of G holds v .edgesIn() c= {v} |` E

proof end;

theorem :: GLUNIR00:103

for V being non empty set

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E

for v being Vertex of G holds

( v is isolated iff not v in field E )

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E

for v being Vertex of G holds

( v is isolated iff not v in field E )

proof end;

theorem :: GLUNIR00:104

for V being non empty set

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E holds VertexAdjSymRel G = E

for E being symmetric Relation of V

for G being GraphFromSymRel of V,E holds VertexAdjSymRel G = E

proof end;

theorem :: GLUNIR00:105

for V1 being non empty set

for 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

for G2 being GraphFromSymRel of V2,E2 st E2 c= E1 holds

ex F being PGraphMapping of G2,G1 st

( F is weak_SG-embedding & F _V = id V2 & ( for v, w being object holds

( not [v,w] in the_Edges_of G2 or (F _E) . [v,w] = [v,w] or (F _E) . [v,w] = [w,v] ) ) )

for 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

for G2 being GraphFromSymRel of V2,E2 st E2 c= E1 holds

ex F being PGraphMapping of G2,G1 st

( F is weak_SG-embedding & F _V = id V2 & ( for v, w being object holds

( not [v,w] in the_Edges_of G2 or (F _E) . [v,w] = [v,w] or (F _E) . [v,w] = [w,v] ) ) )

proof end;

theorem Th106: :: 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 holds

( not e in the_Edges_of G1 or (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)] ) ) )

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 holds

( not e in the_Edges_of G1 or (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)] ) ) )

proof end;

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

for G2 being GraphFromSymRel of (the_Vertices_of G1),(VertexAdjSymRel G1) holds G2 is G1 -isomorphic

proof end;