:: by Yozo Toda

::

:: Received September 8, 1994

:: Copyright (c) 1994-2012 Association of Mizar Users

begin

Lm1: for e being set

for n being Element of NAT st e in Seg n holds

ex i being Element of NAT st

( e = i & 1 <= i & i <= n )

proof end;

definition

let m, n be Nat;

{ i where i is Element of NAT : ( m <= i & i <= n ) } is Subset of NAT

end;
func nat_interval (m,n) -> Subset of NAT equals :: SGRAPH1:def 1

{ i where i is Element of NAT : ( m <= i & i <= n ) } ;

coherence { i where i is Element of NAT : ( m <= i & i <= n ) } ;

{ i where i is Element of NAT : ( m <= i & i <= n ) } is Subset of NAT

proof end;

:: deftheorem defines nat_interval SGRAPH1:def 1 :

for m, n being Nat holds nat_interval (m,n) = { i where i is Element of NAT : ( m <= i & i <= n ) } ;

for m, n being Nat holds nat_interval (m,n) = { i where i is Element of NAT : ( m <= i & i <= n ) } ;

theorem :: SGRAPH1:1

Lm2: for A being set

for s being Subset of A

for n being set st n in A holds

s \/ {n} is Subset of A

proof end;

definition

let A be set ;

{ z where z is finite Subset of A : card z = 2 } is set ;

end;
func TWOELEMENTSETS A -> set equals :: SGRAPH1:def 2

{ z where z is finite Subset of A : card z = 2 } ;

coherence { z where z is finite Subset of A : card z = 2 } ;

{ z where z is finite Subset of A : card z = 2 } is set ;

:: deftheorem defines TWOELEMENTSETS SGRAPH1:def 2 :

for A being set holds TWOELEMENTSETS A = { z where z is finite Subset of A : card z = 2 } ;

for A being set holds TWOELEMENTSETS A = { z where z is finite Subset of A : card z = 2 } ;

theorem Th8: :: SGRAPH1:8

for A, e being set holds

( e in TWOELEMENTSETS A iff ( e is finite Subset of A & ex x, y being set st

( x in A & y in A & x <> y & e = {x,y} ) ) )

( e in TWOELEMENTSETS A iff ( e is finite Subset of A & ex x, y being set st

( x in A & y in A & x <> y & e = {x,y} ) ) )

proof end;

begin

:: graph is defined as a pair of two sets, of vertices and of edges.

:: we treat only simple graphs;

:: edges are non-directed, there is no loop,

:: between two vertices is at most one edge.

:: we define the set of all graphs SIMPLEGRAPHS,

:: and later define some operations on graphs

:: (contraction, deletion, minor, etc.) as relations on SIMPLEGRAPHS.

:: Vertices and Edges are used in graph_1. so we must use different names.

:: we restrict simple graphs as finite ones

:: to treat degree as a cardinal of a set of edges.

:: we treat only simple graphs;

:: edges are non-directed, there is no loop,

:: between two vertices is at most one edge.

:: we define the set of all graphs SIMPLEGRAPHS,

:: and later define some operations on graphs

:: (contraction, deletion, minor, etc.) as relations on SIMPLEGRAPHS.

:: Vertices and Edges are used in graph_1. so we must use different names.

:: we restrict simple graphs as finite ones

:: to treat degree as a cardinal of a set of edges.

definition

attr c_{1} is strict ;

struct SimpleGraphStruct -> 1-sorted ;

aggr SimpleGraphStruct(# carrier, SEdges #) -> SimpleGraphStruct ;

sel SEdges c_{1} -> Subset of (TWOELEMENTSETS the carrier of c_{1});

end;
struct SimpleGraphStruct -> 1-sorted ;

aggr SimpleGraphStruct(# carrier, SEdges #) -> SimpleGraphStruct ;

sel SEdges c

:: SIMPLEGRAPHS is the set of all (simple) graphs,

:: which is the smallest set satisfying following three conditions:

:: (1) it contains <Empty,Empty>,

:: (2) if <V,E> is an element of SIMPLEGRAPHS and n is not a vertex of <V,E>,

:: then <(V U {n}),E> is also an element of SIMPLEGRAPHS,

:: (3) if <V,E> is an element of SIMPLEGRAPHS,

:: v1,v2 are different vertices of <V,E>,

:: and {v1,v2} is not an edge of <V,E>,

:: then <V,(E U {v1,v2})> is also an element of SIMPLEGRAPHS.

:: which is the smallest set satisfying following three conditions:

:: (1) it contains <Empty,Empty>,

:: (2) if <V,E> is an element of SIMPLEGRAPHS and n is not a vertex of <V,E>,

:: then <(V U {n}),E> is also an element of SIMPLEGRAPHS,

:: (3) if <V,E> is an element of SIMPLEGRAPHS,

:: v1,v2 are different vertices of <V,E>,

:: and {v1,v2} is not an edge of <V,E>,

:: then <V,(E U {v1,v2})> is also an element of SIMPLEGRAPHS.

definition

let X be set ;

{ SimpleGraphStruct(# v,e #) where v is finite Subset of X, e is finite Subset of (TWOELEMENTSETS v) : verum } is set ;

end;
func SIMPLEGRAPHS X -> set equals :: SGRAPH1:def 3

{ SimpleGraphStruct(# v,e #) where v is finite Subset of X, e is finite Subset of (TWOELEMENTSETS v) : verum } ;

coherence { SimpleGraphStruct(# v,e #) where v is finite Subset of X, e is finite Subset of (TWOELEMENTSETS v) : verum } ;

{ SimpleGraphStruct(# v,e #) where v is finite Subset of X, e is finite Subset of (TWOELEMENTSETS v) : verum } is set ;

:: deftheorem defines SIMPLEGRAPHS SGRAPH1:def 3 :

for X being set holds SIMPLEGRAPHS X = { SimpleGraphStruct(# v,e #) where v is finite Subset of X, e is finite Subset of (TWOELEMENTSETS v) : verum } ;

for X being set holds SIMPLEGRAPHS X = { SimpleGraphStruct(# v,e #) where v is finite Subset of X, e is finite Subset of (TWOELEMENTSETS v) : verum } ;

registration
end;

definition

let X be set ;

ex b_{1} being strict SimpleGraphStruct st b_{1} is Element of SIMPLEGRAPHS X

end;
mode SimpleGraph of X -> strict SimpleGraphStruct means :Def4: :: SGRAPH1:def 4

it is Element of SIMPLEGRAPHS X;

existence it is Element of SIMPLEGRAPHS X;

ex b

proof end;

:: deftheorem Def4 defines SimpleGraph SGRAPH1:def 4 :

for X being set

for b_{2} being strict SimpleGraphStruct holds

( b_{2} is SimpleGraph of X iff b_{2} is Element of SIMPLEGRAPHS X );

for X being set

for b

( b

theorem Th17: :: SGRAPH1:17

for X, g being set holds

( g in SIMPLEGRAPHS X iff ex v being finite Subset of X ex e being finite Subset of (TWOELEMENTSETS v) st g = SimpleGraphStruct(# v,e #) ) ;

( g in SIMPLEGRAPHS X iff ex v being finite Subset of X ex e being finite Subset of (TWOELEMENTSETS v) st g = SimpleGraphStruct(# v,e #) ) ;

begin

theorem Th18: :: SGRAPH1:18

for X being set

for g being SimpleGraph of X holds

( the carrier of g c= X & the SEdges of g c= TWOELEMENTSETS the carrier of g )

for g being SimpleGraph of X holds

( the carrier of g c= X & the SEdges of g c= TWOELEMENTSETS the carrier of g )

proof end;

theorem :: SGRAPH1:19

theorem :: SGRAPH1:20

theorem Th21: :: SGRAPH1:21

for X being set

for g being SimpleGraph of X holds

( the carrier of g is finite Subset of X & the SEdges of g is finite Subset of (TWOELEMENTSETS the carrier of g) )

for g being SimpleGraph of X holds

( the carrier of g is finite Subset of X & the SEdges of g is finite Subset of (TWOELEMENTSETS the carrier of g) )

proof end;

:: SECTION 3: equality relation on SIMPLEGRAPHS.

:: two graphs are said to be "isomorphic" if

:: (1) there is bijective function (i.e. set-theoretic isomorphism)

:: between two sets of vertices,

:: (2) this iso. respects the correspondence of edges.

:: two graphs are said to be "isomorphic" if

:: (1) there is bijective function (i.e. set-theoretic isomorphism)

:: between two sets of vertices,

:: (2) this iso. respects the correspondence of edges.

:: deftheorem defines is_isomorphic_to SGRAPH1:def 5 :

for X being set

for G, G9 being SimpleGraph of X holds

( G is_isomorphic_to G9 iff ex Fv being Function of the carrier of G, the carrier of G9 st

( Fv is bijective & ( for v1, v2 being Element of G holds

( {v1,v2} in the SEdges of G iff {(Fv . v1),(Fv . v2)} in the SEdges of G ) ) ) );

for X being set

for G, G9 being SimpleGraph of X holds

( G is_isomorphic_to G9 iff ex Fv being Function of the carrier of G, the carrier of G9 st

( Fv is bijective & ( for v1, v2 being Element of G holds

( {v1,v2} in the SEdges of G iff {(Fv . v1),(Fv . v2)} in the SEdges of G ) ) ) );

begin

:: here is the induction principle on SIMPLEGRAPHS(X).

scheme :: SGRAPH1:sch 1

IndSimpleGraphs0{ F_{1}() -> set , P_{1}[ set ] } :

provided

IndSimpleGraphs0{ F

provided

A1:
P_{1}[ SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #)]
and

A2: for g being SimpleGraph of F_{1}()

for v being set st g in SIMPLEGRAPHS F_{1}() & P_{1}[g] & v in F_{1}() & not v in the carrier of g holds

P_{1}[ SimpleGraphStruct(# ( the carrier of g \/ {v}),({} (TWOELEMENTSETS ( the carrier of g \/ {v}))) #)]
and

A3: for g being SimpleGraph of F_{1}()

for e being set st P_{1}[g] & e in TWOELEMENTSETS the carrier of g & not e in the SEdges of g holds

ex sege being Subset of (TWOELEMENTSETS the carrier of g) st

( sege = the SEdges of g \/ {e} & P_{1}[ SimpleGraphStruct(# the carrier of g,sege #)] )

A2: for g being SimpleGraph of F

for v being set st g in SIMPLEGRAPHS F

P

A3: for g being SimpleGraph of F

for e being set st P

ex sege being Subset of (TWOELEMENTSETS the carrier of g) st

( sege = the SEdges of g \/ {e} & P

proof end;

:: now we give a theorem characterising SIMPLEGRAPHS as

:: an inductively defined set. we need some lemmas.

:: an inductively defined set. we need some lemmas.

theorem :: SGRAPH1:22

for X being set

for g being SimpleGraph of X holds

( g = SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) or ex v being set ex e being Subset of (TWOELEMENTSETS v) st

( not v is empty & g = SimpleGraphStruct(# v,e #) ) )

for g being SimpleGraph of X holds

( g = SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) or ex v being set ex e being Subset of (TWOELEMENTSETS v) st

( not v is empty & g = SimpleGraphStruct(# v,e #) ) )

proof end;

theorem Th23: :: SGRAPH1:23

for X being set

for V being Subset of X

for E being Subset of (TWOELEMENTSETS V)

for n being set

for Evn being finite Subset of (TWOELEMENTSETS (V \/ {n})) st SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X & n in X holds

SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X

for V being Subset of X

for E being Subset of (TWOELEMENTSETS V)

for n being set

for Evn being finite Subset of (TWOELEMENTSETS (V \/ {n})) st SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X & n in X holds

SimpleGraphStruct(# (V \/ {n}),Evn #) in SIMPLEGRAPHS X

proof end;

theorem Th24: :: SGRAPH1:24

for X being set

for V being Subset of X

for E being Subset of (TWOELEMENTSETS V)

for v1, v2 being set st v1 in V & v2 in V & v1 <> v2 & SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X holds

ex v1v2 being finite Subset of (TWOELEMENTSETS V) st

( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X )

for V being Subset of X

for E being Subset of (TWOELEMENTSETS V)

for v1, v2 being set st v1 in V & v2 in V & v1 <> v2 & SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X holds

ex v1v2 being finite Subset of (TWOELEMENTSETS V) st

( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X )

proof end;

:: next we define a predicate

:: which describe how SIMPLEGRAPHS are generated inductively.

:: *** QUESTION ***

:: conditions (not n in V) and (not {v1,v2} in E) are redundant?

:: which describe how SIMPLEGRAPHS are generated inductively.

:: *** QUESTION ***

:: conditions (not n in V) and (not {v1,v2} in E) are redundant?

definition

let X, GG be set ;

end;
pred GG is_SetOfSimpleGraphs_of X means :Def6: :: SGRAPH1:def 6

( SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) in GG & ( for V being Subset of X

for E being Subset of (TWOELEMENTSETS V)

for n being set

for Evn being finite Subset of (TWOELEMENTSETS (V \/ {n})) st SimpleGraphStruct(# V,E #) in GG & n in X & not n in V holds

SimpleGraphStruct(# (V \/ {n}),Evn #) in GG ) & ( for V being Subset of X

for E being Subset of (TWOELEMENTSETS V)

for v1, v2 being set st SimpleGraphStruct(# V,E #) in GG & v1 in V & v2 in V & v1 <> v2 & not {v1,v2} in E holds

ex v1v2 being finite Subset of (TWOELEMENTSETS V) st

( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in GG ) ) );

( SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) in GG & ( for V being Subset of X

for E being Subset of (TWOELEMENTSETS V)

for n being set

for Evn being finite Subset of (TWOELEMENTSETS (V \/ {n})) st SimpleGraphStruct(# V,E #) in GG & n in X & not n in V holds

SimpleGraphStruct(# (V \/ {n}),Evn #) in GG ) & ( for V being Subset of X

for E being Subset of (TWOELEMENTSETS V)

for v1, v2 being set st SimpleGraphStruct(# V,E #) in GG & v1 in V & v2 in V & v1 <> v2 & not {v1,v2} in E holds

ex v1v2 being finite Subset of (TWOELEMENTSETS V) st

( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in GG ) ) );

:: deftheorem Def6 defines is_SetOfSimpleGraphs_of SGRAPH1:def 6 :

for X, GG being set holds

( GG is_SetOfSimpleGraphs_of X iff ( SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) in GG & ( for V being Subset of X

for E being Subset of (TWOELEMENTSETS V)

for n being set

for Evn being finite Subset of (TWOELEMENTSETS (V \/ {n})) st SimpleGraphStruct(# V,E #) in GG & n in X & not n in V holds

SimpleGraphStruct(# (V \/ {n}),Evn #) in GG ) & ( for V being Subset of X

for E being Subset of (TWOELEMENTSETS V)

for v1, v2 being set st SimpleGraphStruct(# V,E #) in GG & v1 in V & v2 in V & v1 <> v2 & not {v1,v2} in E holds

ex v1v2 being finite Subset of (TWOELEMENTSETS V) st

( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in GG ) ) ) );

for X, GG being set holds

( GG is_SetOfSimpleGraphs_of X iff ( SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #) in GG & ( for V being Subset of X

for E being Subset of (TWOELEMENTSETS V)

for n being set

for Evn being finite Subset of (TWOELEMENTSETS (V \/ {n})) st SimpleGraphStruct(# V,E #) in GG & n in X & not n in V holds

SimpleGraphStruct(# (V \/ {n}),Evn #) in GG ) & ( for V being Subset of X

for E being Subset of (TWOELEMENTSETS V)

for v1, v2 being set st SimpleGraphStruct(# V,E #) in GG & v1 in V & v2 in V & v1 <> v2 & not {v1,v2} in E holds

ex v1v2 being finite Subset of (TWOELEMENTSETS V) st

( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in GG ) ) ) );

theorem :: SGRAPH1:27

for X being set holds

( SIMPLEGRAPHS X is_SetOfSimpleGraphs_of X & ( for OTHER being set st OTHER is_SetOfSimpleGraphs_of X holds

SIMPLEGRAPHS X c= OTHER ) ) by Th25, Th26;

( SIMPLEGRAPHS X is_SetOfSimpleGraphs_of X & ( for OTHER being set st OTHER is_SetOfSimpleGraphs_of X holds

SIMPLEGRAPHS X c= OTHER ) ) by Th25, Th26;

begin

:: graph G is a subgraph of graph G' if

:: (1) the set of vertices of G is a subset of the set of vertices of G',

:: (2) the set of edges of G is a subset of the set of edges of G',

:: where two endpoints of each edge of G must be the vertices of G.

:: (of course G must be a graph!)

:: now no lemma is proved )-:

:: (1) the set of vertices of G is a subset of the set of vertices of G',

:: (2) the set of edges of G is a subset of the set of edges of G',

:: where two endpoints of each edge of G must be the vertices of G.

:: (of course G must be a graph!)

:: now no lemma is proved )-:

definition

let X be set ;

let G be SimpleGraph of X;

ex b_{1} being SimpleGraph of X st

( the carrier of b_{1} c= the carrier of G & the SEdges of b_{1} c= the SEdges of G )
;

end;
let G be SimpleGraph of X;

mode SubGraph of G -> SimpleGraph of X means :: SGRAPH1:def 7

( the carrier of it c= the carrier of G & the SEdges of it c= the SEdges of G );

existence ( the carrier of it c= the carrier of G & the SEdges of it c= the SEdges of G );

ex b

( the carrier of b

:: deftheorem defines SubGraph SGRAPH1:def 7 :

for X being set

for G, b_{3} being SimpleGraph of X holds

( b_{3} is SubGraph of G iff ( the carrier of b_{3} c= the carrier of G & the SEdges of b_{3} c= the SEdges of G ) );

for X being set

for G, b

( b

begin

:: the degree of a vertex means the number of edges connected to that vertex.

:: in the case of simple graphs, we can prove that

:: the degree is equal to the number of adjacent vertices.

:: (if loop is allowed,

:: the number of edges and the number of adjacent vertices are different.)

:: at first we defined degree(v),

:: where v was Element of the SEdges of(G) and G was an implicit argument.

:: but now we have changed the type of v to set,

:: and G must be an explicit argument

:: or we get an error "Inaccessible locus".

:: in the case of simple graphs, we can prove that

:: the degree is equal to the number of adjacent vertices.

:: (if loop is allowed,

:: the number of edges and the number of adjacent vertices are different.)

:: at first we defined degree(v),

:: where v was Element of the SEdges of(G) and G was an implicit argument.

:: but now we have changed the type of v to set,

:: and G must be an explicit argument

:: or we get an error "Inaccessible locus".

definition

let X be set ;

let G be SimpleGraph of X;

let v be set ;

ex b_{1} being Element of NAT ex X being finite set st

( ( for z being set holds

( z in X iff ( z in the SEdges of G & v in z ) ) ) & b_{1} = card X )

for b_{1}, b_{2} being Element of NAT st ex X being finite set st

( ( for z being set holds

( z in X iff ( z in the SEdges of G & v in z ) ) ) & b_{1} = card X ) & ex X being finite set st

( ( for z being set holds

( z in X iff ( z in the SEdges of G & v in z ) ) ) & b_{2} = card X ) holds

b_{1} = b_{2}

end;
let G be SimpleGraph of X;

let v be set ;

func degree (G,v) -> Element of NAT means :Def8: :: SGRAPH1:def 8

ex X being finite set st

( ( for z being set holds

( z in X iff ( z in the SEdges of G & v in z ) ) ) & it = card X );

existence ex X being finite set st

( ( for z being set holds

( z in X iff ( z in the SEdges of G & v in z ) ) ) & it = card X );

ex b

( ( for z being set holds

( z in X iff ( z in the SEdges of G & v in z ) ) ) & b

proof end;

uniqueness for b

( ( for z being set holds

( z in X iff ( z in the SEdges of G & v in z ) ) ) & b

( ( for z being set holds

( z in X iff ( z in the SEdges of G & v in z ) ) ) & b

b

proof end;

:: deftheorem Def8 defines degree SGRAPH1:def 8 :

for X being set

for G being SimpleGraph of X

for v being set

for b_{4} being Element of NAT holds

( b_{4} = degree (G,v) iff ex X being finite set st

( ( for z being set holds

( z in X iff ( z in the SEdges of G & v in z ) ) ) & b_{4} = card X ) );

for X being set

for G being SimpleGraph of X

for v being set

for b

( b

( ( for z being set holds

( z in X iff ( z in the SEdges of G & v in z ) ) ) & b

theorem Th28: :: SGRAPH1:28

for X being non empty set

for G being SimpleGraph of X

for v being set ex ww being finite set st

( ww = { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } & degree (G,v) = card ww )

for G being SimpleGraph of X

for v being set ex ww being finite set st

( ww = { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } & degree (G,v) = card ww )

proof end;

theorem :: SGRAPH1:29

for X being non empty set

for g being SimpleGraph of X

for v being set st v in the carrier of g holds

ex VV being finite set st

( VV = the carrier of g & degree (g,v) < card VV )

for g being SimpleGraph of X

for v being set st v in the carrier of g holds

ex VV being finite set st

( VV = the carrier of g & degree (g,v) < card VV )

proof end;

theorem :: SGRAPH1:30

for X being set

for g being SimpleGraph of X

for v, e being set st e in the SEdges of g & degree (g,v) = 0 holds

not v in e

for g being SimpleGraph of X

for v, e being set st e in the SEdges of g & degree (g,v) = 0 holds

not v in e

proof end;

theorem :: SGRAPH1:31

for X being set

for g being SimpleGraph of X

for v being set

for vg being finite set st vg = the carrier of g & v in vg & 1 + (degree (g,v)) = card vg holds

for w being Element of vg st v <> w holds

ex e being set st

( e in the SEdges of g & e = {v,w} )

for g being SimpleGraph of X

for v being set

for vg being finite set st vg = the carrier of g & v in vg & 1 + (degree (g,v)) = card vg holds

for w being Element of vg st v <> w holds

ex e being set st

( e in the SEdges of g & e = {v,w} )

proof end;

begin

:: path is coded as a sequence of vertices,

:: any two of them contained are different each other.

:: but the head and the tail may be equal (which is cycle).

:: any two of them contained are different each other.

:: but the head and the tail may be equal (which is cycle).

definition

let X be set ;

let g be SimpleGraph of X;

let v1, v2 be Element of g;

let p be FinSequence of the carrier of g;

end;
let g be SimpleGraph of X;

let v1, v2 be Element of g;

let p be FinSequence of the carrier of g;

pred p is_path_of v1,v2 means :Def9: :: SGRAPH1:def 9

( p . 1 = v1 & p . (len p) = v2 & ( for i being Element of NAT st 1 <= i & i < len p holds

{(p . i),(p . (i + 1))} in the SEdges of g ) & ( for i, j being Element of NAT st 1 <= i & i < len p & i < j & j < len p holds

( p . i <> p . j & {(p . i),(p . (i + 1))} <> {(p . j),(p . (j + 1))} ) ) );

( p . 1 = v1 & p . (len p) = v2 & ( for i being Element of NAT st 1 <= i & i < len p holds

{(p . i),(p . (i + 1))} in the SEdges of g ) & ( for i, j being Element of NAT st 1 <= i & i < len p & i < j & j < len p holds

( p . i <> p . j & {(p . i),(p . (i + 1))} <> {(p . j),(p . (j + 1))} ) ) );

:: deftheorem Def9 defines is_path_of SGRAPH1:def 9 :

for X being set

for g being SimpleGraph of X

for v1, v2 being Element of g

for p being FinSequence of the carrier of g holds

( p is_path_of v1,v2 iff ( p . 1 = v1 & p . (len p) = v2 & ( for i being Element of NAT st 1 <= i & i < len p holds

{(p . i),(p . (i + 1))} in the SEdges of g ) & ( for i, j being Element of NAT st 1 <= i & i < len p & i < j & j < len p holds

( p . i <> p . j & {(p . i),(p . (i + 1))} <> {(p . j),(p . (j + 1))} ) ) ) );

for X being set

for g being SimpleGraph of X

for v1, v2 being Element of g

for p being FinSequence of the carrier of g holds

( p is_path_of v1,v2 iff ( p . 1 = v1 & p . (len p) = v2 & ( for i being Element of NAT st 1 <= i & i < len p holds

{(p . i),(p . (i + 1))} in the SEdges of g ) & ( for i, j being Element of NAT st 1 <= i & i < len p & i < j & j < len p holds

( p . i <> p . j & {(p . i),(p . (i + 1))} <> {(p . j),(p . (j + 1))} ) ) ) );

definition

let X be set ;

let g be SimpleGraph of X;

let v1, v2 be Element of the carrier of g;

{ ss where ss is Element of the carrier of g * : ss is_path_of v1,v2 } is Subset of ( the carrier of g *)

end;
let g be SimpleGraph of X;

let v1, v2 be Element of the carrier of g;

func PATHS (v1,v2) -> Subset of ( the carrier of g *) equals :: SGRAPH1:def 10

{ ss where ss is Element of the carrier of g * : ss is_path_of v1,v2 } ;

coherence { ss where ss is Element of the carrier of g * : ss is_path_of v1,v2 } ;

{ ss where ss is Element of the carrier of g * : ss is_path_of v1,v2 } is Subset of ( the carrier of g *)

proof end;

:: deftheorem defines PATHS SGRAPH1:def 10 :

for X being set

for g being SimpleGraph of X

for v1, v2 being Element of the carrier of g holds PATHS (v1,v2) = { ss where ss is Element of the carrier of g * : ss is_path_of v1,v2 } ;

for X being set

for g being SimpleGraph of X

for v1, v2 being Element of the carrier of g holds PATHS (v1,v2) = { ss where ss is Element of the carrier of g * : ss is_path_of v1,v2 } ;

theorem :: SGRAPH1:32

theorem :: SGRAPH1:33

for X being set

for g being SimpleGraph of X

for v1, v2 being Element of the carrier of g

for e being Element of the carrier of g * st e is_path_of v1,v2 holds

e in PATHS (v1,v2) ;

for g being SimpleGraph of X

for v1, v2 being Element of the carrier of g

for e being Element of the carrier of g * st e is_path_of v1,v2 holds

e in PATHS (v1,v2) ;

::definition :: is_cycle

:: let g be SimpleGraph of X,

:: v1,v2 be Element of (the carrier of g),

:: p be Element of PATHS(v1,v2);

:: pred p is_cycle means :cycleDef:

:: v1=v2 & ex q being Element of ((the carrier of g)*) st (q=p & 3<=(len q));

::end;

:: let g be SimpleGraph of X,

:: v1,v2 be Element of (the carrier of g),

:: p be Element of PATHS(v1,v2);

:: pred p is_cycle means :cycleDef:

:: v1=v2 & ex q being Element of ((the carrier of g)*) st (q=p & 3<=(len q));

::end;

definition

let X be set ;

let g be SimpleGraph of X;

let p be set ;

end;
let g be SimpleGraph of X;

let p be set ;

pred p is_cycle_of g means :Def11: :: SGRAPH1:def 11

ex v being Element of the carrier of g st p in PATHS (v,v);

ex v being Element of the carrier of g st p in PATHS (v,v);

:: deftheorem Def11 defines is_cycle_of SGRAPH1:def 11 :

for X being set

for g being SimpleGraph of X

for p being set holds

( p is_cycle_of g iff ex v being Element of the carrier of g st p in PATHS (v,v) );

for X being set

for g being SimpleGraph of X

for p being set holds

( p is_cycle_of g iff ex v being Element of the carrier of g st p in PATHS (v,v) );

begin

:: K_{3,3} = {{1,2,3,4,5,6},

:: {{1,4},{1,5},{1,6},{2,4},{2,5},{2,6},{3,4},{3,5},{3,6}}}.

:: K_5 = {{1,2,3,4,5},

:: {{1,2},{1,3},{1,4},{1,5},{2,3},{2,4},{2,5},{3,4},{3,5},{4,5}}}.

:: for the proof of Kuratowski's theorem, we need only K_{3,3} and K_5.

:: here we define complete (and complete bipartate) graphs in general.

:: {{1,4},{1,5},{1,6},{2,4},{2,5},{2,6},{3,4},{3,5},{3,6}}}.

:: K_5 = {{1,2,3,4,5},

:: {{1,2},{1,3},{1,4},{1,5},{2,3},{2,4},{2,5},{3,4},{3,5},{4,5}}}.

:: for the proof of Kuratowski's theorem, we need only K_{3,3} and K_5.

:: here we define complete (and complete bipartate) graphs in general.

definition

let n, m be Element of NAT ;

ex b_{1} being SimpleGraph of NAT ex ee being Subset of (TWOELEMENTSETS (Seg (m + n))) st

( ee = { {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) ) } & b_{1} = SimpleGraphStruct(# (Seg (m + n)),ee #) )

for b_{1}, b_{2} being SimpleGraph of NAT st ex ee being Subset of (TWOELEMENTSETS (Seg (m + n))) st

( ee = { {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) ) } & b_{1} = SimpleGraphStruct(# (Seg (m + n)),ee #) ) & ex ee being Subset of (TWOELEMENTSETS (Seg (m + n))) st

( ee = { {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) ) } & b_{2} = SimpleGraphStruct(# (Seg (m + n)),ee #) ) holds

b_{1} = b_{2}
;

end;
func K_ (m,n) -> SimpleGraph of NAT means :: SGRAPH1:def 12

ex ee being Subset of (TWOELEMENTSETS (Seg (m + n))) st

( ee = { {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) ) } & it = SimpleGraphStruct(# (Seg (m + n)),ee #) );

existence ex ee being Subset of (TWOELEMENTSETS (Seg (m + n))) st

( ee = { {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) ) } & it = SimpleGraphStruct(# (Seg (m + n)),ee #) );

ex b

( ee = { {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) ) } & b

proof end;

uniqueness for b

( ee = { {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) ) } & b

( ee = { {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) ) } & b

b

:: deftheorem defines K_ SGRAPH1:def 12 :

for n, m being Element of NAT

for b_{3} being SimpleGraph of NAT holds

( b_{3} = K_ (m,n) iff ex ee being Subset of (TWOELEMENTSETS (Seg (m + n))) st

( ee = { {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) ) } & b_{3} = SimpleGraphStruct(# (Seg (m + n)),ee #) ) );

for n, m being Element of NAT

for b

( b

( ee = { {i,j} where i, j is Element of NAT : ( i in Seg m & j in nat_interval ((m + 1),(m + n)) ) } & b

definition

let n be Element of NAT ;

ex b_{1} being SimpleGraph of NAT ex ee being finite Subset of (TWOELEMENTSETS (Seg n)) st

( ee = { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } & b_{1} = SimpleGraphStruct(# (Seg n),ee #) )

for b_{1}, b_{2} being SimpleGraph of NAT st ex ee being finite Subset of (TWOELEMENTSETS (Seg n)) st

( ee = { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } & b_{1} = SimpleGraphStruct(# (Seg n),ee #) ) & ex ee being finite Subset of (TWOELEMENTSETS (Seg n)) st

( ee = { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } & b_{2} = SimpleGraphStruct(# (Seg n),ee #) ) holds

b_{1} = b_{2}
;

end;
func K_ n -> SimpleGraph of NAT means :Def13: :: SGRAPH1:def 13

ex ee being finite Subset of (TWOELEMENTSETS (Seg n)) st

( ee = { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } & it = SimpleGraphStruct(# (Seg n),ee #) );

existence ex ee being finite Subset of (TWOELEMENTSETS (Seg n)) st

( ee = { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } & it = SimpleGraphStruct(# (Seg n),ee #) );

ex b

( ee = { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } & b

proof end;

uniqueness for b

( ee = { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } & b

( ee = { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } & b

b

:: deftheorem Def13 defines K_ SGRAPH1:def 13 :

for n being Element of NAT

for b_{2} being SimpleGraph of NAT holds

( b_{2} = K_ n iff ex ee being finite Subset of (TWOELEMENTSETS (Seg n)) st

( ee = { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } & b_{2} = SimpleGraphStruct(# (Seg n),ee #) ) );

for n being Element of NAT

for b

( b

( ee = { {i,j} where i, j is Element of NAT : ( i in Seg n & j in Seg n & i <> j ) } & b

:: TriangleGraph will be used in the definition of planegraphs.

theorem Th34: :: SGRAPH1:34

ex ee being Subset of (TWOELEMENTSETS (Seg 3)) st

( ee = {.{.1,2.},{.2,3.},{.3,1.}.} & TriangleGraph = SimpleGraphStruct(# (Seg 3),ee #) )

( ee = {.{.1,2.},{.2,3.},{.3,1.}.} & TriangleGraph = SimpleGraphStruct(# (Seg 3),ee #) )

proof end;

theorem :: SGRAPH1:35

theorem :: SGRAPH1:36

( {1,2} in the SEdges of TriangleGraph & {2,3} in the SEdges of TriangleGraph & {3,1} in the SEdges of TriangleGraph ) by Th34, ENUMSET1:def 1;

:: so we use a symbol nat_interval here.

:: following the definition of Seg, I add an assumption 1 <= m.

:: but it is unnatural, I think.

:: I changed the proof of existence

:: so that the assumption (1 <= m) is not necessary.

:: now nat_interval has the very natural definition, I think (-: