begin
Lm1:
for GS being GraphStruct holds
( GS is [Graph-like] iff ( _GraphSelectors c= dom GS & not the_Vertices_of GS is empty & the_Source_of GS is Function of (the_Edges_of GS),(the_Vertices_of GS) & the_Target_of GS is Function of (the_Edges_of GS),(the_Vertices_of GS) ) )
Lm2:
for G being _Graph
for e, x, y being set holds
( e Joins x,y,G iff ( e DJoins x,y,G or e DJoins y,x,G ) )
Lm3:
for G being _Graph st the_Edges_of G = {} holds
G is simple
definition
let G be
_Graph;
let X,
Y be
set ;
existence
ex b1 being Subset of (the_Edges_of G) st
for e being set holds
( e in b1 iff e SJoins X,Y,G )
uniqueness
for b1, b2 being Subset of (the_Edges_of G) st ( for e being set holds
( e in b1 iff e SJoins X,Y,G ) ) & ( for e being set holds
( e in b2 iff e SJoins X,Y,G ) ) holds
b1 = b2
existence
ex b1 being Subset of (the_Edges_of G) st
for e being set holds
( e in b1 iff e DSJoins X,Y,G )
uniqueness
for b1, b2 being Subset of (the_Edges_of G) st ( for e being set holds
( e in b1 iff e DSJoins X,Y,G ) ) & ( for e being set holds
( e in b2 iff e DSJoins X,Y,G ) ) holds
b1 = b2
end;
Lm4:
for G being _Graph holds G is Subgraph of G
Lm5:
for G1 being _Graph
for G2 being Subgraph of G1
for x, y, e being set st e Joins x,y,G2 holds
e Joins x,y,G1
Lm6:
for G being _Graph
for e, X being set holds
( ( e in the_Edges_of G & (the_Source_of G) . e in X & (the_Target_of G) . e in X ) iff e in G .edgesBetween X )
Lm7:
for G being _Graph holds the_Edges_of G = G .edgesBetween (the_Vertices_of G)
Lm8:
for G being _Graph
for v being Vertex of G
for e being set holds
( e in v .edgesIn() iff ( e in the_Edges_of G & (the_Target_of G) . e = v ) )
Lm9:
for G being _Graph
for v being Vertex of G
for e being set holds
( e in v .edgesOut() iff ( e in the_Edges_of G & (the_Source_of G) . e = v ) )
begin
theorem
for
V being non
empty set for
E being
set for
S,
T being
Function of
E,
V holds
(
the_Vertices_of (createGraph (V,E,S,T)) = V &
the_Edges_of (createGraph (V,E,S,T)) = E &
the_Source_of (createGraph (V,E,S,T)) = S &
the_Target_of (createGraph (V,E,S,T)) = T )
by FINSEQ_4:76;
theorem
for
GS being
GraphStruct for
x,
y being
set for
n1,
n2 being
Nat st
n1 <> n2 holds
(
n1 in dom ((GS .set (n1,x)) .set (n2,y)) &
n2 in dom ((GS .set (n1,x)) .set (n2,y)) &
((GS .set (n1,x)) .set (n2,y)) . n1 = x &
((GS .set (n1,x)) .set (n2,y)) . n2 = y )
theorem
for
G being
_Graph for
e,
x1,
y1,
x2,
y2 being
set st
e Joins x1,
y1,
G &
e Joins x2,
y2,
G & not (
x1 = x2 &
y1 = y2 ) holds
(
x1 = y2 &
y1 = x2 )
theorem Th72:
for
G1 being
_Graph for
G2 being
Subgraph of
G1 for
x,
y,
e being
set holds
( (
e Joins x,
y,
G2 implies
e Joins x,
y,
G1 ) & (
e DJoins x,
y,
G2 implies
e DJoins x,
y,
G1 ) & (
e SJoins x,
y,
G2 implies
e SJoins x,
y,
G1 ) & (
e DSJoins x,
y,
G2 implies
e DSJoins x,
y,
G1 ) )
theorem
for
G1 being
_Graph for
G2 being
Subgraph of
G1 for
x,
y,
e being
set st
e in the_Edges_of G2 holds
( (
e Joins x,
y,
G1 implies
e Joins x,
y,
G2 ) & (
e DJoins x,
y,
G1 implies
e DJoins x,
y,
G2 ) & (
e SJoins x,
y,
G1 implies
e SJoins x,
y,
G2 ) & (
e DSJoins x,
y,
G1 implies
e DSJoins x,
y,
G2 ) )
theorem Th85:
for
G1,
G2,
G3 being
_Graph st
G1 == G2 &
G2 == G3 holds
G1 == G3
theorem Th88:
for
G1,
G2 being
_Graph for
e,
x,
y,
X,
Y being
set st
G1 == G2 holds
( (
e Joins x,
y,
G1 implies
e Joins x,
y,
G2 ) & (
e DJoins x,
y,
G1 implies
e DJoins x,
y,
G2 ) & (
e SJoins X,
Y,
G1 implies
e SJoins X,
Y,
G2 ) & (
e DSJoins X,
Y,
G1 implies
e DSJoins X,
Y,
G2 ) )