:: Introduction to Graph Enumerations
:: by Sebastian Koch
::
:: Received March 31, 2023
:: Copyright (c) 2023-2025 Association of Mizar Users

::$INSERT "SG" is short for "Subgraphs".

definition

let G be _Graph;

func G .allSG() -> Graph-membered set equals :: GLENUM00:def 1
{ the plain inducedSubgraph of G,V,E where V is non empty Subset of (the_Vertices_of G), E is Subset of (the_Edges_of G) : E c= G .edgesBetween V } ;

coherence
{ the plain inducedSubgraph of G,V,E where V is non empty Subset of (the_Vertices_of G), E is Subset of (the_Edges_of G) : E c= G .edgesBetween V } is Graph-membered set

proof end;

end;

:: deftheorem defines .allSG() GLENUM00:def 1 :
for G being _Graph holds G .allSG() = { the plain inducedSubgraph of G,V,E where V is non empty Subset of (the_Vertices_of G), E is Subset of (the_Edges_of G) : E c= G .edgesBetween V } ;

registration

let G be _finite _Graph;

cluster G .allSG() -> finite Graph-membered ;

coherence
G .allSG() is finite

proof end;

end;

theorem Th1: :: GLENUM00:1

for G1, G2 being _Graph holds
( G2 in G1 .allSG() iff G2 is plain Subgraph of G1 )

proof end;

theorem Th2: :: GLENUM00:2

for G being _Graph
for H being Subgraph of G holds H | _GraphSelectors in G .allSG()

proof end;

theorem Th3: :: GLENUM00:3

for G being _Graph holds G | _GraphSelectors in G .allSG()

proof end;

Lm1: for G being _Graph
for V being non empty Subset of (the_Vertices_of G)
for S, T being Function of {},V holds createGraph (V,{},S,T) in G .allSG()

proof end;

definition

let G be _Graph;
let V be non empty Subset of (the_Vertices_of G);

func createGraph V -> plain Subgraph of G equals :: GLENUM00:def 2
createGraph (V,{}, the Function of {},V, the Function of {},V);

coherence
createGraph (V,{}, the Function of {},V, the Function of {},V) is plain Subgraph of G

proof end;

end;

:: deftheorem defines createGraph GLENUM00:def 2 :
for G being _Graph
for V being non empty Subset of (the_Vertices_of G) holds createGraph V = createGraph (V,{}, the Function of {},V, the Function of {},V);

registration

let G be _Graph;
let V be non empty Subset of (the_Vertices_of G);

cluster createGraph V -> edgeless plain ;

coherence
createGraph V is edgeless ;

end;

theorem Th4: :: GLENUM00:4

for G being _Graph
for V being non empty Subset of (the_Vertices_of G) holds createGraph V in G .allSG() by Lm1;

theorem Th5: :: GLENUM00:5

for G being _Graph
for V being non empty Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,V, {} holds H == createGraph V

proof end;

theorem Th6: :: GLENUM00:6

for G being _Graph
for H being removeEdges of G,(the_Edges_of G) holds H == createGraph ([#] (the_Vertices_of G))

proof end;

theorem Th7: :: GLENUM00:7

for G being _Graph holds
( G is edgeless iff G == createGraph ([#] (the_Vertices_of G)) )

proof end;

theorem Th8: :: GLENUM00:8

for G1, G2 being _Graph
for V being non empty Subset of (the_Vertices_of G1) st V c= the_Vertices_of G2 holds
createGraph V is Subgraph of G2

proof end;

theorem Th9: :: GLENUM00:9

for G being _Graph holds
( G is edgeless iff G .allSG() = { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } )

proof end;

Lm2: for G being _Graph
for v being Vertex of G
for S, T being Function of {},{v} holds createGraph ({v},{},S,T) in G .allSG()
by Lm1;

definition

let G be _Graph;
let v be Vertex of G;

func createGraph v -> plain Subgraph of G equals :: GLENUM00:def 3
createGraph {v};

coherence
createGraph {v} is plain Subgraph of G ;

end;

:: deftheorem defines createGraph GLENUM00:def 3 :
for G being _Graph
for v being Vertex of G holds createGraph v = createGraph {v};

registration

let G be _Graph;
let v be Vertex of G;

cluster createGraph v -> _trivial edgeless plain ;

coherence
( createGraph v is _trivial & createGraph v is edgeless ) ;

end;

theorem :: GLENUM00:10

for G being _Graph
for v being Vertex of G holds createGraph v in G .allSG() by Lm2;

theorem :: GLENUM00:11

for G being _Graph
for v being Vertex of G
for H being inducedSubgraph of G,{v}, {} holds H == createGraph v by Th5;

theorem :: GLENUM00:12

for G1, G2 being _Graph
for v being Vertex of G1 st v in the_Vertices_of G2 holds
createGraph v is Subgraph of G2 by Th8, ZFMISC_1:31;

definition

let G be non edgeless _Graph;
let e be Edge of G;

func createGraph e -> plain Subgraph of G means :Def4: :: GLENUM00:def 4
ex V being non empty Subset of (the_Vertices_of G) ex S, T being Function of {e},V st
( it = createGraph (V,{e},S,T) & {((the_Source_of G) . e),((the_Target_of G) . e)} = V & S = e .--> ((the_Source_of G) . e) & T = e .--> ((the_Target_of G) . e) );

existence
ex b₁ being plain Subgraph of G ex V being non empty Subset of (the_Vertices_of G) ex S, T being Function of {e},V st
( b₁ = createGraph (V,{e},S,T) & {((the_Source_of G) . e),((the_Target_of G) . e)} = V & S = e .--> ((the_Source_of G) . e) & T = e .--> ((the_Target_of G) . e) )

proof end;

uniqueness
for b₁, b₂ being plain Subgraph of G st ex V being non empty Subset of (the_Vertices_of G) ex S, T being Function of {e},V st
( b₁ = createGraph (V,{e},S,T) & {((the_Source_of G) . e),((the_Target_of G) . e)} = V & S = e .--> ((the_Source_of G) . e) & T = e .--> ((the_Target_of G) . e) ) & ex V being non empty Subset of (the_Vertices_of G) ex S, T being Function of {e},V st
( b₂ = createGraph (V,{e},S,T) & {((the_Source_of G) . e),((the_Target_of G) . e)} = V & S = e .--> ((the_Source_of G) . e) & T = e .--> ((the_Target_of G) . e) ) holds
b₁ = b₂ ;

end;

:: deftheorem Def4 defines createGraph GLENUM00:def 4 :
for G being non edgeless _Graph
for e being Edge of G
for b₃ being plain Subgraph of G holds
( b₃ = createGraph e iff ex V being non empty Subset of (the_Vertices_of G) ex S, T being Function of {e},V st
( b₃ = createGraph (V,{e},S,T) & {((the_Source_of G) . e),((the_Target_of G) . e)} = V & S = e .--> ((the_Source_of G) . e) & T = e .--> ((the_Target_of G) . e) ) );

theorem Th13: :: GLENUM00:13

for G being non edgeless _Graph
for e being Edge of G holds
( the_Edges_of (createGraph e) = {e} & the_Vertices_of (createGraph e) = {((the_Source_of G) . e),((the_Target_of G) . e)} )

proof end;

theorem Th14: :: GLENUM00:14

for G being non edgeless _Graph
for e being Edge of G holds e DJoins (the_Source_of G) . e,(the_Target_of G) . e, createGraph e

proof end;

theorem Th15: :: GLENUM00:15

for G being non edgeless _Graph
for e being Edge of G
for e0, v, w being object st e0 DJoins v,w, createGraph e holds
( e0 = e & v = (the_Source_of G) . e & w = (the_Target_of G) . e )

proof end;

theorem Th16: :: GLENUM00:16

for G being non edgeless _Graph
for e being Edge of G
for e0, v, w being object st e0 Joins v,w, createGraph e holds
e0 = e

proof end;

registration

let G be non edgeless _Graph;
let e be Edge of G;

cluster createGraph e -> _finite non-multi connected non edgeless plain ;

coherence
( not createGraph e is edgeless & createGraph e is non-multi & createGraph e is connected & createGraph e is _finite )

proof end;

end;

theorem Th17: :: GLENUM00:17

for G being non edgeless _Graph
for e being Edge of G holds
( createGraph e is loopless iff not e in G .loops() )

proof end;

theorem Th18: :: GLENUM00:18

for G being non edgeless _Graph
for e being Edge of G holds
( createGraph e is acyclic iff not e in G .loops() )

proof end;

theorem :: GLENUM00:19

for G being non edgeless _Graph
for e being Edge of G holds createGraph e in G .allSG() by Th1;

theorem :: GLENUM00:20

for G being non edgeless _Graph
for e being Edge of G
for H being inducedSubgraph of G,{((the_Source_of G) . e),((the_Target_of G) . e)},{e} holds H == createGraph e

proof end;

theorem Th21: :: GLENUM00:21

for G being non edgeless _Graph
for e being Edge of G
for V being Subset of (the_Vertices_of G)
for H being addVertices of createGraph e,V holds H is Subgraph of G

proof end;

theorem Th22: :: GLENUM00:22

for G being edgeless _Graph
for S being GraphUnionSet
for G9 being GraphUnion of S st ( for v being Vertex of G ex H9 being Element of S st v in the_Vertices_of H9 ) holds
G is Subgraph of G9

proof end;

theorem Th23: :: GLENUM00:23

for G being non edgeless _Graph
for S being GraphUnionSet
for G9 being GraphUnion of S st ( for v being Vertex of G ex H9 being Element of S st v in the_Vertices_of H9 ) & ( for e being Edge of G ex H9 being Element of S st createGraph e is Subgraph of H9 ) holds
G is Subgraph of G9

proof end;

theorem Th24: :: GLENUM00:24

for G being edgeless _Graph
for S being GraphUnionSet
for G9 being GraphUnion of S st ( for v being Vertex of G holds createGraph v in S ) holds
G is Subgraph of G9

proof end;

theorem Th25: :: GLENUM00:25

for G being non edgeless _Graph
for S being GraphUnionSet
for G9 being GraphUnion of S st ( for v being Vertex of G holds createGraph v in S ) & ( for e being Edge of G holds createGraph e in S ) holds
G is Subgraph of G9

proof end;

theorem Th26: :: GLENUM00:26

for G being non edgeless _Graph
for E being set
for e being Edge of G
for H being removeEdges of G,E st not e in E holds
createGraph e is Subgraph of H

proof end;

theorem Th27: :: GLENUM00:27

for G being non edgeless _Graph
for H being removeLoops of G
for S being GraphUnionSet
for G9 being GraphUnion of S st ( for v being Vertex of G ex H9 being Element of S st v in the_Vertices_of H9 ) & ( for e being Edge of G st not e in G .loops() holds
ex H9 being Element of S st createGraph e is Subgraph of H9 ) holds
H is Subgraph of G9

proof end;

theorem :: GLENUM00:28

for G being non edgeless _Graph
for H being removeLoops of G
for S being GraphUnionSet
for G9 being GraphUnion of S st ( for v being Vertex of G holds createGraph v in S ) & ( for e being Edge of G st not e in G .loops() holds
createGraph e in S ) holds
H is Subgraph of G9

proof end;

registration

let G be _Graph;

cluster G .allSG() -> non empty Graph-membered plain \/-tolerating ;

coherence
( not G .allSG() is empty & G .allSG() is \/-tolerating & G .allSG() is plain )

proof end;

end;

definition

let G be _Graph;
let S be non empty Subset of (G .allSG());
:: original: Element
redefine mode Element of S -> Subgraph of G;
coherence
for b₁ being Element of S holds b₁ is Subgraph of G

proof end;

end;

theorem Th29: :: GLENUM00:29

for G1, G2 being _Graph holds
( G2 .allSG() c= G1 .allSG() iff G2 is Subgraph of G1 )

proof end;

theorem :: GLENUM00:30

for G1, G2 being _Graph holds
( G1 == G2 iff G1 .allSG() = G2 .allSG() )

proof end;

definition

let G1, G2 be _Graph;
let F be PGraphMapping of G1,G2;

func SG2SGFunc F -> Function of (G1 .allSG()),(G2 .allSG()) means :Def5: :: GLENUM00:def 5
for H being plain Subgraph of G1 holds it . H = rng (F | H);

existence
ex b₁ being Function of (G1 .allSG()),(G2 .allSG()) st
for H being plain Subgraph of G1 holds b₁ . H = rng (F | H)

proof end;

uniqueness
for b₁, b₂ being Function of (G1 .allSG()),(G2 .allSG()) st ( for H being plain Subgraph of G1 holds b₁ . H = rng (F | H) ) & ( for H being plain Subgraph of G1 holds b₂ . H = rng (F | H) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines SG2SGFunc GLENUM00:def 5 :
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for b₄ being Function of (G1 .allSG()),(G2 .allSG()) holds
( b₄ = SG2SGFunc F iff for H being plain Subgraph of G1 holds b₄ . H = rng (F | H) );

registration

let G1, G2 be _Graph;
let F be PGraphMapping of G1,G2;

cluster SG2SGFunc F -> non empty Graph-yielding ;

coherence
( not SG2SGFunc F is empty & SG2SGFunc F is Graph-yielding )

proof end;

cluster dom (SG2SGFunc F) -> Graph-membered ;

coherence
dom (SG2SGFunc F) is Graph-membered ;

end;

registration

let G1, G2 be _Graph;
let F be PGraphMapping of G1,G2;

cluster dom (SG2SGFunc F) -> plain ;

coherence
dom (SG2SGFunc F) is plain ;

end;

theorem Th31: :: GLENUM00:31

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds
SG2SGFunc F is one-to-one

proof end;

registration

let G1 be _Graph;
let G2 be G1 -isomorphic _Graph;
let F be Isomorphism of G1,G2;

cluster SG2SGFunc F -> one-to-one ;

coherence
SG2SGFunc F is one-to-one by Th31;

end;

theorem Th32: :: GLENUM00:32

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is onto holds
rng (SG2SGFunc F) = G2 .allSG()

proof end;

:: the other direction doesn't hold for all graphs, but for finite ones
:: which is not proven here

theorem :: GLENUM00:33

for G1, G2 being _Graph st G2 is G1 -Disomorphic holds
G1 .allSG() ,G2 .allSG() are_Disomorphic

proof end;

theorem :: GLENUM00:34

for G1, G2 being _Graph st G2 is G1 -isomorphic holds
G1 .allSG() ,G2 .allSG() are_isomorphic

proof end;

theorem Th35: :: GLENUM00:35

for G being _Graph holds G is GraphUnion of G .allSG()

proof end;

theorem Th36: :: GLENUM00:36

for G being _Graph holds
( ( G is loopless implies G .allSG() is loopless ) & ( G .allSG() is loopless implies G is loopless ) & ( G is non-multi implies G .allSG() is non-multi ) & ( G .allSG() is non-multi implies G is non-multi ) & ( G is non-Dmulti implies G .allSG() is non-Dmulti ) & ( G .allSG() is non-Dmulti implies G is non-Dmulti ) & ( G is simple implies G .allSG() is simple ) & ( G .allSG() is simple implies G is simple ) & ( G is Dsimple implies G .allSG() is Dsimple ) & ( G .allSG() is Dsimple implies G is Dsimple ) & ( G is acyclic implies G .allSG() is acyclic ) & ( G .allSG() is acyclic implies G is acyclic ) & ( G is edgeless implies G .allSG() is edgeless ) & ( G .allSG() is edgeless implies G is edgeless ) )

proof end;

registration

let G be loopless _Graph;

cluster G .allSG() -> Graph-membered loopless ;

coherence
G .allSG() is loopless by Th36;

end;

registration

let G be non-multi _Graph;

cluster G .allSG() -> Graph-membered non-multi ;

coherence
G .allSG() is non-multi by Th36;

end;

registration

let G be non-Dmulti _Graph;

cluster G .allSG() -> Graph-membered non-Dmulti ;

coherence
G .allSG() is non-Dmulti by Th36;

end;

registration

let G be simple _Graph;

cluster G .allSG() -> Graph-membered simple ;

coherence
G .allSG() is simple ;

end;

registration

let G be Dsimple _Graph;

cluster G .allSG() -> Graph-membered Dsimple ;

coherence
G .allSG() is Dsimple ;

end;

registration

let G be acyclic _Graph;

cluster G .allSG() -> Graph-membered acyclic ;

coherence
G .allSG() is acyclic by Th36;

end;

registration

let G be edgeless _Graph;

cluster G .allSG() -> Graph-membered edgeless ;

coherence
G .allSG() is edgeless by Th36;

end;

theorem Th37: :: GLENUM00:37

for G being _Graph holds the_Vertices_of (G .allSG()) = (bool (the_Vertices_of G)) \ {{}}

proof end;

theorem Th38: :: GLENUM00:38

for G being _Graph holds the_Edges_of (G .allSG()) = bool (the_Edges_of G)

proof end;

definition

let G be _Graph;

func SubgraphRel G -> Relation of (G .allSG()) means :Def6: :: GLENUM00:def 6
for H1, H2 being Element of G .allSG() holds
( [H1,H2] in it iff H1 is Subgraph of H2 );

existence
ex b₁ being Relation of (G .allSG()) st
for H1, H2 being Element of G .allSG() holds
( [H1,H2] in b₁ iff H1 is Subgraph of H2 )

proof end;

uniqueness
for b₁, b₂ being Relation of (G .allSG()) st ( for H1, H2 being Element of G .allSG() holds
( [H1,H2] in b₁ iff H1 is Subgraph of H2 ) ) & ( for H1, H2 being Element of G .allSG() holds
( [H1,H2] in b₂ iff H1 is Subgraph of H2 ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines SubgraphRel GLENUM00:def 6 :
for G being _Graph
for b₂ being Relation of (G .allSG()) holds
( b₂ = SubgraphRel G iff for H1, H2 being Element of G .allSG() holds
( [H1,H2] in b₂ iff H1 is Subgraph of H2 ) );

theorem Th39: :: GLENUM00:39

for G being _Graph
for H being Subgraph of G holds [(H | _GraphSelectors),(G | _GraphSelectors)] in SubgraphRel G

proof end;

theorem Th40: :: GLENUM00:40

for G being _Graph holds field (SubgraphRel G) = G .allSG()

proof end;

theorem Th41: :: GLENUM00:41

for G being _Graph holds SubgraphRel G partially_orders G .allSG()

proof end;

registration

let G be _Graph;

cluster SubgraphRel G -> reflexive antisymmetric transitive being_partial-order ;

coherence
( SubgraphRel G is reflexive & SubgraphRel G is antisymmetric & SubgraphRel G is transitive & SubgraphRel G is being_partial-order )

proof end;

end;

theorem :: GLENUM00:42

for G being _Graph holds G | _GraphSelectors is_maximal_in SubgraphRel G

proof end;

theorem Th43: :: GLENUM00:43

for G being _Graph
for H being Subgraph of G holds SubgraphRel H = (SubgraphRel G) |_2 (H .allSG())

proof end;

theorem Th44: :: GLENUM00:44

for G being _Graph
for S being non empty Subset of (G .allSG())
for G9 being GraphUnion of S st (SubgraphRel G) |_2 S is being_linear-order holds
for W being Walk of G9 ex H being Element of S st W is Walk of H

proof end;

definition

let G be _Graph;

func G .allInducedSG() -> Subset of (G .allSG()) equals :: GLENUM00:def 7
{ the plain inducedSubgraph of G,V where V is non empty Subset of (the_Vertices_of G) : verum } ;

coherence
{ the plain inducedSubgraph of G,V where V is non empty Subset of (the_Vertices_of G) : verum } is Subset of (G .allSG())

proof end;

end;

:: deftheorem defines .allInducedSG() GLENUM00:def 7 :
for G being _Graph holds G .allInducedSG() = { the plain inducedSubgraph of G,V where V is non empty Subset of (the_Vertices_of G) : verum } ;

theorem Th45: :: GLENUM00:45

for G1, G2 being _Graph holds
( G2 in G1 .allInducedSG() iff ex V being non empty Subset of (the_Vertices_of G1) st G2 is plain inducedSubgraph of G1,V )

proof end;

registration

let G be vertex-finite _Graph;

cluster G .allInducedSG() -> finite ;

coherence
G .allInducedSG() is finite

proof end;

end;

theorem Th46: :: GLENUM00:46

for G being _Graph
for V being non empty Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,V holds H | _GraphSelectors in G .allInducedSG()

proof end;

theorem Th47: :: GLENUM00:47

for G being _Graph holds G | _GraphSelectors in G .allInducedSG()

proof end;

registration

let G be _Graph;

cluster G .allInducedSG() -> non empty plain \/-tolerating ;

coherence
( not G .allInducedSG() is empty & G .allInducedSG() is \/-tolerating & G .allInducedSG() is plain ) by Th47;

end;

theorem Th48: :: GLENUM00:48

for G1, G2 being _Graph holds
( G2 .allInducedSG() c= G1 .allInducedSG() iff ex V being non empty Subset of (the_Vertices_of G1) st G2 is inducedSubgraph of G1,V )

proof end;

theorem Th49: :: GLENUM00:49

for G1, G2 being _Graph holds
( G1 == G2 iff G1 .allInducedSG() = G2 .allInducedSG() )

proof end;

theorem Th50: :: GLENUM00:50

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is total & F is onto holds
G2 .allInducedSG() c= rng ((SG2SGFunc F) | (G1 .allInducedSG()))

proof end;

theorem Th51: :: GLENUM00:51

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is total & F is continuous holds
rng ((SG2SGFunc F) | (G1 .allInducedSG())) c= G2 .allInducedSG()

proof end;

theorem Th52: :: GLENUM00:52

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
rng ((SG2SGFunc F) | (G1 .allInducedSG())) = G2 .allInducedSG()

proof end;

theorem :: GLENUM00:53

for G1, G2 being _Graph st G2 is G1 -Disomorphic holds
G1 .allInducedSG() ,G2 .allInducedSG() are_Disomorphic

proof end;

theorem :: GLENUM00:54

for G1, G2 being _Graph st G2 is G1 -isomorphic holds
G1 .allInducedSG() ,G2 .allInducedSG() are_isomorphic

proof end;

theorem Th55: :: GLENUM00:55

for G being _Graph holds G is GraphUnion of G .allInducedSG()

proof end;

theorem Th56: :: GLENUM00:56

for G being _Graph holds
( ( G is loopless implies G .allInducedSG() is loopless ) & ( G .allInducedSG() is loopless implies G is loopless ) & ( G is non-multi implies G .allInducedSG() is non-multi ) & ( G .allInducedSG() is non-multi implies G is non-multi ) & ( G is non-Dmulti implies G .allInducedSG() is non-Dmulti ) & ( G .allInducedSG() is non-Dmulti implies G is non-Dmulti ) & ( G is simple implies G .allInducedSG() is simple ) & ( G .allInducedSG() is simple implies G is simple ) & ( G is Dsimple implies G .allInducedSG() is Dsimple ) & ( G .allInducedSG() is Dsimple implies G is Dsimple ) & ( G is acyclic implies G .allInducedSG() is acyclic ) & ( G .allInducedSG() is acyclic implies G is acyclic ) & ( G is edgeless implies G .allInducedSG() is edgeless ) & ( G .allInducedSG() is edgeless implies G is edgeless ) & ( G is chordal implies G .allInducedSG() is chordal ) & ( G .allInducedSG() is chordal implies G is chordal ) & ( G is loopfull implies G .allInducedSG() is loopfull ) & ( G .allInducedSG() is loopfull implies G is loopfull ) )

proof end;

registration

let G be loopless _Graph;

cluster G .allInducedSG() -> loopless ;

coherence
G .allInducedSG() is loopless ;

end;

registration

let G be non-multi _Graph;

cluster G .allInducedSG() -> non-multi ;

coherence
G .allInducedSG() is non-multi ;

end;

registration

let G be non-Dmulti _Graph;

cluster G .allInducedSG() -> non-Dmulti ;

coherence
G .allInducedSG() is non-Dmulti ;

end;

registration

let G be simple _Graph;

cluster G .allInducedSG() -> simple ;

coherence
G .allInducedSG() is simple ;

end;

registration

let G be Dsimple _Graph;

cluster G .allInducedSG() -> Dsimple ;

coherence
G .allInducedSG() is Dsimple ;

end;

registration

let G be acyclic _Graph;

cluster G .allInducedSG() -> acyclic ;

coherence
G .allInducedSG() is acyclic ;

end;

registration

let G be edgeless _Graph;

cluster G .allInducedSG() -> edgeless ;

coherence
G .allInducedSG() is edgeless ;

end;

registration

let G be chordal _Graph;

cluster G .allInducedSG() -> chordal ;

coherence
G .allInducedSG() is chordal by Th56;

end;

registration

let G be loopfull _Graph;

cluster G .allInducedSG() -> loopfull ;

coherence
G .allInducedSG() is loopfull by Th56;

end;

theorem Th57: :: GLENUM00:57

for G being _Graph holds
( G is edgeless iff G .allInducedSG() = { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } )

proof end;

theorem :: GLENUM00:58

for G being _Graph holds
( G is edgeless iff G .allSG() = G .allInducedSG() )

proof end;

theorem :: GLENUM00:59

for G being _Graph holds the_Vertices_of (G .allInducedSG()) = (bool (the_Vertices_of G)) \ {{}}

proof end;

::$INSERT The following functor could also be named G.allFactors().

definition

let G be _Graph;

func G .allSpanningSG() -> Subset of (G .allSG()) equals :: GLENUM00:def 8
{ H where H is Element of [#] (G .allSG()) : H is spanning } ;

coherence
{ H where H is Element of [#] (G .allSG()) : H is spanning } is Subset of (G .allSG())

proof end;

end;

:: deftheorem defines .allSpanningSG() GLENUM00:def 8 :
for G being _Graph holds G .allSpanningSG() = { H where H is Element of [#] (G .allSG()) : H is spanning } ;

theorem Th60: :: GLENUM00:60

for G1, G2 being _Graph holds
( G2 in G1 .allSpanningSG() iff G2 is spanning plain Subgraph of G1 )

proof end;

theorem Th61: :: GLENUM00:61

for G being _Graph
for H being spanning Subgraph of G holds H | _GraphSelectors in G .allSpanningSG()

proof end;

theorem Th62: :: GLENUM00:62

for G being _Graph holds G | _GraphSelectors in G .allSpanningSG()

proof end;

theorem Th63: :: GLENUM00:63

for G being _Graph holds createGraph ([#] (the_Vertices_of G)) in G .allSpanningSG()

proof end;

theorem Th64: :: GLENUM00:64

for G being non edgeless _Graph
for e being Edge of G
for H being plain addVertices of createGraph e, the_Vertices_of G holds H in G .allSpanningSG()

proof end;

registration

let G be _Graph;

cluster G .allSpanningSG() -> non empty plain \/-tolerating ;

coherence
( not G .allSpanningSG() is empty & G .allSpanningSG() is \/-tolerating & G .allSpanningSG() is plain ) by Th62;

end;

theorem Th65: :: GLENUM00:65

for G1, G2 being _Graph holds
( G2 .allSpanningSG() c= G1 .allSpanningSG() iff G2 is spanning Subgraph of G1 )

proof end;

theorem :: GLENUM00:66

for G1, G2 being _Graph holds
( G1 == G2 iff G1 .allSpanningSG() = G2 .allSpanningSG() )

proof end;

theorem Th67: :: GLENUM00:67

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st rng (F _V) = the_Vertices_of G2 holds
rng ((SG2SGFunc F) | (G1 .allSpanningSG())) c= G2 .allSpanningSG()

proof end;

theorem Th68: :: GLENUM00:68

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is onto & F _V is one-to-one & F _V is total holds
rng ((SG2SGFunc F) | (G1 .allSpanningSG())) = G2 .allSpanningSG()

proof end;

theorem Th69: :: GLENUM00:69

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
rng ((SG2SGFunc F) | (G1 .allSpanningSG())) = G2 .allSpanningSG()

proof end;

theorem :: GLENUM00:70

for G1, G2 being _Graph st G2 is G1 -Disomorphic holds
G1 .allSpanningSG() ,G2 .allSpanningSG() are_Disomorphic

proof end;

theorem :: GLENUM00:71

for G1, G2 being _Graph st G2 is G1 -isomorphic holds
G1 .allSpanningSG() ,G2 .allSpanningSG() are_isomorphic

proof end;

theorem Th72: :: GLENUM00:72

for G being _Graph holds G is GraphUnion of G .allSpanningSG()

proof end;

theorem :: GLENUM00:73

for G being _Graph holds
( ( G is loopless implies G .allSpanningSG() is loopless ) & ( G .allSpanningSG() is loopless implies G is loopless ) & ( G is non-multi implies G .allSpanningSG() is non-multi ) & ( G .allSpanningSG() is non-multi implies G is non-multi ) & ( G is non-Dmulti implies G .allSpanningSG() is non-Dmulti ) & ( G .allSpanningSG() is non-Dmulti implies G is non-Dmulti ) & ( G is simple implies G .allSpanningSG() is simple ) & ( G .allSpanningSG() is simple implies G is simple ) & ( G is Dsimple implies G .allSpanningSG() is Dsimple ) & ( G .allSpanningSG() is Dsimple implies G is Dsimple ) & ( G is acyclic implies G .allSpanningSG() is acyclic ) & ( G .allSpanningSG() is acyclic implies G is acyclic ) & ( G is edgeless implies G .allSpanningSG() is edgeless ) & ( G .allSpanningSG() is edgeless implies G is edgeless ) )

proof end;

registration

let G be loopless _Graph;

cluster G .allSpanningSG() -> loopless ;

coherence
G .allSpanningSG() is loopless ;

end;

registration

let G be non-multi _Graph;

cluster G .allSpanningSG() -> non-multi ;

coherence
G .allSpanningSG() is non-multi ;

end;

registration

let G be non-Dmulti _Graph;

cluster G .allSpanningSG() -> non-Dmulti ;

coherence
G .allSpanningSG() is non-Dmulti ;

end;

registration

let G be simple _Graph;

cluster G .allSpanningSG() -> simple ;

coherence
G .allSpanningSG() is simple ;

end;

registration

let G be Dsimple _Graph;

cluster G .allSpanningSG() -> Dsimple ;

coherence
G .allSpanningSG() is Dsimple ;

end;

registration

let G be acyclic _Graph;

cluster G .allSpanningSG() -> acyclic ;

coherence
G .allSpanningSG() is acyclic ;

end;

registration

let G be edgeless _Graph;

cluster G .allSpanningSG() -> edgeless ;

coherence
G .allSpanningSG() is edgeless ;

end;

theorem :: GLENUM00:74

for G being _Graph holds
( G is edgeless iff G .allSpanningSG() = {(G | _GraphSelectors)} )

proof end;

theorem Th75: :: GLENUM00:75

for G being _Graph holds the_Vertices_of (G .allSpanningSG()) = {(the_Vertices_of G)}

proof end;

theorem :: GLENUM00:76

for G being _Graph holds the_Edges_of (G .allSpanningSG()) = bool (the_Edges_of G)

proof end;

theorem :: GLENUM00:77

for G being _Graph holds (G .allInducedSG()) /\ (G .allSpanningSG()) = {(G | _GraphSelectors)}

proof end;

definition

let G be _Graph;

func G .allForests() -> Subset of (G .allSG()) equals :: GLENUM00:def 9
{ H where H is Element of [#] (G .allSG()) : H is acyclic } ;

coherence
{ H where H is Element of [#] (G .allSG()) : H is acyclic } is Subset of (G .allSG())

proof end;

end;

:: deftheorem defines .allForests() GLENUM00:def 9 :
for G being _Graph holds G .allForests() = { H where H is Element of [#] (G .allSG()) : H is acyclic } ;

theorem Th78: :: GLENUM00:78

for G1, G2 being _Graph holds
( G2 in G1 .allForests() iff G2 is acyclic plain Subgraph of G1 )

proof end;

theorem Th79: :: GLENUM00:79

for G being _Graph
for H being acyclic Subgraph of G holds H | _GraphSelectors in G .allForests()

proof end;

theorem Th80: :: GLENUM00:80

for G being _Graph holds
( G is acyclic iff G | _GraphSelectors in G .allForests() )

proof end;

theorem Th81: :: GLENUM00:81

for G being _Graph
for V being non empty Subset of (the_Vertices_of G) holds createGraph V in G .allForests() by Th78;

theorem Th82: :: GLENUM00:82

for G being _Graph
for v being Vertex of G holds createGraph v in G .allForests() by Th81;

theorem Th83: :: GLENUM00:83

for G being non edgeless _Graph
for e being Edge of G st not e in G .loops() holds
createGraph e in G .allForests()

proof end;

theorem Th84: :: GLENUM00:84

for G being non edgeless _Graph
for e being Edge of G
for V being Subset of (the_Vertices_of G)
for H being plain addVertices of createGraph e,V st not e in G .loops() holds
H in G .allForests()

proof end;

registration

let G be _Graph;

cluster G .allForests() -> non empty plain simple acyclic \/-tolerating ;

coherence
( not G .allForests() is empty & G .allForests() is \/-tolerating & G .allForests() is plain & G .allForests() is acyclic & G .allForests() is simple )

proof end;

end;

theorem Th85: :: GLENUM00:85

for G being _Graph
for H being Subgraph of G holds H .allForests() c= G .allForests()

proof end;

theorem Th86: :: GLENUM00:86

for G1 being _Graph
for G2 being loopless _Graph st G2 .allForests() c= G1 .allForests() holds
G2 is Subgraph of G1

proof end;

theorem Th87: :: GLENUM00:87

for G being _Graph
for H being removeLoops of G holds G .allForests() = H .allForests()

proof end;

theorem Th88: :: GLENUM00:88

for G1, G2 being loopless _Graph holds
( G1 == G2 iff G1 .allForests() = G2 .allForests() )

proof end;

theorem :: GLENUM00:89

for G1, G2 being _Graph
for G3 being removeLoops of G1
for G4 being removeLoops of G2 holds
( G3 == G4 iff G1 .allForests() = G2 .allForests() )

proof end;

theorem Th90: :: GLENUM00:90

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds
rng ((SG2SGFunc F) | (G1 .allForests())) c= G2 .allForests()

proof end;

theorem Th91: :: GLENUM00:91

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is one-to-one & F is onto holds
G2 .allForests() c= rng ((SG2SGFunc F) | (G1 .allForests()))

proof end;

theorem Th92: :: GLENUM00:92

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
G2 .allForests() = rng ((SG2SGFunc F) | (G1 .allForests()))

proof end;

theorem Th93: :: GLENUM00:93

for G1, G2 being _Graph st G2 is G1 -Disomorphic holds
G1 .allForests() ,G2 .allForests() are_Disomorphic

proof end;

theorem Th94: :: GLENUM00:94

for G1, G2 being _Graph st G2 is G1 -isomorphic holds
G1 .allForests() ,G2 .allForests() are_isomorphic

proof end;

theorem :: GLENUM00:95

for G1, G2 being _Graph
for G3 being removeLoops of G1
for G4 being removeLoops of G2 st G4 is G3 -Disomorphic holds
G1 .allForests() ,G2 .allForests() are_Disomorphic

proof end;

theorem :: GLENUM00:96

for G1, G2 being _Graph
for G3 being removeLoops of G1
for G4 being removeLoops of G2 st G4 is G3 -isomorphic holds
G1 .allForests() ,G2 .allForests() are_isomorphic

proof end;

theorem Th97: :: GLENUM00:97

for G being _Graph
for H being removeLoops of G holds H is GraphUnion of G .allForests()

proof end;

theorem :: GLENUM00:98

for G being _Graph holds
( G is loopless iff G is GraphUnion of G .allForests() )

proof end;

theorem Th99: :: GLENUM00:99

for G being _Graph holds
( the_Edges_of G = G .loops() iff G .allForests() is edgeless )

proof end;

theorem :: GLENUM00:100

for G being _Graph holds
( the_Edges_of G = G .loops() iff G .allForests() = { (createGraph V) where V is non empty Subset of (the_Vertices_of G) : verum } )

proof end;

theorem :: GLENUM00:101

for G being _Graph holds the_Vertices_of (G .allForests()) = (bool (the_Vertices_of G)) \ {{}}

proof end;

definition

let G be _Graph;

func G .allSpanningForests() -> Subset of (G .allSG()) equals :: GLENUM00:def 10
{ H where H is Element of [#] (G .allSG()) : ( H is spanning & H is acyclic ) } ;

coherence
{ H where H is Element of [#] (G .allSG()) : ( H is spanning & H is acyclic ) } is Subset of (G .allSG())

proof end;

end;

:: deftheorem defines .allSpanningForests() GLENUM00:def 10 :
for G being _Graph holds G .allSpanningForests() = { H where H is Element of [#] (G .allSG()) : ( H is spanning & H is acyclic ) } ;

theorem Th102: :: GLENUM00:102

for G1, G2 being _Graph holds
( G2 in G1 .allSpanningForests() iff G2 is spanning acyclic plain Subgraph of G1 )

proof end;

theorem Th103: :: GLENUM00:103

for G being _Graph holds G .allSpanningForests() = (G .allSpanningSG()) /\ (G .allForests())

proof end;

theorem Th104: :: GLENUM00:104

for G being _Graph
for H being spanning acyclic Subgraph of G holds H | _GraphSelectors in G .allSpanningForests()

proof end;

theorem :: GLENUM00:105

for G being _Graph holds
( G is acyclic iff G | _GraphSelectors in G .allSpanningForests() )

proof end;

theorem Th106: :: GLENUM00:106

for G being _Graph holds createGraph ([#] (the_Vertices_of G)) in G .allSpanningForests()

proof end;

theorem Th107: :: GLENUM00:107

for G being non edgeless _Graph
for e being Edge of G
for H being plain addVertices of createGraph e, the_Vertices_of G st not e in G .loops() holds
H in G .allSpanningForests()

proof end;

registration

let G be _Graph;

cluster G .allSpanningForests() -> non empty plain simple acyclic \/-tolerating ;

coherence
( not G .allSpanningForests() is empty & G .allSpanningForests() is \/-tolerating & G .allSpanningForests() is plain & G .allSpanningForests() is acyclic & G .allSpanningForests() is simple )

proof end;

end;

theorem Th108: :: GLENUM00:108

for G being _Graph
for H being spanning Subgraph of G holds H .allSpanningForests() c= G .allSpanningForests()

proof end;

theorem Th109: :: GLENUM00:109

for G1 being _Graph
for G2 being loopless _Graph st G2 .allSpanningForests() c= G1 .allSpanningForests() holds
G2 is spanning Subgraph of G1

proof end;

theorem Th110: :: GLENUM00:110

for G being _Graph
for H being removeLoops of G holds G .allSpanningForests() = H .allSpanningForests()

proof end;

theorem Th111: :: GLENUM00:111

for G1, G2 being loopless _Graph holds
( G1 == G2 iff G1 .allSpanningForests() = G2 .allSpanningForests() )

proof end;

theorem :: GLENUM00:112

for G1, G2 being _Graph
for G3 being removeLoops of G1
for G4 being removeLoops of G2 holds
( G3 == G4 iff G1 .allSpanningForests() = G2 .allSpanningForests() )

proof end;

theorem Th113: :: GLENUM00:113

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding & rng (F _V) = the_Vertices_of G2 holds
rng ((SG2SGFunc F) | (G1 .allSpanningForests())) c= G2 .allSpanningForests()

proof end;

theorem Th114: :: GLENUM00:114

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding & F is onto holds
G2 .allSpanningForests() = rng ((SG2SGFunc F) | (G1 .allSpanningForests()))

proof end;

theorem Th115: :: GLENUM00:115

for G1, G2 being _Graph st G2 is G1 -Disomorphic holds
G1 .allSpanningForests() ,G2 .allSpanningForests() are_Disomorphic

proof end;

theorem Th116: :: GLENUM00:116

for G1, G2 being _Graph st G2 is G1 -isomorphic holds
G1 .allSpanningForests() ,G2 .allSpanningForests() are_isomorphic

proof end;

theorem :: GLENUM00:117

for G1, G2 being _Graph
for G3 being removeLoops of G1
for G4 being removeLoops of G2 st G4 is G3 -Disomorphic holds
G1 .allSpanningForests() ,G2 .allSpanningForests() are_Disomorphic

proof end;

theorem :: GLENUM00:118

for G1, G2 being _Graph
for G3 being removeLoops of G1
for G4 being removeLoops of G2 st G4 is G3 -isomorphic holds
G1 .allSpanningForests() ,G2 .allSpanningForests() are_isomorphic

proof end;

theorem Th119: :: GLENUM00:119

for G being _Graph
for H being removeLoops of G holds H is GraphUnion of G .allSpanningForests()

proof end;

theorem :: GLENUM00:120

for G being _Graph holds
( G is loopless iff G is GraphUnion of G .allSpanningForests() )

proof end;

theorem :: GLENUM00:121

for G being _Graph holds
( the_Edges_of G = G .loops() iff G .allSpanningForests() is edgeless )

proof end;

theorem :: GLENUM00:122

for G being _Graph holds
( the_Edges_of G = G .loops() iff for H being removeLoops of G holds G .allSpanningForests() = {(H | _GraphSelectors)} )

proof end;

theorem Th123: :: GLENUM00:123

for G being _Graph holds the_Vertices_of (G .allSpanningForests()) = {(the_Vertices_of G)}

proof end;

definition

let G be _Graph;

func G .allConnectedSG() -> Subset of (G .allSG()) equals :: GLENUM00:def 11
{ H where H is Element of [#] (G .allSG()) : H is connected } ;

coherence
{ H where H is Element of [#] (G .allSG()) : H is connected } is Subset of (G .allSG())

proof end;

end;

:: deftheorem defines .allConnectedSG() GLENUM00:def 11 :
for G being _Graph holds G .allConnectedSG() = { H where H is Element of [#] (G .allSG()) : H is connected } ;

theorem Th124: :: GLENUM00:124

for G1, G2 being _Graph holds
( G2 in G1 .allConnectedSG() iff G2 is connected plain Subgraph of G1 )

proof end;

theorem Th125: :: GLENUM00:125

for G being _Graph
for H being connected Subgraph of G holds H | _GraphSelectors in G .allConnectedSG()

proof end;

theorem :: GLENUM00:126

for G being _Graph holds
( G is connected iff G | _GraphSelectors in G .allConnectedSG() )

proof end;

theorem Th127: :: GLENUM00:127

for G being _Graph
for v being Vertex of G holds createGraph v in G .allConnectedSG() by Th124;

theorem Th128: :: GLENUM00:128

for G being non edgeless _Graph
for e being Edge of G holds createGraph e in G .allConnectedSG() by Th124;

registration

let G be _Graph;

cluster G .allConnectedSG() -> non empty plain connected \/-tolerating ;

coherence
( not G .allConnectedSG() is empty & G .allConnectedSG() is \/-tolerating & G .allConnectedSG() is plain & G .allConnectedSG() is connected )

proof end;

end;

theorem Th129: :: GLENUM00:129

for G being _Graph
for H being Subgraph of G holds H .allConnectedSG() c= G .allConnectedSG()

proof end;

theorem Th130: :: GLENUM00:130

for G1, G2 being _Graph st G2 .allConnectedSG() c= G1 .allConnectedSG() holds
G2 is Subgraph of G1

proof end;

theorem :: GLENUM00:131

for G1, G2 being _Graph holds
( G1 == G2 iff G1 .allConnectedSG() = G2 .allConnectedSG() )

proof end;

theorem Th132: :: GLENUM00:132

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is total holds
rng ((SG2SGFunc F) | (G1 .allConnectedSG())) c= G2 .allConnectedSG()

proof end;

theorem Th133: :: GLENUM00:133

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is one-to-one & F is onto holds
G2 .allConnectedSG() c= rng ((SG2SGFunc F) | (G1 .allConnectedSG()))

proof end;

theorem Th134: :: GLENUM00:134

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
G2 .allConnectedSG() = rng ((SG2SGFunc F) | (G1 .allConnectedSG()))

proof end;

theorem :: GLENUM00:135

for G1, G2 being _Graph st G2 is G1 -Disomorphic holds
G1 .allConnectedSG() ,G2 .allConnectedSG() are_Disomorphic

proof end;

theorem :: GLENUM00:136

for G1, G2 being _Graph st G2 is G1 -isomorphic holds
G1 .allConnectedSG() ,G2 .allConnectedSG() are_isomorphic

proof end;

theorem :: GLENUM00:137

for G being _Graph holds G is GraphUnion of G .allConnectedSG()

proof end;

definition

let G be _Graph;

func G .allTrees() -> Subset of (G .allSG()) equals :: GLENUM00:def 12
{ H where H is Element of [#] (G .allSG()) : H is Tree-like } ;

coherence
{ H where H is Element of [#] (G .allSG()) : H is Tree-like } is Subset of (G .allSG())

proof end;

end;

:: deftheorem defines .allTrees() GLENUM00:def 12 :
for G being _Graph holds G .allTrees() = { H where H is Element of [#] (G .allSG()) : H is Tree-like } ;

theorem Th138: :: GLENUM00:138

for G1, G2 being _Graph holds
( G2 in G1 .allTrees() iff G2 is Tree-like plain Subgraph of G1 )

proof end;

theorem Th139: :: GLENUM00:139

for G being _Graph holds G .allTrees() = (G .allForests()) /\ (G .allConnectedSG())

proof end;

theorem Th140: :: GLENUM00:140

for G being _Graph
for H being Tree-like Subgraph of G holds H | _GraphSelectors in G .allTrees()

proof end;

theorem Th141: :: GLENUM00:141

for G being _Graph holds
( G is Tree-like iff G | _GraphSelectors in G .allTrees() )

proof end;

theorem Th142: :: GLENUM00:142

for G being _Graph
for v being Vertex of G holds createGraph v in G .allTrees() by Th138;

theorem Th143: :: GLENUM00:143

for G being non edgeless _Graph
for e being Edge of G st not e in G .loops() holds
createGraph e in G .allTrees()

proof end;

registration

let G be _Graph;

cluster G .allTrees() -> non empty plain simple Tree-like \/-tolerating ;

coherence
( not G .allTrees() is empty & G .allTrees() is \/-tolerating & G .allTrees() is plain & G .allTrees() is Tree-like & G .allTrees() is simple )

proof end;

end;

theorem Th144: :: GLENUM00:144

for G being _Graph
for H being Subgraph of G holds H .allTrees() c= G .allTrees()

proof end;

theorem Th145: :: GLENUM00:145

for G1 being _Graph
for G2 being loopless _Graph st G2 .allTrees() c= G1 .allTrees() holds
G2 is Subgraph of G1

proof end;

theorem Th146: :: GLENUM00:146

for G being _Graph
for H being removeLoops of G holds G .allTrees() = H .allTrees()

proof end;

theorem Th147: :: GLENUM00:147

for G1, G2 being loopless _Graph holds
( G1 == G2 iff G1 .allTrees() = G2 .allTrees() )

proof end;

theorem :: GLENUM00:148

for G1, G2 being _Graph
for G3 being removeLoops of G1
for G4 being removeLoops of G2 holds
( G3 == G4 iff G1 .allTrees() = G2 .allTrees() )

proof end;

theorem Th149: :: GLENUM00:149

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds
rng ((SG2SGFunc F) | (G1 .allTrees())) c= G2 .allTrees()

proof end;

theorem Th150: :: GLENUM00:150

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding & F is onto holds
G2 .allTrees() = rng ((SG2SGFunc F) | (G1 .allTrees()))

proof end;

theorem Th151: :: GLENUM00:151

for G1, G2 being _Graph st G2 is G1 -Disomorphic holds
G1 .allTrees() ,G2 .allTrees() are_Disomorphic

proof end;

theorem Th152: :: GLENUM00:152

for G1, G2 being _Graph st G2 is G1 -isomorphic holds
G1 .allTrees() ,G2 .allTrees() are_isomorphic

proof end;

theorem :: GLENUM00:153

for G1, G2 being _Graph
for G3 being removeLoops of G1
for G4 being removeLoops of G2 st G4 is G3 -Disomorphic holds
G1 .allTrees() ,G2 .allTrees() are_Disomorphic

proof end;

theorem :: GLENUM00:154

for G1, G2 being _Graph
for G3 being removeLoops of G1
for G4 being removeLoops of G2 st G4 is G3 -isomorphic holds
G1 .allTrees() ,G2 .allTrees() are_isomorphic

proof end;

theorem Th155: :: GLENUM00:155

for G being _Graph
for H being removeLoops of G holds H is GraphUnion of G .allTrees()

proof end;

theorem :: GLENUM00:156

for G being _Graph holds
( G is loopless iff G is GraphUnion of G .allTrees() )

proof end;

theorem Th157: :: GLENUM00:157

for G being _Graph holds
( the_Edges_of G = G .loops() iff G .allTrees() is edgeless )

proof end;

theorem :: GLENUM00:158

for G being _Graph holds
( the_Edges_of G = G .loops() iff G .allTrees() = { (createGraph v) where v is Vertex of G : verum } )

proof end;

definition

let G be _Graph;

func SubtreeRel G -> Relation of (G .allTrees()) equals :: GLENUM00:def 13
(SubgraphRel G) |_2 (G .allTrees());

coherence
(SubgraphRel G) |_2 (G .allTrees()) is Relation of (G .allTrees()) ;

end;

:: deftheorem defines SubtreeRel GLENUM00:def 13 :
for G being _Graph holds SubtreeRel G = (SubgraphRel G) |_2 (G .allTrees());

theorem Th159: :: GLENUM00:159

for G being _Graph
for H1, H2 being Tree-like plain Subgraph of G holds
( [H1,H2] in SubtreeRel G iff H1 is Subgraph of H2 )

proof end;

theorem Th160: :: GLENUM00:160

for G being _Graph holds field (SubtreeRel G) = G .allTrees()

proof end;

theorem Th161: :: GLENUM00:161

for G being _Graph holds SubtreeRel G partially_orders G .allTrees()

proof end;

registration

let G be _Graph;

cluster SubtreeRel G -> reflexive antisymmetric transitive being_partial-order ;

coherence
( SubtreeRel G is reflexive & SubtreeRel G is antisymmetric & SubtreeRel G is transitive & SubtreeRel G is being_partial-order )

proof end;

end;

theorem Th162: :: GLENUM00:162

for G being _Graph
for H being Subgraph of G holds SubtreeRel H = (SubtreeRel G) |_2 (H .allTrees())

proof end;

theorem Th163: :: GLENUM00:163

for G being loopless _Graph holds
( G is edgeless iff SubtreeRel G = id (G .allTrees()) )

proof end;

theorem Th164: :: GLENUM00:164

for G being _Graph
for H being removeLoops of G holds SubtreeRel G = SubtreeRel H

proof end;

theorem :: GLENUM00:165

for G being _Graph holds
( the_Edges_of G = G .loops() iff SubtreeRel G = id (G .allTrees()) )

proof end;

theorem Th166: :: GLENUM00:166

for G being _Graph holds G .allTrees() has_upper_Zorn_property_wrt SubtreeRel G

proof end;

registration

let G be connected _Graph;

cluster Relation-like K97() -defined Function-like finite [Graph-like] spanning Tree-like plain non 0 -vertex for Subgraph of G;

existence
ex b₁ being Subgraph of G st
( b₁ is plain & b₁ is spanning & b₁ is Tree-like )

proof end;

end;

theorem Th167: :: GLENUM00:167

for G being connected _Graph
for e being object st e in (the_Edges_of G) \ (G .loops()) holds
ex T being spanning Tree-like plain Subgraph of G st e in the_Edges_of T

proof end;

definition

let G be _Graph;

func G .allSpanningTrees() -> Subset of (G .allSG()) equals :: GLENUM00:def 14
{ H where H is Element of [#] (G .allSG()) : ( H is spanning & H is Tree-like ) } ;

coherence
{ H where H is Element of [#] (G .allSG()) : ( H is spanning & H is Tree-like ) } is Subset of (G .allSG())

proof end;

end;

:: deftheorem defines .allSpanningTrees() GLENUM00:def 14 :
for G being _Graph holds G .allSpanningTrees() = { H where H is Element of [#] (G .allSG()) : ( H is spanning & H is Tree-like ) } ;

theorem Th168: :: GLENUM00:168

for G1, G2 being _Graph holds
( G2 in G1 .allSpanningTrees() iff ( G2 is spanning acyclic plain Subgraph of G1 & G2 is connected ) )

proof end;

theorem Th169: :: GLENUM00:169

for G being _Graph holds G .allSpanningTrees() = (G .allSpanningSG()) /\ (G .allTrees())

proof end;

theorem Th170: :: GLENUM00:170

for G being _Graph holds G .allSpanningTrees() = (G .allConnectedSG()) /\ (G .allSpanningForests())

proof end;

theorem :: GLENUM00:171

for G being _Graph
for H being spanning acyclic Subgraph of G st H is connected holds
H | _GraphSelectors in G .allSpanningTrees()

proof end;

theorem Th172: :: GLENUM00:172

for G being _Graph holds
( G is Tree-like iff G | _GraphSelectors in G .allSpanningTrees() )

proof end;

theorem Th173: :: GLENUM00:173

for G being _Graph holds
( G is connected iff G .allSpanningTrees() <> {} )

proof end;

registration

let G be non connected _Graph;

cluster G .allSpanningTrees() -> empty ;

coherence
G .allSpanningTrees() is empty by Th173;

end;

registration

let G be connected _Graph;

cluster G .allSpanningTrees() -> non empty simple Tree-like ;

coherence
( not G .allSpanningTrees() is empty & G .allSpanningTrees() is Tree-like & G .allSpanningTrees() is simple )

proof end;

end;

theorem Th174: :: GLENUM00:174

for G being connected _Graph
for H being spanning connected Subgraph of G holds H .allSpanningTrees() c= G .allSpanningTrees()

proof end;

theorem Th175: :: GLENUM00:175

for G1 being _Graph
for G2 being loopless connected _Graph st G2 .allSpanningTrees() c= G1 .allSpanningTrees() holds
G2 is spanning Subgraph of G1

proof end;

theorem Th176: :: GLENUM00:176

for G being _Graph
for H being removeLoops of G holds G .allSpanningTrees() = H .allSpanningTrees()

proof end;

theorem Th177: :: GLENUM00:177

for G1, G2 being loopless connected _Graph holds
( G1 == G2 iff G1 .allSpanningTrees() = G2 .allSpanningTrees() )

proof end;

theorem :: GLENUM00:178

for G1, G2 being connected _Graph
for G3 being removeLoops of G1
for G4 being removeLoops of G2 holds
( G3 == G4 iff G1 .allSpanningTrees() = G2 .allSpanningTrees() )

proof end;

theorem Th179: :: GLENUM00:179

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding & rng (F _V) = the_Vertices_of G2 holds
rng ((SG2SGFunc F) | (G1 .allSpanningTrees())) c= G2 .allSpanningTrees()

proof end;

theorem Th180: :: GLENUM00:180

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding & F is onto holds
G2 .allSpanningTrees() = rng ((SG2SGFunc F) | (G1 .allSpanningTrees()))

proof end;

theorem Th181: :: GLENUM00:181

for G1, G2 being _Graph st G2 is G1 -Disomorphic holds
G1 .allSpanningTrees() ,G2 .allSpanningTrees() are_Disomorphic

proof end;

theorem Th182: :: GLENUM00:182

for G1, G2 being _Graph st G2 is G1 -isomorphic holds
G1 .allSpanningTrees() ,G2 .allSpanningTrees() are_isomorphic

proof end;

theorem :: GLENUM00:183

for G1, G2 being _Graph
for G3 being removeLoops of G1
for G4 being removeLoops of G2 st G4 is G3 -Disomorphic holds
G1 .allSpanningTrees() ,G2 .allSpanningTrees() are_Disomorphic

proof end;

theorem :: GLENUM00:184

for G1, G2 being _Graph
for G3 being removeLoops of G1
for G4 being removeLoops of G2 st G4 is G3 -isomorphic holds
G1 .allSpanningTrees() ,G2 .allSpanningTrees() are_isomorphic

proof end;

theorem Th185: :: GLENUM00:185

for G being connected _Graph
for H being removeLoops of G holds H is GraphUnion of G .allSpanningTrees()

proof end;

theorem :: GLENUM00:186

for G being loopless connected _Graph holds G is GraphUnion of G .allSpanningTrees()

proof end;

theorem :: GLENUM00:187

for G being _Graph holds
( G is Tree-like iff G .allSpanningTrees() = {(G | _GraphSelectors)} )

proof end;

theorem :: GLENUM00:188

for G being _Graph holds
( G is connected iff the_Vertices_of (G .allSpanningTrees()) = {(the_Vertices_of G)} )

proof end;

definition

let G be _Graph;

func G .allComponents() -> Subset of (G .allSG()) equals :: GLENUM00:def 15
{ H where H is Element of [#] (G .allSG()) : H is Component-like } ;

coherence
{ H where H is Element of [#] (G .allSG()) : H is Component-like } is Subset of (G .allSG())

proof end;

end;

:: deftheorem defines .allComponents() GLENUM00:def 15 :
for G being _Graph holds G .allComponents() = { H where H is Element of [#] (G .allSG()) : H is Component-like } ;

theorem Th189: :: GLENUM00:189

for G1, G2 being _Graph holds
( G2 in G1 .allComponents() iff G2 is plain Component of G1 )

proof end;

theorem :: GLENUM00:190

for G being _Graph holds G .allComponents() c= (G .allInducedSG()) /\ (G .allConnectedSG())

proof end;

theorem Th191: :: GLENUM00:191

for G being _Graph
for H being Component of G holds H | _GraphSelectors in G .allComponents()

proof end;

theorem Th192: :: GLENUM00:192

for G being _Graph holds
( G is connected iff G | _GraphSelectors in G .allComponents() )

proof end;

Lm3: for G being _Graph holds the_Vertices_of (G .allComponents()) = G .componentSet()

proof end;

registration

let G be _Graph;

cluster G .allComponents() -> non empty plain connected \/-tolerating vertex-disjoint edge-disjoint ;

coherence
( not G .allComponents() is empty & G .allComponents() is vertex-disjoint & G .allComponents() is edge-disjoint & G .allComponents() is \/-tolerating & G .allComponents() is plain & G .allComponents() is connected )

proof end;

end;

theorem Th193: :: GLENUM00:193

for G1, G2 being _Graph st G2 .allComponents() c= G1 .allComponents() holds
G2 is Subgraph of G1

proof end;

theorem :: GLENUM00:194

for G1, G2 being _Graph holds
( G1 == G2 iff G1 .allComponents() = G2 .allComponents() )

proof end;

theorem Th195: :: GLENUM00:195

for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2 st F is isomorphism holds
G2 .allComponents() = rng ((SG2SGFunc F) | (G1 .allComponents()))

proof end;

theorem :: GLENUM00:196

for G1, G2 being _Graph st G2 is G1 -Disomorphic holds
G1 .allComponents() ,G2 .allComponents() are_Disomorphic

proof end;

theorem :: GLENUM00:197

for G1, G2 being _Graph st G2 is G1 -isomorphic holds
G1 .allComponents() ,G2 .allComponents() are_isomorphic

proof end;

theorem Th198: :: GLENUM00:198

for G being _Graph holds G is GraphUnion of G .allComponents()

proof end;

theorem Th199: :: GLENUM00:199

for G being _Graph holds
( ( G is loopless implies G .allComponents() is loopless ) & ( G .allComponents() is loopless implies G is loopless ) & ( G is non-multi implies G .allComponents() is non-multi ) & ( G .allComponents() is non-multi implies G is non-multi ) & ( G is non-Dmulti implies G .allComponents() is non-Dmulti ) & ( G .allComponents() is non-Dmulti implies G is non-Dmulti ) & ( G is simple implies G .allComponents() is simple ) & ( G .allComponents() is simple implies G is simple ) & ( G is Dsimple implies G .allComponents() is Dsimple ) & ( G .allComponents() is Dsimple implies G is Dsimple ) & ( G is acyclic implies G .allComponents() is acyclic ) & ( G .allComponents() is acyclic implies G is acyclic ) & ( G is edgeless implies G .allComponents() is edgeless ) & ( G .allComponents() is edgeless implies G is edgeless ) & ( G is chordal implies G .allComponents() is chordal ) & ( G .allComponents() is chordal implies G is chordal ) & ( G is loopfull implies G .allComponents() is loopfull ) & ( G .allComponents() is loopfull implies G is loopfull ) )

proof end;

registration

let G be loopless _Graph;

cluster G .allComponents() -> loopless ;

coherence
G .allComponents() is loopless ;

end;

registration

let G be non-multi _Graph;

cluster G .allComponents() -> non-multi ;

coherence
G .allComponents() is non-multi ;

end;

registration

let G be non-Dmulti _Graph;

cluster G .allComponents() -> non-Dmulti ;

coherence
G .allComponents() is non-Dmulti ;

end;

registration

let G be simple _Graph;

cluster G .allComponents() -> simple ;

coherence
G .allComponents() is simple ;

end;

registration

let G be Dsimple _Graph;

cluster G .allComponents() -> Dsimple ;

coherence
G .allComponents() is Dsimple ;

end;

registration

let G be acyclic _Graph;

cluster G .allComponents() -> acyclic ;

coherence
G .allComponents() is acyclic ;

end;

registration

let G be edgeless _Graph;

cluster G .allComponents() -> edgeless ;

coherence
G .allComponents() is edgeless ;

end;

registration

let G be chordal _Graph;

cluster G .allComponents() -> chordal ;

coherence
G .allComponents() is chordal by Th199;

end;

registration

let G be loopfull _Graph;

cluster G .allComponents() -> loopfull ;

coherence
G .allComponents() is loopfull by Th199;

end;

theorem :: GLENUM00:200

for G being _Graph holds
( G is connected iff G .allComponents() = {(G | _GraphSelectors)} )

proof end;

theorem :: GLENUM00:201

for G being _Graph holds the_Vertices_of (G .allComponents()) = G .componentSet() by Lm3;

theorem :: GLENUM00:202

for G being _Graph holds G .numComponents() = card (G .allComponents())

proof end;