:: Miscellaneous Graph Preliminaries
:: by Sebastian Koch
::
:: Received December 30, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users

:: generalization of XBOOLE_1:45
:: into XBOOLE_1 ?

theorem :: GLIBPRE0:1

for X, Y, Z being set st Z c= X holds
X \/ (Y \ Z) = X \/ Y

proof end;

:: generalization of XBOOLE_1:89
:: into XBOOLE_1 ?

theorem Th2: :: GLIBPRE0:2

for X, Y, Z being set holds X /\ Z misses Y \ Z

proof end;

:: into ZFMISC_1 ?

theorem :: GLIBPRE0:3

for x, y being object holds
( {x,y} \ { the Element of {x,y}} = {} iff x = y )

proof end;

:: into ZFMISC_1 ?

theorem :: GLIBPRE0:4

for a, b, x, y being object st a <> b & x = the Element of {a,b} & y = the Element of {a,b} \ { the Element of {a,b}} & not ( x = a & y = b ) holds
( x = b & y = a )

proof end;

:: into ZFMISC_1 ?

theorem :: GLIBPRE0:5

for a, b, x, y being object holds
( {a,b} = {x,y} iff ( ( x = a & y = b ) or ( x = b & y = a ) ) ) by ZFMISC_1:22;

:: into SUBSET_1 ?

theorem :: GLIBPRE0:6

for X being set
for Y being non empty set holds
( X c< Y iff X is proper Subset of Y ) by SUBSET_1:def 6, XBOOLE_0:def 8;

registration

let X be non empty set ;

cluster id X -> non irreflexive ;

coherence
not id X is irreflexive

proof end;

cluster [:X,X:] -> non irreflexive non asymmetric ;

coherence
( not [:X,X:] is irreflexive & not [:X,X:] is asymmetric )

proof end;

cluster Relation-like X -defined X -valued non irreflexive non asymmetric for Element of bool [:X,X:];

existence
ex b₁ being Relation of X st
( not b₁ is irreflexive & not b₁ is asymmetric )

proof end;

cluster Relation-like X -defined X -valued non total irreflexive symmetric for Element of bool [:X,X:];

existence
ex b₁ being Relation of X st
( b₁ is symmetric & b₁ is irreflexive & not b₁ is total )

proof end;

cluster non empty Relation-like X -defined X -valued non irreflexive symmetric for Element of bool [:X,X:];

existence
ex b₁ being Relation of X st
( b₁ is symmetric & not b₁ is irreflexive & not b₁ is empty )

proof end;

end;

registration

let X be non trivial set ;

cluster id X -> non connected ;

coherence
not id X is connected

proof end;

cluster Relation-like X -defined X -valued symmetric non connected for Element of bool [:X,X:];

existence
ex b₁ being Relation of X st
( b₁ is symmetric & not b₁ is connected )

proof end;

cluster [:X,X:] -> non antisymmetric ;

coherence
not [:X,X:] is antisymmetric

proof end;

cluster Relation-like X -defined X -valued non antisymmetric for Element of bool [:X,X:];

existence
not for b₁ being Relation of X holds b₁ is antisymmetric

proof end;

end;

:: into RELAT_1 ?

theorem :: GLIBPRE0:7

for R, S being Relation
for X being set holds (R \/ S) .: X = (R .: X) \/ (S .: X)

proof end;

:: into RELAT_1 ?

theorem :: GLIBPRE0:8

for R, S being Relation
for Y being set holds (R \/ S) " Y = (R " Y) \/ (S " Y)

proof end;

:: into RELAT_1 ?

theorem :: GLIBPRE0:9

for R being Relation
for X, Y being set holds (Y |` R) | X = (Y |` R) /\ (R | X)

proof end;

:: into RELAT_2 ?

theorem :: GLIBPRE0:10

for R being symmetric Relation
for x being object holds Im (R,x) = Coim (R,x)

proof end;

:: into RELSET_1 ?

theorem :: GLIBPRE0:11

for X being set
for R being Relation of X holds
( R is irreflexive iff id X misses R )

proof end;

:: into ZFMISC_1 or SYSREL ? (in both cases the qua can be omitted)

theorem :: GLIBPRE0:12

for x, y being object holds {[x,y]} ~ = {[y,x]}

proof end;

:: generalization of EQREL_1:6 (total is unneeded assumption)
:: into EQREL_1 ?

theorem :: GLIBPRE0:13

for X being set
for x, y being object
for R being symmetric Relation of X st [x,y] in R holds
[y,x] in R

proof end;

:: into CARD_1 ?

registration

let a, b be Cardinal;

cluster a /\ b -> cardinal ;

coherence
a /\ b is cardinal by ORDINAL3:13;

cluster a \/ b -> cardinal ;

coherence
a \/ b is cardinal by ORDINAL3:12;

end;

:: into ORDINAL1 or WELLORD2 ?

registration

let X be c=-linear set ;

cluster RelIncl X -> connected ;

coherence
RelIncl X is connected

proof end;

end;

:: into YELLOW_1 or ORDERS_5 ?

registration

let X be c=-linear set ;

cluster InclPoset X -> connected ;

coherence
InclPoset X is connected

proof end;

end;

:: into CARD_1 ?

theorem Th15: :: GLIBPRE0:14

for X being non empty set st ( for a being set st a in X holds
a is cardinal number ) holds
ex A being Cardinal st
( A in X & A = meet X )

proof end;

:: analogous to TOPGEN_2:3
:: into CARD_1 ?

theorem :: GLIBPRE0:15

for X being set st ( for a being set st a in X holds
a is cardinal number ) holds
meet X is cardinal number

proof end;

:: into CARD_3 ?

registration

let f be Cardinal-yielding Function;
let x be object ;

cluster f . x -> cardinal ;

coherence
f . x is cardinal

proof end;

end;

Th19: for X being functional set holds meet X is Function

proof end;

registration

let X be functional set ;

cluster meet X -> Relation-like Function-like ;

coherence
( meet X is Function-like & meet X is Relation-like ) by Th19;

end;

:: into PENCIL_1 ?
:: mostly copied from there

theorem Th20: :: GLIBPRE0:16

for X being set holds
( 4 c= card X iff ex w, x, y, z being object st
( w in X & x in X & y in X & z in X & w <> x & w <> y & w <> z & x <> y & x <> z & y <> z ) )

proof end;

:: into PENCIL_1 ?

theorem Th21: :: GLIBPRE0:17

for X being set st 4 c= card X holds
for w, x, y being object ex z being object st
( z in X & w <> z & x <> z & y <> z )

proof end;

:: into BSPACE or SGRAPH1 ?

theorem :: GLIBPRE0:18

for X being set holds singletons X misses 2Set X

proof end;

:: into SGRAPH1 or MATRIX11 ?

theorem Th23: :: GLIBPRE0:19

for X, Y being set st card X = card Y holds
card (2Set X) = card (2Set Y)

proof end;

:: into MATRIX13 ?

theorem :: GLIBPRE0:20

for X being finite set holds card (2Set X) = (card X) choose 2

proof end;

theorem Th25: :: GLIBPRE0:21

for G being _Graph
for v being Vertex of G
for e, w being object st v is isolated holds
not e Joins v,w,G

proof end;

theorem Th26: :: GLIBPRE0:22

for G being _Graph
for v being Vertex of G
for e, w being object st v is isolated holds
( not e DJoins v,w,G & not e DJoins w,v,G )

proof end;

:: into GLIB_000 ?

theorem :: GLIBPRE0:23

for G being _Graph
for v being Vertex of G holds
( v is isolated iff not v in (rng (the_Source_of G)) \/ (rng (the_Target_of G)) )

proof end;

theorem :: GLIBPRE0:24

for G being _Graph
for v being Vertex of G
for e being object st v is endvertex holds
not e Joins v,v,G

proof end;

theorem :: GLIBPRE0:25

for G being _Graph
for v being Vertex of G holds
( v .edgesIn() = (the_Target_of G) " {v} & v .edgesOut() = (the_Source_of G) " {v} )

proof end;

theorem Th30: :: GLIBPRE0:26

for G being _trivial _Graph
for v being Vertex of G holds
( v .edgesIn() = the_Edges_of G & v .edgesOut() = the_Edges_of G & v .edgesInOut() = the_Edges_of G )

proof end;

theorem :: GLIBPRE0:27

for G being _trivial _Graph
for v being Vertex of G holds
( v .inDegree() = G .size() & v .outDegree() = G .size() & v .degree() = (G .size()) +` (G .size()) )

proof end;

theorem Th32: :: GLIBPRE0:28

for G being _Graph
for X, Y being set holds G .edgesBetween (X,Y) = (G .edgesDBetween (X,Y)) \/ (G .edgesDBetween (Y,X))

proof end;

theorem Th33: :: GLIBPRE0:29

for G being _Graph
for v being Vertex of G holds v .edgesInOut() = G .edgesBetween ((the_Vertices_of G),{v})

proof end;

theorem :: GLIBPRE0:30

for G being _Graph
for X, Y being set holds G .edgesDBetween (X,Y) = (G .edgesOutOf X) /\ (G .edgesInto Y)

proof end;

theorem :: GLIBPRE0:31

for G being _Graph
for X, Y being set holds G .edgesDBetween (X,Y) c= G .edgesBetween (X,Y)

proof end;

:: generalized case for GLIB_000:19

theorem Th36: :: GLIBPRE0:32

for G being _Graph
for v being Vertex of G st ( for e being object holds not e Joins v,v,G ) holds
card (v .edgesInOut()) = v .degree()

proof end;

theorem Th37: :: GLIBPRE0:33

for G being _Graph
for v being Vertex of G holds
( v is isolated iff ( v .edgesIn() = {} & v .edgesOut() = {} ) )

proof end;

theorem Th38: :: GLIBPRE0:34

for G being _Graph
for v being Vertex of G holds
( v is isolated iff ( v .inDegree() = 0 & v .outDegree() = 0 ) )

proof end;

:: generalization of GLIB_000:def 50

theorem Th39: :: GLIBPRE0:35

for G being _Graph
for v being Vertex of G holds
( v is isolated iff v .degree() = 0 )

proof end;

theorem :: GLIBPRE0:36

for G being _Graph
for X being set holds G .edgesInto X = union { (v .edgesIn()) where v is Vertex of G : v in X }

proof end;

theorem :: GLIBPRE0:37

for G being _Graph
for X being set holds G .edgesOutOf X = union { (v .edgesOut()) where v is Vertex of G : v in X }

proof end;

theorem :: GLIBPRE0:38

for G being _Graph
for X being set holds G .edgesInOut X = union { (v .edgesInOut()) where v is Vertex of G : v in X }

proof end;

theorem :: GLIBPRE0:39

for G being _Graph
for X, Y being set holds G .edgesDBetween (X,Y) = union { ((v .edgesOut()) /\ (w .edgesIn())) where v, w is Vertex of G : ( v in X & w in Y ) }

proof end;

theorem Th44: :: GLIBPRE0:40

for G being _Graph
for X, Y being set holds G .edgesBetween (X,Y) c= union { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) }

proof end;

theorem :: GLIBPRE0:41

for G being _Graph
for X, Y being set st X misses Y holds
G .edgesBetween (X,Y) = union { ((v .edgesInOut()) /\ (w .edgesInOut())) where v, w is Vertex of G : ( v in X & w in Y ) }

proof end;

theorem :: GLIBPRE0:42

for G1 being _Graph
for E being set
for G2 being removeEdges of G1,E
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .edgesIn() = (v1 .edgesIn()) \ E & v2 .edgesOut() = (v1 .edgesOut()) \ E & v2 .edgesInOut() = (v1 .edgesInOut()) \ E )

proof end;

theorem :: GLIBPRE0:43

for G1, G2 being _Graph
for V being set holds
( G2 is removeVertices of G1,V iff G2 is removeVertices of G1,(V /\ (the_Vertices_of G1)) )

proof end;

theorem Th48: :: GLIBPRE0:44

for G1 being _Graph
for V being set
for G2 being removeVertices of G1,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st V c< the_Vertices_of G1 & v1 = v2 holds
( v2 .edgesIn() = (v1 .edgesIn()) \ (G1 .edgesOutOf V) & v2 .edgesOut() = (v1 .edgesOut()) \ (G1 .edgesInto V) & v2 .edgesInOut() = (v1 .edgesInOut()) \ (G1 .edgesInOut V) )

proof end;

theorem :: GLIBPRE0:45

for G1 being non _trivial _Graph
for v being Vertex of G1
for G2 being removeVertex of G1,v
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .edgesIn() = (v1 .edgesIn()) \ (v .edgesOut()) & v2 .edgesOut() = (v1 .edgesOut()) \ (v .edgesIn()) & v2 .edgesInOut() = (v1 .edgesInOut()) \ (v .edgesInOut()) )

proof end;

theorem :: GLIBPRE0:46

for G being _Graph
for C being Component of G
for v1 being Vertex of G
for v2 being Vertex of C st v1 = v2 holds
( v1 .edgesIn() = v2 .edgesIn() & v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )

proof end;

theorem :: GLIBPRE0:47

for G2 being _Graph
for V being set
for G1 being addVertices of G2,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 .edgesIn() = v2 .edgesIn() & v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )

proof end;

theorem :: GLIBPRE0:48

for G2 being _Graph
for v, w, e being object
for G1 being addEdge of G2,v,e,w
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v2 <> v & v2 <> w holds
( v1 .edgesIn() = v2 .edgesIn() & v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )

proof end;

theorem :: GLIBPRE0:49

for G2 being _Graph
for v, w being Vertex of G2
for e being object
for G1 being addEdge of G2,v,e,w
for v1 being Vertex of G1 st not e in the_Edges_of G2 & v1 = v & v <> w holds
( v1 .edgesIn() = v .edgesIn() & v1 .inDegree() = v .inDegree() & v1 .edgesOut() = (v .edgesOut()) \/ {e} & v1 .outDegree() = (v .outDegree()) +` 1 & v1 .edgesInOut() = (v .edgesInOut()) \/ {e} & v1 .degree() = (v .degree()) +` 1 )

proof end;

theorem :: GLIBPRE0:50

for G2 being _Graph
for v, w being Vertex of G2
for e being object
for G1 being addEdge of G2,v,e,w
for w1 being Vertex of G1 st not e in the_Edges_of G2 & w1 = w & v <> w holds
( w1 .edgesIn() = (w .edgesIn()) \/ {e} & w1 .inDegree() = (w .inDegree()) +` 1 & w1 .edgesOut() = w .edgesOut() & w1 .outDegree() = w .outDegree() & w1 .edgesInOut() = (w .edgesInOut()) \/ {e} & w1 .degree() = (w .degree()) +` 1 )

proof end;

theorem :: GLIBPRE0:51

for G2 being _Graph
for v being Vertex of G2
for e being object
for G1 being addEdge of G2,v,e,v
for v1 being Vertex of G1 st not e in the_Edges_of G2 & v1 = v holds
( v1 .edgesIn() = (v .edgesIn()) \/ {e} & v1 .inDegree() = (v .inDegree()) +` 1 & v1 .edgesOut() = (v .edgesOut()) \/ {e} & v1 .outDegree() = (v .outDegree()) +` 1 & v1 .edgesInOut() = (v .edgesInOut()) \/ {e} & v1 .degree() = (v .degree()) +` 2 )

proof end;

theorem :: GLIBPRE0:52

for G3 being _Graph
for E being set
for G4 being reverseEdgeDirections of G3,E
for G1 being Supergraph of G3
for G2 being reverseEdgeDirections of G1,E st E c= the_Edges_of G3 holds
G2 is Supergraph of G4

proof end;

:: counterpart of GLIB_007:55

theorem :: GLIBPRE0:53

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

proof end;

theorem Th58: :: GLIBPRE0:54

for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & E c= the_Edges_of G1 holds
( v2 .edgesIn() = ((v1 .edgesIn()) \ E) \/ ((v1 .edgesOut()) /\ E) & v2 .edgesOut() = ((v1 .edgesOut()) \ E) \/ ((v1 .edgesIn()) /\ E) )

proof end;

theorem :: GLIBPRE0:55

for G1 being _Graph
for G2 being reverseEdgeDirections of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .edgesIn() = v1 .edgesOut() & v2 .inDegree() = v1 .outDegree() & v2 .edgesOut() = v1 .edgesIn() & v2 .outDegree() = v1 .inDegree() )

proof end;

theorem Th60: :: GLIBPRE0:56

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

proof end;

theorem :: GLIBPRE0:57

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V
for w being Vertex of G1 st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v = w holds
( w .allNeighbors() = V & w .degree() = card V )

proof end;

theorem Th62: :: GLIBPRE0:58

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & not v2 in V holds
( v1 .edgesIn() = v2 .edgesIn() & v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )

proof end;

theorem :: GLIBPRE0:59

for G2 being _Graph
for v being object
for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st not v in the_Vertices_of G2 & v1 = v2 & v2 in V holds
( v1 .allNeighbors() = (v2 .allNeighbors()) \/ {v} & v1 .degree() = (v2 .degree()) +` 1 )

proof end;

theorem :: GLIBPRE0:60

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 .degree() c= (v2 .degree()) +` 1 & v1 .inDegree() c= (v2 .inDegree()) +` 1 & v1 .outDegree() c= (v2 .outDegree()) +` 1 )

proof end;

theorem Th65: :: GLIBPRE0:61

for G being _Graph holds
( G is edgeless iff for v, w being Vertex of G holds not v,w are_adjacent )

proof end;

theorem :: GLIBPRE0:62

for G being loopless _Graph holds
( G is edgeless iff for v, w being Vertex of G st v <> w holds
not v,w are_adjacent )

proof end;

theorem Th67: :: GLIBPRE0:63

for G being _Graph holds G .loops() = dom ((the_Source_of G) /\ (the_Target_of G))

proof end;

Lm1: for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E holds G2 is reverseEdgeDirections of G1,E \ (G1 .loops())

proof end;

Lm2: for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E \ (G1 .loops()) holds G2 is reverseEdgeDirections of G1,E

proof end;

theorem :: GLIBPRE0:64

for G1, G2 being _Graph
for E being set holds
( G2 is reverseEdgeDirections of G1,E iff G2 is reverseEdgeDirections of G1,E \ (G1 .loops()) ) by Lm1, Lm2;

theorem Th69: :: GLIBPRE0:65

for G1 being _Graph
for G2 being removeLoops of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inNeighbors() = (v1 .inNeighbors()) \ {v1} & v2 .outNeighbors() = (v1 .outNeighbors()) \ {v1} & v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1} )

proof end;

theorem Th70: :: GLIBPRE0:66

for G1 being _Graph
for G2 being removeParallelEdges of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
v2 .allNeighbors() = v1 .allNeighbors()

proof end;

theorem Th71: :: GLIBPRE0:67

for G1 being _Graph
for G2 being removeDParallelEdges of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inNeighbors() = v1 .inNeighbors() & v2 .outNeighbors() = v1 .outNeighbors() & v2 .allNeighbors() = v1 .allNeighbors() )

proof end;

theorem :: GLIBPRE0:68

for G1 being _Graph
for G2 being SimpleGraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1}

proof end;

theorem :: GLIBPRE0:69

for G1 being _Graph
for G2 being DSimpleGraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inNeighbors() = (v1 .inNeighbors()) \ {v1} & v2 .outNeighbors() = (v1 .outNeighbors()) \ {v1} & v2 .allNeighbors() = (v1 .allNeighbors()) \ {v1} )

proof end;

registration

let G be non loopless _Graph;

cluster -> non loopless for removeParallelEdges of G;

coherence
for b₁ being removeParallelEdges of G holds not b₁ is loopless

proof end;

cluster -> non loopless for removeDParallelEdges of G;

coherence
for b₁ being removeDParallelEdges of G holds not b₁ is loopless

proof end;

end;

registration

let G be non edgeless _Graph;

cluster -> non edgeless for removeParallelEdges of G;

coherence
for b₁ being removeParallelEdges of G holds not b₁ is edgeless

proof end;

cluster -> non edgeless for removeDParallelEdges of G;

coherence
for b₁ being removeDParallelEdges of G holds not b₁ is edgeless

proof end;

end;

theorem :: GLIBPRE0:70

for G being _Graph
for E being RepEdgeSelection of G holds card E = card (Class (EdgeAdjEqRel G))

proof end;

theorem :: GLIBPRE0:71

for G being _Graph
for E being RepDEdgeSelection of G holds card E = card (Class (DEdgeAdjEqRel G))

proof end;

Lm3: for G being _Graph
for X being set
for E being Subset of (the_Edges_of G)
for H being reverseEdgeDirections of G,X st E is RepEdgeSelection of G holds
E is RepEdgeSelection of H

proof end;

theorem :: GLIBPRE0:72

for G being _Graph
for X being set
for E being Subset of (the_Edges_of G)
for H being reverseEdgeDirections of G,X holds
( E is RepEdgeSelection of G iff E is RepEdgeSelection of H )

proof end;

theorem :: GLIBPRE0:73

for G being _Graph
for V being non empty Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,V
for E being RepEdgeSelection of G holds E /\ (G .edgesBetween V) is RepEdgeSelection of H

proof end;

theorem :: GLIBPRE0:74

for G being _Graph
for V being non empty Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,V
for E being RepDEdgeSelection of G holds E /\ (G .edgesBetween V) is RepDEdgeSelection of H

proof end;

theorem :: GLIBPRE0:75

for G being _Graph
for V being set
for H being addVertices of G,V
for E being Subset of (the_Edges_of G) holds
( E is RepEdgeSelection of G iff E is RepEdgeSelection of H )

proof end;

theorem :: GLIBPRE0:76

for G being _Graph
for V being set
for H being addVertices of G,V
for E being Subset of (the_Edges_of G) holds
( E is RepDEdgeSelection of G iff E is RepDEdgeSelection of H )

proof end;

registration

cluster Relation-like omega -defined Function-like finite [Graph-like] non non-multi non-Dmulti countable for set ;

existence
ex b₁ being _Graph st
( not b₁ is non-multi & b₁ is non-Dmulti )

proof end;

end;

definition

let GF be Graph-yielding Function;

attr GF is plain means :Def1: :: GLIBPRE0:def 1
for x being object st x in dom GF holds
ex G being _Graph st
( GF . x = G & G is plain );

end;

:: deftheorem Def1 defines plain GLIBPRE0:def 1 :
for GF being Graph-yielding Function holds
( GF is plain iff for x being object st x in dom GF holds
ex G being _Graph st
( GF . x = G & G is plain ) );

registration

let G be plain _Graph;

cluster <*G*> -> plain ;

coherence
<*G*> is plain

proof end;

cluster NAT --> G -> plain ;

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

end;

definition

let GF be non empty Graph-yielding Function;

redefine attr GF is plain means :Def2: :: GLIBPRE0:def 2
for x being Element of dom GF holds GF . x is plain ;

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

proof end;

end;

:: deftheorem Def2 defines plain GLIBPRE0:def 2 :
for GF being non empty Graph-yielding Function holds
( GF is plain iff for x being Element of dom GF holds GF . x is plain );

Lm4: for F being ManySortedSet of NAT
for n being object holds
( n is Nat iff n in dom F )

proof end;

definition

let GSq be GraphSeq;

redefine attr GSq is plain means :Def3: :: GLIBPRE0:def 3
for n being Nat holds GSq . n is plain ;

compatibility
( GSq is plain iff for n being Nat holds GSq . n is plain )

proof end;

end;

:: deftheorem Def3 defines plain GLIBPRE0:def 3 :
for GSq being GraphSeq holds
( GSq is plain iff for n being Nat holds GSq . n is plain );

registration

cluster empty Relation-like Function-like Graph-yielding -> Graph-yielding plain for set ;

coherence
for b₁ being Graph-yielding Function st b₁ is empty holds
b₁ is plain ;

end;

registration

cluster non empty Relation-like omega -defined Function-like total Graph-yielding plain for set ;

existence
ex b₁ being GraphSeq st b₁ is plain

proof end;

cluster non empty Relation-like omega -defined Function-like finite FinSequence-like FinSubsequence-like Graph-yielding countable plain for set ;

existence
ex b₁ being Graph-yielding FinSequence st
( not b₁ is empty & b₁ is plain )

proof end;

end;

registration

let GF be non empty Graph-yielding plain Function;
let x be Element of dom GF;

cluster GF . x -> plain ;

coherence
GF . x is plain by Def2;

end;

registration

let GSq be plain GraphSeq;
let x be Nat;

cluster GSq . x -> plain ;

coherence
GSq . x is plain by Def3;

end;

registration

let p be Graph-yielding plain FinSequence;
let n be Nat;

cluster p | n -> plain ;

coherence
p | n is plain

proof end;

cluster p /^ n -> plain ;

coherence
p /^ n is plain

proof end;

let m be Nat;

cluster smid (p,m,n) -> plain ;

coherence
smid (p,m,n) is plain

proof end;

cluster (m,n) -cut p -> plain ;

coherence
(m,n) -cut p is plain

proof end;

end;

registration

let p, q be Graph-yielding plain FinSequence;

cluster p ^ q -> plain ;

coherence
p ^ q is plain

proof end;

cluster p ^' q -> plain ;

coherence
p ^' q is plain

proof end;

end;

registration

let G1, G2 be plain _Graph;

cluster <*G1,G2*> -> plain ;

coherence
<*G1,G2*> is plain

proof end;

let G3 be plain _Graph;

cluster <*G1,G2,G3*> -> plain ;

coherence
<*G1,G2,G3*> is plain

proof end;

end;

theorem Th81: :: GLIBPRE0:77

for G1, G2 being _Graph st G1 == G2 holds
ex F being PGraphMapping of G1,G2 st
( F = id G1 & F is Disomorphism )

proof end;

theorem :: GLIBPRE0:78

for G1, G2 being _Graph st G1 == G2 holds
G2 is G1 -Disomorphic

proof end;

theorem Th83: :: GLIBPRE0:79

for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E ex F being PGraphMapping of G1,G2 st
( F = id G1 & F is isomorphism )

proof end;

theorem :: GLIBPRE0:80

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

proof end;

:: correction of GLIB_010:90

theorem :: GLIBPRE0:81

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is Dcontinuous & F is isomorphism holds
( ( G1 is non-Dmulti implies G2 is non-Dmulti ) & ( G2 is non-Dmulti implies G1 is non-Dmulti ) & ( G1 is Dsimple implies G2 is Dsimple ) & ( G2 is Dsimple implies G1 is Dsimple ) )

proof end;

theorem Th86: :: GLIBPRE0:82

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v being Vertex of G1 st v in dom (F _V) holds
(F _E) .: (v .edgesInOut()) c= ((F _V) /. v) .edgesInOut()

proof end;

theorem Th87: :: GLIBPRE0:83

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is directed & v in dom (F _V) holds
( (F _E) .: (v .edgesIn()) c= ((F _V) /. v) .edgesIn() & (F _E) .: (v .edgesOut()) c= ((F _V) /. v) .edgesOut() )

proof end;

theorem Th88: :: GLIBPRE0:84

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is onto & F is semi-continuous & v in dom (F _V) holds
(F _E) .: (v .edgesInOut()) = ((F _V) /. v) .edgesInOut()

proof end;

theorem Th89: :: GLIBPRE0:85

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is onto & F is semi-Dcontinuous & v in dom (F _V) holds
( (F _E) .: (v .edgesIn()) = ((F _V) /. v) .edgesIn() & (F _E) .: (v .edgesOut()) = ((F _V) /. v) .edgesOut() )

proof end;

theorem :: GLIBPRE0:86

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is isomorphism holds
(F _E) .: (v .edgesInOut()) = ((F _V) /. v) .edgesInOut()

proof end;

theorem :: GLIBPRE0:87

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is Disomorphism holds
( (F _E) .: (v .edgesIn()) = ((F _V) /. v) .edgesIn() & (F _E) .: (v .edgesOut()) = ((F _V) /. v) .edgesOut() )

proof end;

registration

let G1 be _Graph;
let G2 be edgeless _Graph;

cluster -> directed for PGraphMapping of G1,G2;

coherence
for b₁ being PGraphMapping of G1,G2 holds b₁ is directed

proof end;

end;

theorem Th92: :: GLIBPRE0:88

for G1, G2 being _Graph
for F0 being PGraphMapping of G1,G2 st F0 _E is one-to-one holds
ex E being Subset of (the_Edges_of G2) st
for G3 being reverseEdgeDirections of G2,E ex F being PGraphMapping of G1,G3 st
( F = F0 & F is directed & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is onto implies F is onto ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) )

proof end;

theorem Th93: :: GLIBPRE0:89

for G1, G2 being _Graph
for F0 being PGraphMapping of G1,G2 st F0 _E is one-to-one holds
ex E being Subset of (the_Edges_of G2) st
for G3 being reverseEdgeDirections of G2,E ex F being PGraphMapping of G1,G3 st
( F = F0 & F is directed & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

proof end;

theorem Th94: :: GLIBPRE0:90

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is directed & F is weak_SG-embedding holds
( v .inDegree() c= ((F _V) /. v) .inDegree() & v .outDegree() c= ((F _V) /. v) .outDegree() )

proof end;

Lm5: for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is directed & F is weak_SG-embedding holds
v .degree() c= ((F _V) /. v) .degree()

proof end;

theorem :: GLIBPRE0:91

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is weak_SG-embedding holds
v .degree() c= ((F _V) /. v) .degree()

proof end;

theorem Th96: :: GLIBPRE0:92

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is onto & F is semi-Dcontinuous & v in dom (F _V) holds
( ((F _V) /. v) .inDegree() c= v .inDegree() & ((F _V) /. v) .outDegree() c= v .outDegree() )

proof end;

:: Can this theorem and all using it be improved to semi-continuous?

theorem :: GLIBPRE0:93

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is onto & F is semi-Dcontinuous & v in dom (F _V) holds
((F _V) /. v) .degree() c= v .degree()

proof end;

theorem Th98: :: GLIBPRE0:94

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is Disomorphism holds
( v .inDegree() = ((F _V) /. v) .inDegree() & v .outDegree() = ((F _V) /. v) .outDegree() )

proof end;

theorem Th99: :: GLIBPRE0:95

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is isomorphism holds
v .degree() = ((F _V) /. v) .degree()

proof end;

theorem Th100: :: GLIBPRE0:96

for G being _Graph
for u, v, w being Vertex of G st v is endvertex & u <> w & u,v are_adjacent holds
not v,w are_adjacent

proof end;

theorem Th101: :: GLIBPRE0:97

for G being _Graph
for v being Vertex of G st 3 c= G .order() & v is endvertex holds
ex u, w being Vertex of G st
( u <> v & w <> v & u <> w & u,v are_adjacent & not v,w are_adjacent )

proof end;

theorem :: GLIBPRE0:98

for G being _Graph
for v being Vertex of G st 4 c= G .order() & v is endvertex holds
ex x, y, z being Vertex of G st
( v <> x & v <> y & v <> z & x <> y & x <> z & y <> z & v,x are_adjacent & not v,y are_adjacent & not v,z are_adjacent )

proof end;

definition

let GF be Graph-yielding Function;

attr GF is chordal means :Def4: :: GLIBPRE0:def 4
for x being object st x in dom GF holds
ex G being _Graph st
( GF . x = G & G is chordal );

end;

:: deftheorem Def4 defines chordal GLIBPRE0:def 4 :
for GF being Graph-yielding Function holds
( GF is chordal iff for x being object st x in dom GF holds
ex G being _Graph st
( GF . x = G & G is chordal ) );

registration

let G be chordal _Graph;

cluster <*G*> -> chordal ;

coherence
<*G*> is chordal

proof end;

cluster NAT --> G -> chordal ;

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

end;

definition

let GF be non empty Graph-yielding Function;

redefine attr GF is chordal means :Def5: :: GLIBPRE0:def 5
for x being Element of dom GF holds GF . x is chordal ;

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

proof end;

end;

:: deftheorem Def5 defines chordal GLIBPRE0:def 5 :
for GF being non empty Graph-yielding Function holds
( GF is chordal iff for x being Element of dom GF holds GF . x is chordal );

definition

let GSq be GraphSeq;

redefine attr GSq is chordal means :Def6: :: GLIBPRE0:def 6
for n being Nat holds GSq . n is chordal ;

compatibility
( GSq is chordal iff for n being Nat holds GSq . n is chordal )

proof end;

end;

:: deftheorem Def6 defines chordal GLIBPRE0:def 6 :
for GSq being GraphSeq holds
( GSq is chordal iff for n being Nat holds GSq . n is chordal );

registration

cluster empty Relation-like Function-like Graph-yielding -> Graph-yielding chordal for set ;

coherence
for b₁ being Graph-yielding Function st b₁ is empty holds
b₁ is chordal ;

end;

registration

cluster non empty Relation-like omega -defined Function-like total Graph-yielding chordal for set ;

existence
ex b₁ being GraphSeq st b₁ is chordal

proof end;

cluster non empty Relation-like omega -defined Function-like finite FinSequence-like FinSubsequence-like Graph-yielding countable chordal for set ;

existence
ex b₁ being Graph-yielding FinSequence st
( not b₁ is empty & b₁ is chordal )

proof end;

end;

registration

let GF be non empty Graph-yielding chordal Function;
let x be Element of dom GF;

cluster GF . x -> chordal ;

coherence
GF . x is chordal by Def5;

end;

registration

let GSq be chordal GraphSeq;
let x be Nat;

cluster GSq . x -> chordal ;

coherence
GSq . x is chordal by Def6;

end;

registration

let p be Graph-yielding chordal FinSequence;
let n be Nat;

cluster p | n -> chordal ;

coherence
p | n is chordal

proof end;

cluster p /^ n -> chordal ;

coherence
p /^ n is chordal

proof end;

let m be Nat;

cluster smid (p,m,n) -> chordal ;

coherence
smid (p,m,n) is chordal

proof end;

cluster (m,n) -cut p -> chordal ;

coherence
(m,n) -cut p is chordal

proof end;

end;

registration

let p, q be Graph-yielding chordal FinSequence;

cluster p ^ q -> chordal ;

coherence
p ^ q is chordal

proof end;

cluster p ^' q -> chordal ;

coherence
p ^' q is chordal

proof end;

end;

registration

let G1, G2 be chordal _Graph;

cluster <*G1,G2*> -> chordal ;

coherence
<*G1,G2*> is chordal

proof end;

let G3 be chordal _Graph;

cluster <*G1,G2,G3*> -> chordal ;

coherence
<*G1,G2,G3*> is chordal

proof end;

end;

theorem :: GLIBPRE0:99

for G1, G2 being non-Dmulti _Graph
for f being directed PVertexMapping of G1,G2
for v being Vertex of G1 st f is Disomorphism holds
( v .inDegree() = (f /. v) .inDegree() & v .outDegree() = (f /. v) .outDegree() )

proof end;

theorem :: GLIBPRE0:100

for G1, G2 being non-multi _Graph
for f being PVertexMapping of G1,G2
for v being Vertex of G1 st f is isomorphism holds
v .degree() = (f /. v) .degree()

proof end;