:: Refined Finiteness and Degree properties in Graphs
:: by Sebastian Koch
::
:: Received May 19, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies SUBSET_1, RELAT_1, FUNCT_1, XXREAL_0, TARSKI, ARYTM_3, CARD_1,
XBOOLE_0, NAT_1, ARYTM_1, GLIB_000, PARTFUN1, FINSET_1, ZFMISC_1,
FUNCOP_1, FUNCT_2, GLIB_009, MOD_4, WAYBEL_0, GLIB_006, GLIB_007,
FUNCT_4, CARD_2, SCMYCIEL, SGRAPH1, GLIB_010, SIMPLEX0, XCMPLX_0,
MATRIX11, BSPACE, GLIB_013, SQUARE_1, SETFAM_1, RELAT_2, STRUCT_0,
ORDINAL1, GLIB_012, YELLOW_1, WELLORD2, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
ORDINAL1, RELSET_1, PARTFUN1, WELLORD2, FUNCT_2, DOMAIN_1, FUNCOP_1,
FUNCT_4, FINSET_1, CARD_1, XCMPLX_0, XXREAL_0, SQUARE_1, CARD_2, NEWTON,
GLIB_000, STRUCT_0, ORDERS_2, SGRAPH1, MATRIX11, YELLOW_1, ORDERS_5,
BSPACE, GLIB_006, GLIB_007, GLIB_008, GLIB_009, GLIB_010, GLIB_012;
constructors DOMAIN_1, FUNCT_4, CARD_2, GLIB_002, GLIB_007, BSPACE, MATRIX11,
GLIB_008, GLIB_009, GLIB_010, SQUARE_1, NEWTON, YELLOW_1, ORDERS_5,
GLIB_012;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XREAL_0, NAT_1,
GLIB_000, CARD_1, XTUPLE_0, GLIB_008, GLIB_010, SQUARE_1, CARD_2,
RAMSEY_1, MSAFREE5, SGRAPH1, CARD_5, GLIBPRE0, YELLOW_1, ORDINAL7;
requirements ARITHM, BOOLE, NUMERALS, SUBSET;
begin :: Upper Size of Graphs without parallel Edges
theorem :: GLIB_013:1
for G being non-Dmulti _Graph ex f being one-to-one Function
st dom f = the_Edges_of G &
rng f c= [: the_Vertices_of G, the_Vertices_of G :] &
for e being object st e in dom f holds
f.e = [(the_Source_of G).e,(the_Target_of G).e];
theorem :: GLIB_013:2
for G being non-Dmulti _Graph holds G.size() c= G.order() *` G.order();
theorem :: GLIB_013:3
for G being Dsimple _Graph ex f being one-to-one Function
st dom f = the_Edges_of G &
rng f c= [: the_Vertices_of G, the_Vertices_of G :]\id the_Vertices_of G &
for e being object st e in dom f holds
f.e = [(the_Source_of G).e,(the_Target_of G).e];
theorem :: GLIB_013:4
for G being non-multi _Graph ex f being one-to-one Function
st dom f = the_Edges_of G &
rng f c= 2Set the_Vertices_of G \/ singletons the_Vertices_of G &
for e being object st e in dom f holds
f.e = {(the_Source_of G).e,(the_Target_of G).e};
theorem :: GLIB_013:5
for G being simple _Graph ex f being one-to-one Function
st dom f = the_Edges_of G & rng f c= 2Set the_Vertices_of G &
for e being object st e in dom f holds
f.e = {(the_Source_of G).e,(the_Target_of G).e};
begin :: vertex- and edge-finite graph
definition
let G be _Graph;
attr G is vertex-finite means
:: GLIB_013:def 1
the_Vertices_of G is finite;
attr G is edge-finite means
:: GLIB_013:def 2
the_Edges_of G is finite;
end;
theorem :: GLIB_013:6
for G being _Graph holds G is vertex-finite iff G.order() is finite;
theorem :: GLIB_013:7
for G being _Graph holds G is edge-finite iff G.size() is finite;
theorem :: GLIB_013:8
for G1, G2 being _Graph st G1 == G2 holds
(G1 is vertex-finite implies G2 is vertex-finite) &
(G1 is edge-finite implies G2 is edge-finite);
registration
let V be non empty finite set, E be set;
let S, T be Function of E, V;
cluster createGraph(V,E,S,T) -> vertex-finite;
end;
registration
let V be infinite set, E be set;
let S, T be Function of E, V;
cluster createGraph(V,E,S,T) -> non vertex-finite;
end;
registration
let V be non empty set, E be finite set;
let S, T be Function of E, V;
cluster createGraph(V,E,S,T) -> edge-finite;
end;
registration
let V be non empty set, E be infinite set;
let S, T be Function of E, V;
cluster createGraph(V,E,S,T) -> non edge-finite;
end;
registration
cluster _finite -> vertex-finite edge-finite for _Graph;
cluster vertex-finite edge-finite -> _finite for _Graph;
cluster edgeless -> edge-finite for _Graph;
cluster _trivial -> vertex-finite for _Graph;
cluster vertex-finite non-Dmulti -> edge-finite for _Graph;
cluster non vertex-finite loopfull -> non edge-finite for _Graph;
::cluster non vertex-finite without_isolated_vertices -> non edge-finite
::for _Graph;
::coherence; :: f(v) = the Element of v.edgesInOut has infinite range
::cluster edge-finite without_isolated_vertices ->
::vertex-finite for _Graph;
::coherence;
cluster vertex-finite edge-finite simple for _Graph;
cluster vertex-finite non edge-finite for _Graph;
cluster non vertex-finite edge-finite for _Graph;
cluster non vertex-finite non edge-finite for _Graph;
end;
registration
let G be vertex-finite _Graph;
cluster G.order() -> non zero natural;
end;
definition
let G be vertex-finite _Graph;
redefine func G.order() -> non zero Nat;
end;
registration
let G be edge-finite _Graph;
cluster G.size() -> natural;
end;
definition
let G be edge-finite _Graph;
redefine func G.size() -> Nat;
end;
theorem :: GLIB_013:9
for G being vertex-finite non-Dmulti _Graph
holds G.size() <= G.order()^2;
theorem :: GLIB_013:10
for G being vertex-finite Dsimple _Graph
holds G.size() <= G.order()^2 - G.order();
theorem :: GLIB_013:11
for G being vertex-finite non-multi _Graph
holds G.size() <= (G.order()^2 + G.order())/2;
theorem :: GLIB_013:12
for G being vertex-finite simple _Graph
holds G.size() <= (G.order()^2 - G.order())/2;
registration
let G be vertex-finite _Graph;
cluster the_Vertices_of G -> finite;
cluster -> vertex-finite for Subgraph of G;
cluster -> vertex-finite edge-finite for DLGraphComplement of G;
cluster -> vertex-finite edge-finite for LGraphComplement of G;
cluster -> vertex-finite edge-finite for DGraphComplement of G;
cluster -> vertex-finite edge-finite for GraphComplement of G;
let V be finite set;
cluster -> vertex-finite for addVertices of G, V;
end;
registration
let G be vertex-finite _Graph, v be object;
cluster -> vertex-finite for addVertex of G, v;
let e,w be object;
cluster -> vertex-finite for addEdge of G,v,e,w;
cluster -> vertex-finite for addAdjVertex of G,v,e,w;
end;
registration
let G be vertex-finite _Graph, E be set;
cluster -> vertex-finite for reverseEdgeDirections of G, E;
end;
registration
let G be vertex-finite _Graph, v be object, V be set;
cluster -> vertex-finite for addAdjVertexAll of G,v,V;
end;
registration
let G be vertex-finite _Graph, V be set;
cluster -> vertex-finite for addLoops of G, V;
end;
registration
let G be _Graph;
let V be infinite set;
cluster -> non vertex-finite for addVertices of G, V;
end;
registration
let G be non vertex-finite _Graph;
cluster the_Vertices_of G -> infinite;
cluster -> non vertex-finite for Supergraph of G;
cluster spanning -> non vertex-finite for Subgraph of G;
cluster -> non vertex-finite for DLGraphComplement of G;
cluster -> non vertex-finite for LGraphComplement of G;
cluster -> non vertex-finite for DGraphComplement of G;
cluster -> non vertex-finite for GraphComplement of G;
let V be infinite set, E be set;
cluster -> non vertex-finite for inducedSubgraph of G, V, E;
end;
registration
let G be non vertex-finite _Graph, V be infinite Subset of the_Vertices_of G;
cluster -> non edge-finite for addLoops of G, V;
end;
registration
let G be edge-finite _Graph;
cluster the_Edges_of G -> finite;
cluster -> edge-finite for Subgraph of G;
let V be set;
cluster -> edge-finite for addVertices of G, V;
end;
registration
let G be edge-finite _Graph, E be set;
cluster -> edge-finite for reverseEdgeDirections of G, E;
end;
registration
let G be edge-finite _Graph, v be object;
cluster -> edge-finite for addVertex of G, v;
let e,w be object;
cluster -> edge-finite for addEdge of G,v,e,w;
cluster -> edge-finite for addAdjVertex of G,v,e,w;
end;
registration
let G be edge-finite _Graph, v be object, V be finite set;
cluster -> edge-finite for addAdjVertexAll of G, v, V;
end;
registration
let G be edge-finite _Graph, V be finite Subset of the_Vertices_of G;
cluster -> edge-finite for addLoops of G, V;
end;
registration
let G be non vertex-finite edge-finite _Graph;
cluster isolated for Vertex of G;
end;
registration
let G be non vertex-finite edge-finite _Graph;
cluster -> non edge-finite for DLGraphComplement of G;
cluster -> non edge-finite for LGraphComplement of G;
cluster -> non edge-finite for DGraphComplement of G;
cluster -> non edge-finite for GraphComplement of G;
end;
registration
let G be non edge-finite _Graph;
cluster the_Edges_of G -> infinite;
cluster -> non edge-finite for Supergraph of G;
let V be set, E be infinite Subset of the_Edges_of G;
cluster -> non edge-finite for inducedSubgraph of G, V, E;
end;
registration
let G be non edge-finite _Graph, E be finite set;
cluster -> non edge-finite for removeEdges of G, E;
end;
registration
let G be non edge-finite _Graph, e be set;
cluster -> non edge-finite for removeEdge of G, e;
end;
theorem :: GLIB_013:13
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is weak_SG-embedding holds
(G2 is vertex-finite implies G1 is vertex-finite) &
(G2 is edge-finite implies G1 is edge-finite);
theorem :: GLIB_013:14
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is onto holds
(G1 is vertex-finite implies G2 is vertex-finite) &
(G1 is edge-finite implies G2 is edge-finite);
theorem :: GLIB_013:15
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is isomorphism holds
(G1 is vertex-finite iff G2 is vertex-finite) &
(G1 is edge-finite iff G2 is edge-finite);
begin :: Order and Size of a Graph as attributes
definition
let c be Cardinal, G be _Graph;
attr G is c-vertex means
:: GLIB_013:def 3
G.order() = c;
attr G is c-edge means
:: GLIB_013:def 4
G.size() = c;
end;
theorem :: GLIB_013:16
for G being _Graph
holds G is vertex-finite iff ex n being non zero Nat st G is n-vertex;
theorem :: GLIB_013:17
for G being _Graph
holds G is edge-finite iff ex n being Nat st G is n-edge;
theorem :: GLIB_013:18
for G1, G2 being _Graph, c being Cardinal
st the_Vertices_of G1 = the_Vertices_of G2
holds G1 is c-vertex implies G2 is c-vertex;
theorem :: GLIB_013:19
for G1, G2 being _Graph, c being Cardinal
st the_Edges_of G1 = the_Edges_of G2
holds G1 is c-edge implies G2 is c-edge;
theorem :: GLIB_013:20
for G1, G2 being _Graph, c being Cardinal st G1 == G2 holds
(G1 is c-vertex implies G2 is c-vertex) &
(G1 is c-edge implies G2 is c-edge);
theorem :: GLIB_013:21
for G being _Graph holds G is G.order()-vertex G.size()-edge;
registration
let V be non empty set, E be set;
let S, T be Function of E, V;
cluster createGraph(V,E,S,T) -> (card V)-vertex (card E)-edge;
end;
registration
let a be non zero Cardinal, b be Cardinal;
cluster a-vertex b-edge for _Graph;
end;
registration
let c be Cardinal;
cluster _trivial c-edge for _Graph;
end;
registration
cluster -> non 0-vertex for _Graph;
cluster _trivial -> 1-vertex for _Graph;
cluster 1-vertex -> _trivial for _Graph;
let n be non zero Nat;
cluster n-vertex -> vertex-finite for _Graph;
end;
registration
let c be non zero Cardinal, G be c-vertex _Graph;
cluster spanning -> c-vertex for Subgraph of G;
cluster -> c-vertex for DLGraphComplement of G;
cluster -> c-vertex for LGraphComplement of G;
cluster -> c-vertex for DGraphComplement of G;
cluster -> c-vertex for GraphComplement of G;
let E be set;
cluster -> c-vertex for reverseEdgeDirections of G, E;
end;
registration
let c be non zero Cardinal, G be c-vertex _Graph, V be set;
cluster -> c-vertex for addLoops of G, V;
end;
registration
let c be non zero Cardinal, G be c-vertex _Graph, v,e,w be object;
cluster -> c-vertex for addEdge of G,v,e,w;
end;
registration
cluster edgeless -> 0-edge for _Graph;
cluster 0-edge -> edgeless for _Graph;
let n be Nat;
cluster n-edge -> edge-finite for _Graph;
end;
registration
let c be Cardinal, G be c-edge _Graph, E be set;
cluster -> c-edge for reverseEdgeDirections of G, E;
end;
registration
let c be Cardinal, G be c-edge _Graph, V be set;
cluster -> c-edge for addVertices of G, V;
end;
theorem :: GLIB_013:22
for G1, G2 being _Graph, F being PGraphMapping of G1, G2, c being Cardinal
st F is isomorphism holds
(G1 is c-vertex iff G2 is c-vertex) &
(G1 is c-edge iff G2 is c-edge);
begin :: Locally finite Graphs
definition
let G be _Graph;
attr G is locally-finite means
:: GLIB_013:def 5 :: or finite-branching
for v being Vertex of G holds v.edgesInOut() is finite;
end;
theorem :: GLIB_013:23
for G being _Graph holds G is locally-finite
iff for v being Vertex of G holds v.degree() is finite;
theorem :: GLIB_013:24
for G1, G2 being _Graph st G1 == G2
holds G1 is locally-finite implies G2 is locally-finite;
theorem :: GLIB_013:25
for G being _Graph holds G is locally-finite iff
for v being Vertex of G
holds v.edgesIn() is finite & v.edgesOut() is finite;
theorem :: GLIB_013:26
for G being _Graph holds G is locally-finite iff
for v being Vertex of G
holds v.inDegree() is finite & v.outDegree() is finite;
theorem :: GLIB_013:27
for V being non empty set, E being set, S,T being Function of E,V
st for v being Element of V holds S"{v} is finite & T"{v} is finite
holds createGraph(V,E,S,T) is locally-finite;
theorem :: GLIB_013:28
for V being non empty set, E being set, S,T being Function of E,V
st ex v being Element of V st S"{v} is infinite or T"{v} is infinite
holds createGraph(V,E,S,T) is non locally-finite;
:: easy creation of non locally-finite graph
registration
let G be non vertex-finite _Graph;
let V be infinite Subset of the_Vertices_of G;
cluster -> non locally-finite for addAdjVertexAll of G,the_Vertices_of G,V;
end;
registration
cluster edge-finite -> locally-finite for _Graph;
cluster locally-finite for _Graph;
cluster non locally-finite for _Graph;
end;
registration
let G be locally-finite _Graph;
cluster -> locally-finite for Subgraph of G;
let X be finite set;
cluster G.edgesInto(X) -> finite;
cluster G.edgesOutOf(X) -> finite;
cluster G.edgesInOut(X) -> finite;
cluster G.edgesBetween(X) -> finite;
let Y be finite set;
cluster G.edgesBetween(X,Y) -> finite;
cluster G.edgesDBetween(X,Y) -> finite;
end;
registration
let G be locally-finite _Graph, v be Vertex of G;
cluster v.edgesIn() -> finite;
cluster v.edgesOut() -> finite;
cluster v.edgesInOut() -> finite;
cluster v.inDegree() -> finite;
cluster v.outDegree() -> finite;
cluster v.degree() -> finite;
end;
definition
let G be locally-finite _Graph, v be Vertex of G;
redefine func v.inDegree() -> Nat;
redefine func v.outDegree() -> Nat;
redefine func v.degree() -> Nat;
end;
registration
let G be locally-finite _Graph, V be set;
cluster -> locally-finite for addVertices of G, V;
cluster -> locally-finite for addLoops of G, V;
end;
registration
let G be locally-finite _Graph, E be set;
cluster -> locally-finite for reverseEdgeDirections of G, E;
end;
registration
let G be locally-finite _Graph;
let v,e,w be object;
cluster -> locally-finite for addEdge of G, v, e, w;
cluster -> locally-finite for addAdjVertex of G, v, e, w;
end;
theorem :: GLIB_013:29
for G2 being _Graph, v being object, V being Subset of the_Vertices_of G2
for G1 being addAdjVertexAll of G2, v, V st not v in the_Vertices_of G2
holds (G2 is locally-finite & V is finite) iff G1 is locally-finite;
registration
let G be locally-finite _Graph;
let v be object, V be finite set;
cluster -> locally-finite for addAdjVertexAll of G, v, V;
end;
registration
let G be non locally-finite _Graph;
cluster -> non locally-finite for Supergraph of G;
let E be finite set;
cluster -> non locally-finite for removeEdges of G, E;
end;
registration
let G be non locally-finite _Graph, e be set;
cluster -> non locally-finite for removeEdge of G, e;
end;
theorem :: GLIB_013:30
for G1 being non locally-finite _Graph
for V being finite Subset of the_Vertices_of G1
for G2 being removeVertices of G1, V
st for v being Vertex of G1 st v in V holds v.edgesInOut() is finite
holds G2 is non locally-finite;
theorem :: GLIB_013:31
for G1 being non locally-finite _Graph, v being Vertex of G1
for G2 being removeVertex of G1, v st v.edgesInOut() is finite
holds G2 is non locally-finite;
theorem :: GLIB_013:32
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is weak_SG-embedding & G2 is locally-finite holds G1 is locally-finite;
theorem :: GLIB_013:33
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is onto semi-Dcontinuous & G1 is locally-finite
holds G2 is locally-finite;
theorem :: GLIB_013:34
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is isomorphism holds G1 is locally-finite iff G2 is locally-finite;
begin :: Degree properties in Graphs
definition
let G be _Graph;
func G.supDegree() -> Cardinal equals
:: GLIB_013:def 6
union the set of all v.degree() where v is Vertex of G;
func G.supInDegree() -> Cardinal equals
:: GLIB_013:def 7
union the set of all v.inDegree() where v is Vertex of G;
func G.supOutDegree() -> Cardinal equals
:: GLIB_013:def 8
union the set of all v.outDegree() where v is Vertex of G;
func G.minDegree() -> Cardinal equals
:: GLIB_013:def 9
meet the set of all v.degree() where v is Vertex of G;
func G.minInDegree() -> Cardinal equals
:: GLIB_013:def 10
meet the set of all v.inDegree() where v is Vertex of G;
func G.minOutDegree() -> Cardinal equals
:: GLIB_013:def 11
meet the set of all v.outDegree() where v is Vertex of G;
end;
theorem :: GLIB_013:35
for G being _Graph, v being Vertex of G holds
G.minDegree() c= v.degree() & v.degree() c= G.supDegree() &
G.minInDegree() c= v.inDegree() & v.inDegree() c= G.supInDegree() &
G.minOutDegree() c= v.outDegree() & v.outDegree() c= G.supOutDegree();
theorem :: GLIB_013:36
for G being _Graph, c being Cardinal holds G.minDegree() = c iff
ex v being Vertex of G st v.degree() = c &
for w being Vertex of G holds v.degree() c= w.degree();
theorem :: GLIB_013:37
for G being _Graph, c being Cardinal holds G.minInDegree() = c iff
ex v being Vertex of G st v.inDegree() = c &
for w being Vertex of G holds v.inDegree() c= w.inDegree();
theorem :: GLIB_013:38
for G being _Graph, c being Cardinal holds G.minOutDegree() = c iff
ex v being Vertex of G st v.outDegree() = c &
for w being Vertex of G holds v.outDegree() c= w.outDegree();
theorem :: GLIB_013:39
for G being _Graph holds G.supInDegree() c= G.supDegree();
theorem :: GLIB_013:40
for G being _Graph holds G.supOutDegree() c= G.supDegree();
theorem :: GLIB_013:41
for G being _Graph holds G.minInDegree() c= G.minDegree();
theorem :: GLIB_013:42
for G being _Graph holds G.minOutDegree() c= G.minDegree();
theorem :: GLIB_013:43
for G being _Graph holds G.minDegree() c= G.supDegree();
theorem :: GLIB_013:44
for G being _Graph holds G.minInDegree() c= G.supInDegree();
theorem :: GLIB_013:45
for G being _Graph holds G.minOutDegree() c= G.supOutDegree();
theorem :: GLIB_013:46
for G being _Graph st ex v being Vertex of G st v is isolated
holds G.minDegree() = 0 & G.minInDegree() = 0 & G.minOutDegree() = 0;
theorem :: GLIB_013:47
for G being _Graph st G.minDegree() = 0
ex v being Vertex of G st v is isolated;
::theorem
::for G being with_isolated_vertices _Graph
::holds G.minDegree() = 0 & G.minInDegree() = 0 & G.minOutDegree() = 0;
::theorem
::for G being without_isolated_vertices _Graph holds G.minDegree() <> 0;
theorem :: GLIB_013:48
for G being _Graph, c being Cardinal
st ex v being Vertex of G st v.degree() = c &
for w being Vertex of G holds w.degree() c= v.degree()
holds G.supDegree() = c;
theorem :: GLIB_013:49
for G being _Graph, c being Cardinal
st ex v being Vertex of G st v.inDegree() = c &
for w being Vertex of G holds w.inDegree() c= v.inDegree()
holds G.supInDegree() = c;
theorem :: GLIB_013:50
for G being _Graph, c being Cardinal
st ex v being Vertex of G st v.outDegree() = c &
for w being Vertex of G holds w.outDegree() c= v.outDegree()
holds G.supOutDegree() = c;
theorem :: GLIB_013:51
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is weak_SG-embedding holds G1.supDegree() c= G2.supDegree();
theorem :: GLIB_013:52
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is weak_SG-embedding & rng F_V = the_Vertices_of G2 holds
G1.minDegree() c= G2.minDegree();
theorem :: GLIB_013:53
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is onto semi-Dcontinuous holds G2.supDegree() c= G1.supDegree();
theorem :: GLIB_013:54
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is onto semi-Dcontinuous & dom F_V = the_Vertices_of G1
holds G2.minDegree() c= G1.minDegree();
theorem :: GLIB_013:55
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is isomorphism
holds G1.supDegree() = G2.supDegree() & G1.minDegree() = G2.minDegree();
theorem :: GLIB_013:56
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is directed weak_SG-embedding holds
G1.supInDegree() c= G2.supInDegree() &
G1.supOutDegree() c= G2.supOutDegree();
theorem :: GLIB_013:57
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is directed weak_SG-embedding & rng F_V = the_Vertices_of G2 holds
G1.minInDegree() c= G2.minInDegree() &
G1.minOutDegree() c= G2.minOutDegree();
theorem :: GLIB_013:58
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is onto semi-Dcontinuous holds
G2.supInDegree() c= G1.supInDegree() &
G2.supOutDegree() c= G1.supOutDegree();
theorem :: GLIB_013:59
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is onto semi-Dcontinuous & dom F_V = the_Vertices_of G1 holds
G2.minInDegree() c= G1.minInDegree() &
G2.minOutDegree() c= G1.minOutDegree();
theorem :: GLIB_013:60
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is Disomorphism holds
G1.supInDegree() = G2.supInDegree() &
G1.supOutDegree() = G2.supOutDegree() &
G1.minInDegree() = G2.minInDegree() &
G1.minOutDegree() = G2.minOutDegree();
theorem :: GLIB_013:61
for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
holds G1.supDegree() = G2.supDegree() & G1.minDegree() = G2.minDegree();
theorem :: GLIB_013:62
for G1, G2 being _Graph st G1 == G2 holds
G1.supDegree() = G2.supDegree() &
G1.minDegree() = G2.minDegree() &
G1.supInDegree() = G2.supInDegree() &
G1.minInDegree() = G2.minInDegree() &
G1.supOutDegree() = G2.supOutDegree() &
G1.minOutDegree() = G2.minOutDegree();
theorem :: GLIB_013:63
for G1 being _Graph, G2 being Subgraph of G1 holds
G2.supDegree() c= G1.supDegree() &
G2.supInDegree() c= G1.supInDegree() &
G2.supOutDegree() c= G1.supOutDegree();
theorem :: GLIB_013:64
for G1 being _Graph, G2 being spanning Subgraph of G1 holds
G2.minDegree() c= G1.minDegree() &
G2.minInDegree() c= G1.minInDegree() &
G2.minOutDegree() c= G1.minOutDegree();
theorem :: GLIB_013:65
for G2 being _Graph, V being set, G1 being addVertices of G2, V
holds
G1.supDegree() = G2.supDegree() &
G1.supInDegree() = G2.supInDegree() &
G1.supOutDegree() = G2.supOutDegree();
theorem :: GLIB_013:66
for G2 being _Graph, V being set, G1 being addVertices of G2, V
st V \ the_Vertices_of G2 <> {}
holds G1.minDegree() = 0 & G1.minInDegree() = 0 & G1.minOutDegree() = 0;
registration
let G be non edgeless _Graph;
cluster G.supDegree() -> non empty;
cluster G.supInDegree() -> non empty;
cluster G.supOutDegree() -> non empty;
end;
:: better version
:: non trivial connected or loopfull <=> without_isolated_vertices
:: registration
:: let G be non trivial connected _Graph;
:: cluster G.minDegree() -> non empty;
:: coherence;
:: cluster G.minInDegree() -> non empty;
:: coherence;
:: cluster G.minOutDegree() -> non empty;
:: coherence;
:: end;
::
:: registration
:: let G be loopfull _Graph;
:: cluster G.minDegree() -> non empty;
:: coherence;
:: cluster G.minInDegree() -> non empty;
:: coherence;
:: cluster G.minOutDegree() -> non empty;
:: coherence;
:: end;
registration
let G be locally-finite _Graph;
cluster G.minDegree() -> natural;
cluster G.minInDegree() -> natural;
cluster G.minOutDegree() -> natural;
end;
definition
let G be locally-finite _Graph;
redefine func G.minDegree() -> Nat;
redefine func G.minInDegree() -> Nat;
redefine func G.minOutDegree() -> Nat;
end;
theorem :: GLIB_013:67
for G being locally-finite _Graph, n being Nat
holds G.minDegree() = n iff
ex v being Vertex of G st v.degree() = n &
for w being Vertex of G holds v.degree() <= w.degree();
theorem :: GLIB_013:68
for G being locally-finite _Graph, n being Nat
holds G.minInDegree() = n iff
ex v being Vertex of G st v.inDegree() = n &
for w being Vertex of G holds v.inDegree() <= w.inDegree();
theorem :: GLIB_013:69
for G being locally-finite _Graph, n being Nat
holds G.minOutDegree() = n iff
ex v being Vertex of G st v.outDegree() = n &
for w being Vertex of G holds v.outDegree() <= w.outDegree();
theorem :: GLIB_013:70
for G2 being _Graph, v,w being Vertex of G2, e being object
for G1 being addEdge of G2,v,e,w st v <> w holds
G1.minDegree() = G2.minDegree() or
G1.minDegree() = (v.degree() /\ w.degree()) +` 1;
theorem :: GLIB_013:71
for G2 being _Graph, v,w being Vertex of G2, e being object
for G1 being addEdge of G2,v,e,w st v <> w holds
G1.minInDegree() = G2.minInDegree() or
G1.minInDegree() = w.inDegree() +` 1;
theorem :: GLIB_013:72
for G2 being _Graph, v,w being Vertex of G2, e being object
for G1 being addEdge of G2,v,e,w st v <> w holds
G1.minOutDegree() = G2.minOutDegree() or
G1.minOutDegree() = v.outDegree() +` 1;
theorem :: GLIB_013:73
for G2 being locally-finite _Graph, v,w being Vertex of G2,e being object
for G1 being addEdge of G2,v,e,w st v <> w holds
G1.minDegree() = G2.minDegree() or
G1.minDegree() = min(v.degree(),w.degree()) + 1;
theorem :: GLIB_013:74
for G2 being locally-finite _Graph, v,w being Vertex of G2,e being object
for G1 being addEdge of G2,v,e,w st v <> w holds
G1.minInDegree() = G2.minInDegree() or
G1.minInDegree() = w.inDegree() + 1;
theorem :: GLIB_013:75
for G2 being locally-finite _Graph, v,w being Vertex of G2,e being object
for G1 being addEdge of G2,v,e,w st v <> w holds
G1.minOutDegree() = G2.minOutDegree() or
G1.minOutDegree() = v.outDegree() + 1;
:: :: better in combination with_isolated_vertices
:: theorem
:: for G2 being _Graph, v being Vertex of G2, e,w being object
:: for G1 being addAdjVertex of G2,v,e,w
:: st not e in the_Edges_of G2 & not w in the_Vertices_of G2
:: holds G1.minDegree() = {1} /\ G2.minDegree();
::
:: theorem
:: for G2 being _Graph, v,e being object, w being Vertex of G2
:: for G1 being addAdjVertex of G2,v,e,w
:: st not e in the_Edges_of G2 & not v in the_Vertices_of G2
:: holds G1.minDegree() = {1} /\ G2.minDegree();
::
:: theorem
:: for G2 being locally-finite _Graph, v being Vertex of G2,e,w being object
:: for G1 being addAdjVertex of G2,v,e,w
:: st not e in the_Edges_of G2 & not w in the_Vertices_of G2
:: holds G1.minDegree() = min(1,G2.minDegree());
::
:: theorem
:: for G2 being locally-finite _Graph, v,e being object,w being Vertex of G2
:: for G1 being addAdjVertex of G2,v,e,w
:: st not e in the_Edges_of G2 & not v in the_Vertices_of G2
:: holds G1.minDegree() = min(1,G2.minDegree());
theorem :: GLIB_013:76
for G2 being _Graph, v being object
for G1 being addAdjVertexAll of G2,v st not v in the_Vertices_of G2
holds G1.minDegree() = (G2.minDegree() +` 1) /\ G2.order();
theorem :: GLIB_013:77
for G2 being _finite _Graph, v being object
for G1 being addAdjVertexAll of G2,v st not v in the_Vertices_of G2
holds G1.minDegree() = min(G2.minDegree() + 1, G2.order());
theorem :: GLIB_013:78
for G2 being _Graph, V being set, G1 being addLoops of G2, V
holds G1.minDegree() c= G2.minDegree() +` 2;
registration
let G be edge-finite _Graph;
cluster G.supDegree() -> natural;
cluster G.supInDegree() -> natural;
cluster G.supOutDegree() -> natural;
end;
definition
let G be edge-finite _Graph;
redefine func G.supDegree() -> Nat;
redefine func G.supInDegree() -> Nat;
redefine func G.supOutDegree() -> Nat;
end;
definition
let G be _Graph;
attr G is with_max_degree means
:: GLIB_013:def 12
ex v being Vertex of G
st for w being Vertex of G holds w.degree() c= v.degree();
attr G is with_max_in_degree means
:: GLIB_013:def 13
ex v being Vertex of G
st for w being Vertex of G holds w.inDegree() c= v.inDegree();
attr G is with_max_out_degree means
:: GLIB_013:def 14
ex v being Vertex of G
st for w being Vertex of G holds w.outDegree() c= v.outDegree();
end;
theorem :: GLIB_013:79
for G being _Graph st G is with_max_degree
holds ex v being Vertex of G st v.degree() = G.supDegree() &
for w being Vertex of G holds w.degree() c= v.degree();
theorem :: GLIB_013:80
for G being _Graph st G is with_max_in_degree
holds ex v being Vertex of G st v.inDegree() = G.supInDegree() &
for w being Vertex of G holds w.inDegree() c= v.inDegree();
theorem :: GLIB_013:81
for G being _Graph st G is with_max_out_degree
holds ex v being Vertex of G st v.outDegree() = G.supOutDegree() &
for w being Vertex of G holds w.outDegree() c= v.outDegree();
notation
let G be _Graph;
antonym G is without_max_degree for G is with_max_degree;
antonym G is without_max_in_degree for G is with_max_in_degree;
antonym G is without_max_out_degree for G is with_max_out_degree;
end;
registration
cluster with_max_in_degree with_max_out_degree -> with_max_degree
for _Graph;
cluster vertex-finite -> with_max_degree with_max_in_degree
with_max_out_degree for _Graph;
cluster edge-finite -> with_max_degree with_max_in_degree
with_max_out_degree for _Graph;
:: will be clustered after construction of graphs by relations is formalized
::cluster without_max_degree without_max_in_degree
:: without_max_out_degree for _Graph;
::existence;
end;
theorem :: GLIB_013:82
for G being with_max_degree _Graph
holds G is with_max_in_degree or G is with_max_out_degree;
notation
let G be with_max_degree _Graph;
synonym G.maxDegree() for G.supDegree();
end;
notation
let G be with_max_in_degree _Graph;
synonym G.maxInDegree() for G.supInDegree();
end;
notation
let G be with_max_out_degree _Graph;
synonym G.maxOutDegree() for G.supOutDegree();
end;
registration
let G be locally-finite with_max_degree _Graph;
cluster G.maxDegree() -> natural;
end;
definition
let G be locally-finite with_max_degree _Graph;
redefine func G.maxDegree() -> Nat;
end;
registration
let G be locally-finite with_max_in_degree _Graph;
cluster G.maxInDegree() -> natural;
end;
definition
let G be locally-finite with_max_in_degree _Graph;
redefine func G.maxInDegree() -> Nat;
end;
registration
let G be locally-finite with_max_out_degree _Graph;
cluster G.maxOutDegree() -> natural;
end;
definition
let G be locally-finite with_max_out_degree _Graph;
redefine func G.maxOutDegree() -> Nat;
end;
theorem :: GLIB_013:83
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is isomorphism holds G1 is with_max_degree iff G2 is with_max_degree;
theorem :: GLIB_013:84
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is Disomorphism holds
(G1 is with_max_in_degree iff G2 is with_max_in_degree) &
(G1 is with_max_out_degree iff G2 is with_max_out_degree);
theorem :: GLIB_013:85
for G1, G2 being _Graph st G1 == G2 holds
(G1 is with_max_degree implies G2 is with_max_degree) &
(G1 is with_max_in_degree implies G2 is with_max_in_degree) &
(G1 is with_max_out_degree implies G2 is with_max_out_degree);
theorem :: GLIB_013:86
for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
holds G1 is with_max_degree iff G2 is with_max_degree;
registration
let G be with_max_degree _Graph, E be set;
cluster -> with_max_degree for reverseEdgeDirections of G, E;
end;
registration
let G be with_max_degree _Graph, V be set;
cluster -> with_max_degree for addVertices of G, V;
cluster -> with_max_degree for addLoops of G, V;
end;
registration
let G be with_max_degree _Graph, v,e,w be object;
cluster -> with_max_degree for addEdge of G,v,e,w;
cluster -> with_max_degree for addAdjVertex of G,v,e,w;
end;
registration
let G be with_max_degree _Graph, v be object, V be set;
cluster -> with_max_degree for addAdjVertexAll of G,v,V;
end;
registration
let G be with_max_in_degree _Graph;
cluster -> with_max_out_degree for reverseEdgeDirections of G;
end;
registration
let G be with_max_in_degree _Graph, V be set;
cluster -> with_max_in_degree for addVertices of G, V;
cluster -> with_max_in_degree for addLoops of G, V;
end;
registration
let G be with_max_in_degree _Graph, v,e,w be object;
cluster -> with_max_in_degree for addEdge of G,v,e,w;
cluster -> with_max_in_degree for addAdjVertex of G,v,e,w;
end;
registration
let G be with_max_in_degree _Graph, v be object, V be set;
cluster -> with_max_in_degree for addAdjVertexAll of G,v,V;
end;
registration
let G be with_max_out_degree _Graph;
cluster -> with_max_in_degree for reverseEdgeDirections of G ;
end;
registration
let G be with_max_out_degree _Graph, V be set;
cluster -> with_max_out_degree for addVertices of G, V;
cluster -> with_max_out_degree for addLoops of G, V;
end;
registration
let G be with_max_out_degree _Graph, v,e,w be object;
cluster -> with_max_out_degree for addEdge of G,v,e,w;
cluster -> with_max_out_degree for addAdjVertex of G,v,e,w;
end;
registration
let G be with_max_out_degree _Graph, v be object, V be set;
cluster -> with_max_out_degree for addAdjVertexAll of G,v,V;
end;
:: registration
:: let G be without_max_degree _Graph, E be set;
:: cluster -> without_max_degree for reverseEdgeDirections of G, E;
:: coherence;
:: end;
::
:: registration
:: let G be without_max_degree _Graph, V be set;
:: cluster -> without_max_degree for addVertices of G, V;
:: coherence;
:: cluster -> without_max_degree for addLoops of G, V;
:: coherence;
:: end;
::
:: registration
:: let G be without_max_degree _Graph, v,e,w be object;
:: cluster -> without_max_degree for addEdge of G,v,e,w;
:: coherence;
:: cluster -> without_max_degree for addAdjVertex of G,v,e,w;
:: coherence;
:: end;
::
:: registration
:: let G be without_max_degree _Graph, v be object, V be set;
:: cluster -> without_max_degree for addAdjVertexAll of G,v,V;
:: coherence;
:: end;
::
:: registration
:: let G be without_max_in_degree _Graph, E be set;
:: cluster -> without_max_in_degree for reverseEdgeDirections of G, E;
:: coherence;
:: end;
::
:: registration
:: let G be without_max_in_degree _Graph, V be set;
:: cluster -> without_max_in_degree for addVertices of G, V;
:: coherence;
:: cluster -> without_max_in_degree for addLoops of G, V;
:: coherence;
:: end;
::
:: registration
:: let G be without_max_in_degree _Graph, v,e,w be object;
:: cluster -> without_max_in_degree for addEdge of G,v,e,w;
:: coherence;
:: cluster -> without_max_in_degree for addAdjVertex of G,v,e,w;
:: coherence;
:: end;
::
:: registration
:: let G be without_max_in_degree _Graph, v be object, V be set;
:: cluster -> without_max_in_degree for addAdjVertexAll of G,v,V;
:: coherence;
:: end;
::
:: registration
:: let G be without_max_out_degree _Graph, E be set;
:: cluster -> without_max_out_degree for reverseEdgeDirections of G, E;
:: coherence;
:: end;
::
:: registration
:: let G be without_max_out_degree _Graph, V be set;
:: cluster -> without_max_out_degree for addVertices of G, V;
:: coherence;
:: cluster -> without_max_out_degree for addLoops of G, V;
:: coherence;
:: end;
::
:: registration
:: let G be without_max_out_degree _Graph, v,e,w be object;
:: cluster -> without_max_out_degree for addEdge of G,v,e,w;
:: coherence;
:: cluster -> without_max_out_degree for addAdjVertex of G,v,e,w;
:: coherence;
:: end;
::
:: registration
:: let G be without_max_out_degree _Graph, v be object, V be set;
:: cluster -> without_max_out_degree for addAdjVertexAll of G,v,V;
:: coherence;
:: end;
theorem :: GLIB_013:87
for G being locally-finite with_max_degree _Graph, n being Nat
holds G.maxDegree() = n iff
ex v being Vertex of G st v.degree() = n &
for w being Vertex of G holds w.degree() <= v.degree();
theorem :: GLIB_013:88
for G being locally-finite with_max_in_degree _Graph, n being Nat
holds G.maxInDegree() = n iff
ex v being Vertex of G st v.inDegree() = n &
for w being Vertex of G holds w.inDegree() <= v.inDegree();
theorem :: GLIB_013:89
for G being locally-finite with_max_out_degree _Graph, n being Nat
holds G.maxOutDegree() = n iff
ex v being Vertex of G st v.outDegree() = n &
for w being Vertex of G holds w.outDegree() <= v.outDegree();
theorem :: GLIB_013:90
for c being Cardinal, G being _trivial c-edge _Graph holds
G.maxInDegree() = c & G.minInDegree() = c &
G.maxOutDegree() = c & G.minOutDegree() = c &
G.maxDegree() = c +` c & G.minDegree() = c +` c;
definition
let G be _Graph, v be Vertex of G;
attr v is with_min_degree means
:: GLIB_013:def 15
v.degree() = G.minDegree();
attr v is with_min_in_degree means
:: GLIB_013:def 16
v.inDegree() = G.minInDegree();
attr v is with_min_out_degree means
:: GLIB_013:def 17
v.outDegree() = G.minOutDegree();
attr v is with_max_degree means
:: GLIB_013:def 18
v.degree() = G.supDegree();
attr v is with_max_in_degree means
:: GLIB_013:def 19
v.inDegree() = G.supInDegree();
attr v is with_max_out_degree means
:: GLIB_013:def 20
v.outDegree() = G.supOutDegree();
end;
theorem :: GLIB_013:91
for G being _Graph, v,w being Vertex of G st v is with_min_degree
holds v.degree() c= w.degree();
theorem :: GLIB_013:92
for G being _Graph, v,w being Vertex of G st v is with_min_in_degree
holds v.inDegree() c= w.inDegree();
theorem :: GLIB_013:93
for G being _Graph, v,w being Vertex of G st v is with_min_out_degree
holds v.outDegree() c= w.outDegree();
theorem :: GLIB_013:94
for G being _Graph, v,w being Vertex of G st w is with_max_degree
holds v.degree() c= w.degree();
theorem :: GLIB_013:95
for G being _Graph, v,w being Vertex of G st w is with_max_in_degree
holds v.inDegree() c= w.inDegree();
theorem :: GLIB_013:96
for G being _Graph, v,w being Vertex of G st w is with_max_out_degree
holds v.outDegree() c= w.outDegree();
registration
let G be _Graph;
cluster with_min_degree for Vertex of G;
cluster with_min_in_degree for Vertex of G;
cluster with_min_out_degree for Vertex of G;
cluster with_min_in_degree with_min_out_degree -> with_min_degree
for Vertex of G;
cluster with_max_in_degree with_max_out_degree -> with_max_degree
for Vertex of G;
cluster isolated -> with_min_degree with_min_in_degree
with_min_out_degree for Vertex of G;
end;
theorem :: GLIB_013:97
for G being _Graph holds G is with_max_degree iff
ex v being Vertex of G st v is with_max_degree;
theorem :: GLIB_013:98
for G being _Graph holds G is with_max_in_degree iff
ex v being Vertex of G st v is with_max_in_degree;
theorem :: GLIB_013:99
for G being _Graph holds G is with_max_out_degree iff
ex v being Vertex of G st v is with_max_out_degree;
registration
let G be with_max_degree _Graph;
cluster with_max_degree for Vertex of G;
end;
registration
let G be with_max_in_degree _Graph;
cluster with_max_in_degree for Vertex of G;
end;
registration
let G be with_max_out_degree _Graph;
cluster with_max_out_degree for Vertex of G;
end;
:: registration
:: let G be without_max_out_degree _Graph;
:: cluster -> non with_max_out_degree for Vertex of G;
:: coherence by Th125;
:: end;
::
:: registration
:: let G be without_max_degree _Graph;
:: cluster -> non with_max_degree for Vertex of G;
:: coherence by Th126;
:: end;
::
:: registration
:: let G be without_max_in_degree _Graph;
:: cluster -> non with_max_in_degree for Vertex of G;
:: coherence by Th127;
:: end;