:: by Sebastian Koch

::

:: Received December 30, 2019

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

:: generalization of XBOOLE_1:89

:: into XBOOLE_1 ?

:: into XBOOLE_1 ?

:: into ZFMISC_1 ?

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

( x = b & y = a )

proof end;

:: into ZFMISC_1 ?

theorem :: GLIBPRE0:5

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

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 ;

coherence

not id X is irreflexive

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

ex b_{1} being Relation of X st

( not b_{1} is irreflexive & not b_{1} is asymmetric )

ex b_{1} being Relation of X st

( b_{1} is symmetric & b_{1} is irreflexive & not b_{1} is total )

ex b_{1} being Relation of X st

( b_{1} is symmetric & not b_{1} is irreflexive & not b_{1} is empty )

end;
coherence

not id X is irreflexive

proof end;

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

( not b

proof end;

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

existence ex b

( b

proof end;

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

existence ex b

( b

proof end;

registration

let X be non trivial set ;

coherence

not id X is connected

ex b_{1} being Relation of X st

( b_{1} is symmetric & not b_{1} is connected )

not [:X,X:] is antisymmetric

not for b_{1} being Relation of X holds b_{1} is antisymmetric

end;
coherence

not id X is connected

proof end;

existence ex b

( b

proof end;

coherence not [:X,X:] is antisymmetric

proof end;

existence not for b

proof end;

:: into RELAT_1 ?

:: into RELAT_1 ?

:: into RELAT_1 ?

:: into RELAT_2 ?

:: into RELSET_1 ?

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

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

:: into EQREL_1 ?

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

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;

coherence

a /\ b is cardinal by ORDINAL3:13;

coherence

a \/ b is cardinal by ORDINAL3:12;

end;
coherence

a /\ b is cardinal by ORDINAL3:13;

coherence

a \/ b is cardinal by ORDINAL3:12;

:: into ORDINAL1 or WELLORD2 ?

:: into YELLOW_1 or ORDERS_5 ?

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

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 ?

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

a is cardinal number ) holds

meet X is cardinal number

proof end;

:: into CARD_3 ?

registration
end;

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

proof end;

registration
end;

:: into PENCIL_1 ?

:: mostly copied from there

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

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

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 ?

:: into SGRAPH1 or MATRIX11 ?

:: into MATRIX13 ?

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

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 )

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

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

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} )

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 )

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

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

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})

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)

for X, Y being set holds G .edgesDBetween (X,Y) = (G .edgesOutOf X) /\ (G .edgesInto 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()

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() = {} ) )

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

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

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 }

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 }

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 ) }

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 ) }

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 ) }

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 )

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

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

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

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

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

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

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 )

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 )

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 )

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

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, {}

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

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

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

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 )

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

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 )

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 )

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 )

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

( G is edgeless iff for v, w being Vertex of G st v <> w holds

not v,w are_adjacent )

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;

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} )

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

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

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}

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} )

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;

coherence

for b_{1} being removeParallelEdges of G holds not b_{1} is loopless

for b_{1} being removeDParallelEdges of G holds not b_{1} is loopless

end;
coherence

for b

proof end;

coherence for b

proof end;

registration

let G be non edgeless _Graph;

coherence

for b_{1} being removeParallelEdges of G holds not b_{1} is edgeless

for b_{1} being removeDParallelEdges of G holds not b_{1} is edgeless

end;
coherence

for b

proof end;

coherence for b

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 )

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

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

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 )

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 )

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

ex b_{1} being _Graph st

( not b_{1} is non-multi & b_{1} is non-Dmulti )
end;

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

existence ex b

( not b

proof 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 ) );

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;

coherence

<*G*> is plain

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

end;
coherence

<*G*> is plain

proof end;

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

definition

let GF be non empty Graph-yielding Function;

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

end;
redefine attr GF is plain means :Def2: :: GLIBPRE0:def 2

for x being Element of dom GF holds GF . x is plain ;

compatibility for x being Element of dom GF holds GF . x is plain ;

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

proof 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 );

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;

compatibility

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

end;
compatibility

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

proof 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 );

for GSq being GraphSeq holds

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

registration
end;

registration

existence

ex b_{1} being GraphSeq st b_{1} is plain

ex b_{1} being Graph-yielding FinSequence st

( not b_{1} is empty & b_{1} is plain )

end;
ex b

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

( not b

proof end;

registration

let GF be non empty Graph-yielding plain Function;

let x be Element of dom GF;

coherence

GF . x is plain by Def2;

end;
let x be Element of dom GF;

coherence

GF . x is plain by Def2;

registration

let p be Graph-yielding plain FinSequence;

let n be Nat;

coherence

p | n is plain

p /^ n is plain

coherence

smid (p,m,n) is plain

(m,n) -cut p is plain

end;
let n be Nat;

coherence

p | n is plain

proof end;

coherence p /^ n is plain

proof end;

let m be Nat;coherence

smid (p,m,n) is plain

proof end;

coherence (m,n) -cut p is plain

proof end;

registration

let p, q be Graph-yielding plain FinSequence;

coherence

p ^ q is plain

p ^' q is plain

end;
coherence

p ^ q is plain

proof end;

coherence p ^' q is plain

proof end;

registration

let G1, G2 be plain _Graph;

coherence

<*G1,G2*> is plain

coherence

<*G1,G2,G3*> is plain

end;
coherence

<*G1,G2*> is plain

proof end;

let G3 be plain _Graph;coherence

<*G1,G2,G3*> is plain

proof 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 )

ex F being PGraphMapping of G1,G2 st

( F = id G1 & F is Disomorphism )

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 )

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

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

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

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

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

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

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

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

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;

coherence

for b_{1} being PGraphMapping of G1,G2 holds b_{1} is directed

end;
let G2 be edgeless _Graph;

coherence

for b

proof 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 ) )

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

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

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

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

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

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

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

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

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 )

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 )

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;

:: 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 ) );

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;

coherence

<*G*> is chordal

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

end;
coherence

<*G*> is chordal

proof end;

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

definition

let GF be non empty Graph-yielding Function;

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

end;
redefine attr GF is chordal means :Def5: :: GLIBPRE0:def 5

for x being Element of dom GF holds GF . x is chordal ;

compatibility for x being Element of dom GF holds GF . x is chordal ;

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

proof 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 );

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;

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

end;
redefine attr GSq is chordal means :Def6: :: GLIBPRE0:def 6

for n being Nat holds GSq . n is chordal ;

compatibility for n being Nat holds GSq . n is chordal ;

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

proof 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 );

for GSq being GraphSeq holds

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

registration
end;

registration

existence

ex b_{1} being GraphSeq st b_{1} is chordal

ex b_{1} being Graph-yielding FinSequence st

( not b_{1} is empty & b_{1} is chordal )

end;
ex b

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

( not b

proof end;

registration

let GF be non empty Graph-yielding chordal Function;

let x be Element of dom GF;

coherence

GF . x is chordal by Def5;

end;
let x be Element of dom GF;

coherence

GF . x is chordal by Def5;

registration

let p be Graph-yielding chordal FinSequence;

let n be Nat;

coherence

p | n is chordal

p /^ n is chordal

coherence

smid (p,m,n) is chordal

(m,n) -cut p is chordal

end;
let n be Nat;

coherence

p | n is chordal

proof end;

coherence p /^ n is chordal

proof end;

let m be Nat;coherence

smid (p,m,n) is chordal

proof end;

coherence (m,n) -cut p is chordal

proof end;

registration

let p, q be Graph-yielding chordal FinSequence;

coherence

p ^ q is chordal

p ^' q is chordal

end;
coherence

p ^ q is chordal

proof end;

coherence p ^' q is chordal

proof end;

registration

let G1, G2 be chordal _Graph;

coherence

<*G1,G2*> is chordal

coherence

<*G1,G2,G3*> is chordal

end;
coherence

<*G1,G2*> is chordal

proof end;

let G3 be chordal _Graph;coherence

<*G1,G2,G3*> is chordal

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

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

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;

:: into XBOOLE_1 ?