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