P. 259 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

uhgriedg0edg0 25801

A hypergraph has no edges iff its edge function is empty. (Contributed by AV, 21-Oct-2020.) (Proof shortened by AV, 15-Dec-2020.)

⊢ (𝐺 ∈ UHGraph → ((Edg‘𝐺) = ∅ ↔ (iEdg‘𝐺) = ∅))

Theorem

uhgredgn0 25802

An edge of a hypergraph is a nonempty subset of vertices. (Contributed by AV, 28-Nov-2020.)

⊢ ((𝐺 ∈ UHGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → 𝐸 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}))

Theorem

edguhgr 25803

An edge of a hypergraph is a subset of vertices. (Contributed by AV, 26-Oct-2020.) (Proof shortened by AV, 28-Nov-2020.)

⊢ ((𝐺 ∈ UHGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → 𝐸 ∈ 𝒫 (Vtx‘𝐺))

Theorem

uhgredgrnv 25804

An edge of a hypergraph contains only vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 4-Jun-2021.)

⊢ ((𝐺 ∈ UHGraph ∧ 𝐸 ∈ (Edg‘𝐺) ∧ 𝑁 ∈ 𝐸) → 𝑁 ∈ (Vtx‘𝐺))

Theorem

uhgredgss 25805

The set of edges of a hypergraph is a subset of the powerset of vertices without the empty set. (Contributed by AV, 29-Nov-2020.)

⊢ (𝐺 ∈ UHGraph → (Edg‘𝐺) ⊆ (𝒫 (Vtx‘𝐺) ∖ {∅}))

Theorem

upgredgss 25806*

The set of edges of a pseudograph is a subset of the set of unordered pairs of vertices. (Contributed by AV, 29-Nov-2020.)

⊢ (𝐺 ∈ UPGraph → (Edg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣ (#‘𝑥) ≤ 2})

Theorem

umgredgss 25807*

The set of edges of a multigraph is a subset of the set of unordered pairs of vertices. (Contributed by AV, 25-Nov-2020.)

⊢ (𝐺 ∈ UMGraph → (Edg‘𝐺) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2})

Theorem

edgupgr 25808

Properties of an edge of a pseudograph. (Contributed by AV, 8-Nov-2020.)

⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → (𝐸 ∈ 𝒫 (Vtx‘𝐺) ∧ 𝐸 ≠ ∅ ∧ (#‘𝐸) ≤ 2))

Theorem

edgumgr 25809

Properties of an edge of a multigraph. (Contributed by AV, 25-Nov-2020.)

⊢ ((𝐺 ∈ UMGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → (𝐸 ∈ 𝒫 (Vtx‘𝐺) ∧ (#‘𝐸) = 2))

Theorem

uhgrvtxedgiedgb 25810*

In a hypergraph, a vertex is incident with an edge iff it is contained in an element of the range of the edge function. (Contributed by AV, 24-Dec-2020.)

⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉) → (∃𝑖 ∈ dom 𝐼 𝑈 ∈ (𝐼‘𝑖) ↔ ∃𝑒 ∈ 𝐸 𝑈 ∈ 𝑒))

Theorem

upgredg 25811*

For each edge in a pseudograph, there are two vertices which are connected by this edge. (Contributed by AV, 4-Nov-2020.)

⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝐶 = {𝑎, 𝑏})

Theorem

umgredg 25812*

For each edge in a multigraph, there are two distinct vertices which are connected by this edge. (Contributed by Alexander van der Vekens, 9-Dec-2017.) (Revised by AV, 25-Nov-2020.)

⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝐶 ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝐶 = {𝑎, 𝑏}))

Theorem

umgrpredgav 25813

An edge of a multigraph always connects two vertices. Analogue of umgredgprv 25773. This theorem does not hold for arbitrary pseudographs: if either 𝑀 or 𝑁 is a proper class, then {𝑀, 𝑁} ∈ 𝐸 could still hold ({𝑀, 𝑁} would be either {𝑀} or {𝑁}, see prprc1 4243 or prprc2 4244, i.e. a loop), but 𝑀 ∈ 𝑉 or 𝑁 ∈ 𝑉 would not be true. (Contributed by AV, 27-Nov-2020.)

⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ {𝑀, 𝑁} ∈ 𝐸) → (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉))

Theorem

upgredg2vtx 25814*

For a vertex incident to an edge there is another vertex incident to the edge in a pseudograph. (Contributed by AV, 18-Oct-2020.) (Revised by AV, 5-Dec-2020.)

⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ∧ 𝐴 ∈ 𝐶) → ∃𝑏 ∈ 𝑉 𝐶 = {𝐴, 𝑏})

Theorem

upgredgpr 25815

If a proper pair (of vertices) is a subset of an edge in a pseudograph, the pair is the edge. (Contributed by AV, 30-Dec-2020.)

⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐺 ∈ UPGraph ∧ 𝐶 ∈ 𝐸 ∧ {𝐴, 𝐵} ⊆ 𝐶) ∧ (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵)) → {𝐴, 𝐵} = 𝐶)

Theorem

umgredgne 25816

An edge of a multigraph always connects two different vertices. Analog of umgrnloopv 25772 resp. umgrnloop 25774. (Contributed by AV, 27-Nov-2020.)

⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ {𝑀, 𝑁} ∈ 𝐸) → 𝑀 ≠ 𝑁)

Theorem

umgrnloop2 25817

A multigraph has no loops. (Contributed by AV, 27-Oct-2020.) (Revised by AV, 30-Nov-2020.)

⊢ (𝐺 ∈ UMGraph → {𝑁, 𝑁} ∉ (Edg‘𝐺))

Theorem

umgredgnlp 25818*

An edge of a multigraph is not a loop. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 8-Jun-2021.)

⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ 𝐶 ∈ 𝐸) → ¬ ∃𝑣 𝐶 = {𝑣})

PART 17  GRAPH THEORY (DEPRECATED)

To give an overview of the definitions and terms used in the context of graph theory, a glossary is provided in the following, mainly according to definitions in [Bollobas] p. 1-8 or in [Diestel] p. 2-28. Although this glossary concentrates on undirected graphs, many of the concepts are also useful for directed graphs.

Basic kinds of graphs:

Term	Reference	Definition	Remarks
Undirected hypergraph	df-uhgra 25821	an ordered pair ⟨𝑉, 𝐸⟩ of a set 𝑉 and a function 𝐸 into the powerset of 𝑉 (ran 𝐸 ⊆ (𝒫 𝑉)). An element of 𝑉 is called "vertex", an element of ran 𝐸 is called "edge", the function 𝐸 is called the "edge-function" .	In this most general definition of a graph, an "edge" may connect three or more vertices with each other, see [Berge] p. 1. In Wikipedia "Hypergraph", see https://en.wikipedia.org/wiki/Hypergraph (18-Jan-2020) such a hypergraph is called "non-simple hypergraph", "multiple hypergraph" or "multi-hypergraphs". According to Wikipedia "Incidence structure", see https://en.wikipedia.org/wiki/Incidence_structure (18-Jan-2020) "Each hypergraph [...] can be regarded as an incidence structure in which the [vertices] play the role of "points", the corresponding family of [edges] plays the role of "lines" and the incidence relation is set membership". If a graph is represented by a class variable, e.g. 𝐺, the edges of this graph are often represented by the function value (Edges‘𝐺). If the graph is given as pair ⟨𝑉, 𝐸⟩, however, (Edges‘⟨𝑉, 𝐸⟩) or preferably (𝑉Edges𝐸) is only used to talk about edges more explicitly. Otherwise, ran 𝐸 is used, because this is much shorter. Notice that by using (Edges‘𝐺) the (possibly more than one) edges connecting the same vertices could not be distinguished anymore. Therefore, this representation will only be used for undirected simple graphs. For the set of vertices, a function "Vertices" could have been defined analogously. But "( Vertices ` G )" would have been exactly the same as (1st ‘𝐺), so the latter is used to denote the set of vertices if the graph is represented by a class variable.
Undirected simple hypergraph	df-ushgra 25822	an ordered pair ⟨𝑉, 𝐸⟩ of a set 𝑉 and a one-to-one function 𝐸 into the powerset of 𝑉 (ran 𝐸 ⊆ (𝒫 𝑉)).	See also Wikipedia "Hypergraph", https://en.wikipedia.org/wiki/Hypergraph (18-Jan-2020). This is how a "hypergraph" is defined in Section I.1 in [Bollobas] p. 7 or the definition in section 1.10 in [Diestel] p. 27. A simple hypergraph has at most one edge between the same vertices, hence a multigraph needs not to be a simple hypergraph. According to [Berge] p. 1, "A simple hypergraph (or "Sperner family") is a hypergraph H = { E1, E2, ..., Em } such that Ei C_ Ej => i = j". By this definition, a simple hypergraph cannot contain the edges E1 = { v1 , v2 } and E2 = { v1, v2, v3 }, because E1 C_ E2, but 1 =/= 2.
Undirected multigraph	df-umgra 25842	a graph ⟨𝑉, 𝐸⟩ such that 𝐸 is a function into the set of (proper or not proper) unordered pairs of 𝑉.	A proper unordered pair contains two different elements, a not proper unordered pair contains two times the same element, so it is a singleton (see preqsn 4331). According to the definition in Section I.1 in [Bollobas] p. 7, "In a multigraph both multiple edges [joining two vertices] and multiple loops [joining a vertex to itself] are allowed", or according to [Diestel] p. 28, "A multigraph is a pair (V,E) of disjoint sets (of vertices and edges) together with a map E -> V u. [V]^2 assigning to every edge either one or two vertices, its end.".
Undirected simple graph with loops	df-uslgra 25861	a graph ⟨𝑉, 𝐸⟩ such that 𝐸 is a one-to-one function into the set of (proper or not proper) unordered pairs of 𝑉.	This means that there is at most one edge between two vertices, and at most one loop from a vertex to itself.
Undirected simple graph without loops (in short "simple graph")	df-usgra 25862	a graph ⟨𝑉, 𝐸⟩ such that 𝐸 is a one-to-one function into the set of (proper) unordered pairs of 𝑉.	An ordered pair ⟨𝑉, 𝐸⟩ of two distinct sets 𝑉 and 𝐸 (the "usual" definition of a "graph", see, for example, the definition in section I.1 of [Bollobas] p. 1 or in section 1.1 of [Diestel] p. 2) can be identified with an undirected simple graph without loops by "indexing" the edges with themselves, see ausisusgra 25884.
Finite graph	---	a graph ⟨𝑉, 𝐸⟩ with finite sets 𝑉 and 𝐸.	See definitions in [Bollobas] p. 1 or [Diestel] p. 2. In simple graphs, 𝐸 is finite if 𝑉 is finite, see usgrafis 25944. The number of edges is limited by (𝑛C2) (or "𝑛 choose 2") with 𝑛 = (#‘𝑉), see usgramaxsize 26015. Analogously, the number of edges of an undirected simple graph with loops is limited by ((𝑛 + 1)C2). In multigraphs, however, 𝐸 can be infinite although 𝑉 is finite.
Graph of finite size	---	a graph ⟨𝑉, 𝐸⟩ with finite set 𝐸, i.e. with a finite number of edges.	A graph can be of finite size although 𝑉 is infinite.

Terms and properties of graphs:

Term	Reference	Definition	Remarks
Edge joining (two) vertices	---	An edge 𝑒 ∈ ran 𝐸 "joins" the vertices v1, v2, ... vn (𝑛 ∈ ℕ) if 𝑒 = { v1, v2, ... vn }.	If 𝑛 = 1, 𝑒 = { v1 } is a "loop", if 𝑛 = 2, 𝑒 = { v1 , v2 } is an edge as it is usually defined, see definition in Section I.1 in [Bollobas] p. 1.
(Two) Endvertices of an edge	see definition in Section I.1 in [Bollobas] p. 1.	If an edge 𝑒 ∈ ran 𝐸 joins the vertices v1, v2, ... vn (𝑛 ∈ ℕ), then the vertices v1, v2, ... vn are called the "endvertices" of the edge 𝑒.
(Two) Adjacent vertices	see definition in Section I.1 in [Bollobas] p. 1/2.	The vertices v1, v2, ... vn (𝑛 ∈ ℕ) are "adjacent" if there is an edge e = { v1, v2, ... vn } joining these vertices. In this case, the vertices are "incident" with the edge e (see definition in Section I.1 in [Bollobas] p. 2) or "connected" by the edge e.
Edge ending at a vertex		An edge 𝑒 ∈ ran 𝐸 is "ending" at a vertex 𝑣 if the vertex is an endvertex of the edge: 𝑣 ∈ 𝑒. In other words, the vertex 𝑣 is incident with the edge 𝑒.
(Two) Adjacent edges		The edges e0, e1, ... en (𝑛 ∈ ℕ) are "adjacent" if they have exactly one common endvertex.	Generalization of definition in Section I.1 in [Bollobas] p. 2.
Order of a graph	see definition in Section I.1 in [Bollobas] p. 3	the "order" of a graph ⟨𝑉, 𝐸⟩ is the number of vertices in the graph ((#‘𝑉)).
Size of a graph	see definition in Section I.1 in [Bollobas] p. 3	the "size" of a graph ⟨𝑉, 𝐸⟩ is the number of edges in the graph ((#‘𝐸)). Or, for simple graphs 𝐺: (#‘(Edges‘𝐺))).
Neighborhood of a vertex	df-nbgra 25949 resp. definition in Section I.1 in [Bollobas] p. 3	A vertex connected with a vertex 𝑣 by an edge is called a "neighbor" of the vertex 𝑣. The set of neighbors of a vertex 𝑣 is called the "neighborhood" (or "open neighborhood") of the vertex 𝑣. The "closed neighborhood" is the union of the (open) neighborhood of the vertex 𝑣 with {𝑣}.
Degree of a vertex	df-vdgr 26421	The "degree" of a vertex is the number of the edges ending at this vertex.	In a simple graph, the degree of a vertex is the number of neighbors of this vertex, see definition in Section I.1 in [Bollobas] p. 3
Isolated vertex	usgravd0nedg 26445	A vertex is called "isolated" if it is not an endvertex of any edge, thus having degree 0.
Universal vertex	df-uvtx 25951	A vertex is called "universal" if it is connected with every other vertex of the graph by an edge, thus having degree (#‘𝑉).

Special kinds of graphs:

Term	Reference	Definition	Remarks
Complete graph	df-cusgra 25950	A graph is called "complete" if each pair of vertices is connected by an edge.	The size of a complete undirected simple graph of order 𝑛 is (𝑛C2) (or "𝑛 choose 2"), see cusgrasize 26006.
Empty graph	umgra0 25854 and usgra0 25899	A graph is called "empty" if it has no edges.
Null graph	usgra0v 25900	A graph is called the "null graph" if it has no vertices (and therefore also no edges).
Trivial graph	usgra1v 25919	A graph is called the "trivial graph" if it has only one vertex and no edges.
Connected graph	df-conngra 26198 resp. definition in Section I.1 in [Bollobas] p. 6	A graph is called "connected" if for each pair of vertices there is a path between these vertices.

For the terms "Path", "Walk", "Trail", "Circuit", "Cycle" see the remarks below and the definitions in Section I.1 in [Bollobas] p. 4-5.

17.1  Undirected graphs - basics

17.1.1  Undirected hypergraphs

Syntax

cuhg 25819

Extend class notation with undirected hypergraphs.

class UHGrph

Syntax

cushg 25820

Extend class notation with undirected simple hypergraphs.

class USHGrph

Definition

df-uhgra 25821*

Define the class of all undirected hypergraphs. An undirected hypergraph is a pair of a set and a function into the powerset of this set (the empty set excluded). (Contributed by Alexander van der Vekens, 26-Dec-2017.)

⊢ UHGrph = {⟨𝑣, 𝑒⟩ ∣ 𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅})}

Definition

df-ushgra 25822*

Define the class of all undirected simple hypergraphs. An undirected simple hypergraph is a pair of a set and an injective (one-to-one) function into the powerset of this set (the empty set excluded). (Contributed by AV, 19-Jan-2020.)

⊢ USHGrph = {⟨𝑣, 𝑒⟩ ∣ 𝑒:dom 𝑒–1-1→(𝒫 𝑣 ∖ {∅})}

Theorem

reluhgra 25823

The class of all undirected hypergraphs is a relation. (Contributed by Alexander van der Vekens, 26-Dec-2017.)

⊢ Rel UHGrph

Theorem

relushgra 25824

The class of all undirected simple hypergraphs is a relation. (Contributed by AV, 19-Jan-2020.)

⊢ Rel USHGrph

Theorem

uhgrav 25825

The classes of vertices and edges of an undirected hypergraph are sets. (Contributed by Alexander van der Vekens, 26-Dec-2017.)

⊢ (𝑉 UHGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V))

Theorem

uhgraopelvv 25826

An undirected hypergraph is a member in the universal class of ordered pairs. (Contributed by AV, 3-Jan-2020.)

⊢ (𝐺 ∈ UHGrph → 𝐺 ∈ (V × V))

Theorem

isuhgra 25827

The property of being an undirected hypergraph. (Contributed by Alexander van der Vekens, 26-Dec-2017.)

⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉 UHGrph 𝐸 ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})))

Theorem

uhgraf 25828

The edge function of an undirected hypergraph is a function into the power set of the set of vertices. (Contributed by Alexander van der Vekens, 26-Dec-2017.)

⊢ (𝑉 UHGrph 𝐸 → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))

Theorem

uhgrafun 25829

The edge function of an undirected hypergraph is a function. (Contributed by Alexander van der Vekens, 26-Dec-2017.)

⊢ (𝑉 UHGrph 𝐸 → Fun 𝐸)

Theorem

isushgra 25830

The property of being an undirected simple hypergraph. (Contributed by AV, 3-Jan-2020.)

⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉 USHGrph 𝐸 ↔ 𝐸:dom 𝐸–1-1→(𝒫 𝑉 ∖ {∅})))

Theorem

ushgraf 25831

The edge function of an undirected simple hypergraph is a function into the power set of the set of vertices. (Contributed by AV, 19-Jan-2020.)

⊢ (𝑉 USHGrph 𝐸 → 𝐸:dom 𝐸–1-1→(𝒫 𝑉 ∖ {∅}))

Theorem

ushgrauhgra 25832

An undirected simple hypergraph is an undirected hypergraph. (Contributed by AV, 19-Jan-2020.)

⊢ (𝑉 USHGrph 𝐸 → 𝑉 UHGrph 𝐸)

Theorem

uhgraop 25833

The property of being an undirected hypergraph represented as an ordered pair. The representation as an ordered pair is the usual representation of a graph, see section I.1 of [Bollobas] p. 1. (Contributed by AV, 1-Jan-2020.)

⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (⟨𝑉, 𝐸⟩ ∈ UHGrph ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})))

Theorem

uhgrac 25834

The property of being an undirected hypergraph represented by a class. This representation is useful if the set of vertices and the edge function is/needs not to be known. (Contributed by AV, 1-Jan-2020.)

⊢ (𝐺 ∈ UHGrph → (2^nd ‘𝐺):dom (2^nd ‘𝐺)⟶(𝒫 (1^st ‘𝐺) ∖ {∅}))

Theorem

uhgrass 25835

An edge is a subset of vertices, analogous to umgrass 25848. (Contributed by Alexander van der Vekens, 26-Dec-2017.)

⊢ ((𝑉 UHGrph 𝐸 ∧ 𝐹 ∈ dom 𝐸) → (𝐸‘𝐹) ⊆ 𝑉)

Theorem

uhgraeq12d 25836

Equality of hypergraphs. (Contributed by Alexander van der Vekens, 26-Dec-2017.)

⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → (𝑉 UHGrph 𝐸 ↔ 𝑊 UHGrph 𝐹))

Theorem

uhgrares 25837

A subgraph of a hypergraph (formed by removing some edges from the original graph) is a hypergraph, analogous to umgrares 25853. (Contributed by Alexander van der Vekens, 27-Dec-2017.)

⊢ (𝑉 UHGrph 𝐸 → 𝑉 UHGrph (𝐸 ↾ 𝐴))

Theorem

uhgra0 25838

The empty graph, with vertices but no edges, is a hypergraph, analogous to umgra0 25854. (Contributed by Alexander van der Vekens, 27-Dec-2017.)

⊢ (𝑉 ∈ 𝑊 → 𝑉 UHGrph ∅)

Theorem

uhgra0v 25839

The null graph, with no vertices, is a hypergraph if and only if the edge function is empty. (Contributed by Alexander van der Vekens, 27-Dec-2017.)

⊢ (∅ UHGrph 𝐸 ↔ 𝐸 = ∅)

Theorem

uhgraun 25840

The union of two (undirected) hypergraphs (with the same vertex set): If ⟨𝑉, 𝐸⟩ and ⟨𝑉, 𝐹⟩ are hypergraphs, then ⟨𝑉, 𝐸 ∪ 𝐹⟩ is a hypergraph (the vertex set stays the same, but the edges from both graphs are kept, possibly resulting in two edges between two vertices), analogous to umgraun 25857. (Contributed by Alexander van der Vekens, 27-Dec-2017.)

⊢ (𝜑 → 𝐸 Fn 𝐴)    &   ⊢ (𝜑 → 𝐹 Fn 𝐵)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝑉 UHGrph 𝐸)    &   ⊢ (𝜑 → 𝑉 UHGrph 𝐹)    ⇒   ⊢ (𝜑 → 𝑉 UHGrph (𝐸 ∪ 𝐹))

17.1.2  Undirected multigraphs

Syntax

cumg 25841

Extend class notation with undirected multigraphs.

class UMGrph

Definition

df-umgra 25842*

Define the class of all undirected multigraphs. A multigraph is a pair ⟨𝑉, 𝐸⟩ where 𝐸 is a function into subsets of 𝑉 of cardinality one or two, representing the two vertices incident to the edge, or the one vertex if the edge is a loop. (Contributed by Mario Carneiro, 11-Mar-2015.)

⊢ UMGrph = {⟨𝑣, 𝑒⟩ ∣ 𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}}

Theorem

relumgra 25843

The class of all undirected multigraphs is a relation. (Contributed by Mario Carneiro, 11-Mar-2015.)

⊢ Rel UMGrph

Theorem

isumgra 25844*

The property of being an undirected multigraph. (Contributed by Mario Carneiro, 11-Mar-2015.)

⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉 UMGrph 𝐸 ↔ 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}))

Theorem

wrdumgra 25845*

The property of being an undirected multigraph, expressing the edges as "words". (Contributed by Mario Carneiro, 11-Mar-2015.)

⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ Word 𝑋) → (𝑉 UMGrph 𝐸 ↔ 𝐸 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}))

Theorem

umgraf2 25846*

The edge function of an undirected multigraph is a function into unordered pairs of vertices. Version of umgraf 25847 without explicitly specified domain of the edge function. (Contributed by Mario Carneiro, 12-Mar-2015.)

⊢ (𝑉 UMGrph 𝐸 → 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2})

Theorem

umgraf 25847*

The edge function of an undirected multigraph is a function into unordered pairs of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.)

⊢ ((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴) → 𝐸:𝐴⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2})

Theorem

umgrass 25848

An edge is a subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.)

⊢ ((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ⊆ 𝑉)

Theorem

umgran0 25849

An edge is a nonempty subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.)

⊢ ((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ≠ ∅)

Theorem

umgrale 25850

An edge has at most two ends. (Contributed by Mario Carneiro, 11-Mar-2015.)

⊢ ((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (#‘(𝐸‘𝐹)) ≤ 2)

Theorem

umgrafi 25851

An edge is a finite subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.)

⊢ ((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ∈ Fin)

Theorem

umgraex 25852*

An edge is an unordered pair of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.)

⊢ ((𝑉 UMGrph 𝐸 ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦})

Theorem

umgrares 25853

A subgraph of a graph (formed by removing some edges from the original graph) is a graph. (Contributed by Mario Carneiro, 12-Mar-2015.)

⊢ (𝑉 UMGrph 𝐸 → 𝑉 UMGrph (𝐸 ↾ 𝐴))

Theorem

umgra0 25854

The empty graph, with vertices but no edges, is a graph. (Contributed by Mario Carneiro, 12-Mar-2015.)

⊢ (𝑉 ∈ 𝑊 → 𝑉 UMGrph ∅)

Theorem

umgra1 25855

The graph with one edge. (Contributed by Mario Carneiro, 12-Mar-2015.)

⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝑉 UMGrph {⟨𝐴, {𝐵, 𝐶}⟩})

Theorem

umisuhgra 25856

An undirected multigraph is an undirected hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017.)

⊢ (𝑉 UMGrph 𝐸 → 𝑉 UHGrph 𝐸)

Theorem

umgraun 25857

The union of two (undirected) multigraphs (with the same vertex set): If ⟨𝑉, 𝐸⟩ and ⟨𝑉, 𝐹⟩ are graphs, then ⟨𝑉, 𝐸 ∪ 𝐹⟩ is a graph (the vertex set stays the same, but the edges from both graphs are kept). (Contributed by Mario Carneiro, 12-Mar-2015.)

⊢ (𝜑 → 𝐸 Fn 𝐴)    &   ⊢ (𝜑 → 𝐹 Fn 𝐵)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝑉 UMGrph 𝐸)    &   ⊢ (𝜑 → 𝑉 UMGrph 𝐹)    ⇒   ⊢ (𝜑 → 𝑉 UMGrph (𝐸 ∪ 𝐹))

17.1.3  Undirected simple graphs

17.1.3.1  Undirected simple graphs - basics

Syntax

cuslg 25858

Extend class notation with undirected (simple) graphs with loops.

class USLGrph

Syntax

cusg 25859

Extend class notation with undirected (simple) graphs (without loops).

class USGrph

Syntax

cedg 25860

Extend class notation with the set of edges (of an undirected simple graph).

class Edges

Definition

df-uslgra 25861*

Define the class of all undirected simple graphs with loops. An undirected simple graph with loops is a special undirected multigraph ⟨𝑉, 𝐸⟩ where 𝐸 is an injective (one-to-one) function into subsets of 𝑉 of cardinality one or two, representing the two vertices incident to the edge, or the one vertex if the edge is a loop. In contrast to a multigraph, there is at most one edge between two vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.)

⊢ USLGrph = {⟨𝑣, 𝑒⟩ ∣ 𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}}

Definition

df-usgra 25862*

Define the class of all undirected simple graphs without loops. An undirected simple graph without loops is a special undirected simple graph ⟨𝑉, 𝐸⟩ where 𝐸 is an injective (one-to-one) function into subsets of 𝑉 of cardinality two, representing the two vertices incident to the edge. Such graphs are usually simply called "undirected graphs", so if only the term "undirected graph" is used, an undirected simple graph without loops is meant. Therefore, an undirected graph has no loops (edges a vertex to itself). (Contributed by Alexander van der Vekens, 10-Aug-2017.)

⊢ USGrph = {⟨𝑣, 𝑒⟩ ∣ 𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) = 2}}

Theorem

reluslgra 25863

The class of all undirected simple graph with loops is a relation. (Contributed by Alexander van der Vekens, 10-Aug-2017.)

⊢ Rel USLGrph

Theorem

relusgra 25864

The class of all undirected simple graph without loops is a relation. (Contributed by Alexander van der Vekens, 10-Aug-2017.)

⊢ Rel USGrph

Definition

df-edg 25865

Define the class of edges of a graph, see also definition ("E = E(G)") in section I.1 of [Bollobas] p. 1. This definition is very general: It defines edges for any ordered pairs as the range of its second component (which even needs not to be a function). Therefore, this definition could also be used for hypergraphs and multigraphs. In these cases, however, the (possibly more than one) edges connecting the same vertices could not be distinguished anymore. Therefore, this definition should only be used for undirected simple graphs. (Contributed by AV, 1-Jan-2020.)

⊢ Edges = (𝑔 ∈ V ↦ ran (2^nd ‘𝑔))

Theorem

uslgrav 25866

The classes of vertices and edges of an undirected simple graph with loops are sets. (Contributed by Alexander van der Vekens, 20-Aug-2017.)

⊢ (𝑉 USLGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V))

Theorem

usgrav 25867

The classes of vertices and edges of an undirected simple graph without loops are sets. (Contributed by Alexander van der Vekens, 19-Aug-2017.)

⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V))

Theorem

edgval 25868

The edges of a graph. (Contributed by AV, 1-Jan-2020.)

⊢ (𝐺 ∈ 𝑉 → (Edges‘𝐺) = ran (2^nd ‘𝐺))

Theorem

edgopval 25869

The edges of a graph represented as ordered pair. (Contributed by AV, 1-Jan-2020.)

⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (Edges‘⟨𝑉, 𝐸⟩) = ran 𝐸)

Theorem

edgov 25870

The edges of a graph, shown as operation value. Although a little less intuitive, this representation is often used because it is shorter than the representation as function value of a graph given as ordered pair, see edgopval 25869. The representation ran 𝐸 for the set of edges is even shorter, though. (Contributed by AV, 2-Jan-2020.)

⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉Edges𝐸) = ran 𝐸)

Theorem

edguslgra 25871

The edges of an undirected simple graph with loops. (Contributed by AV, 2-Jan-2020.)

⊢ (𝑉 USLGrph 𝐸 → (𝑉Edges𝐸) = ran 𝐸)

Theorem

isuslgra 25872*

The property of being an undirected simple graph with loops. (Contributed by Alexander van der Vekens, 10-Aug-2017.)

⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉 USLGrph 𝐸 ↔ 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}))

Theorem

isusgra 25873*

The property of being an undirected simple graph without loops. (Contributed by Alexander van der Vekens, 10-Aug-2017.)

⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉 USGrph 𝐸 ↔ 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) = 2}))

Theorem

uslgraf 25874*

The edge function of an undirected simple graph with loops is a one-to-one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.)

⊢ (𝑉 USLGrph 𝐸 → 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2})

Theorem

usgraf 25875*

The edge function of an undirected simple graph without loops is a one-to-one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.)

⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) = 2})

Theorem

isusgra0 25876*

The property of being an undirected simple graph without loops. (Contributed by Alexander van der Vekens, 13-Aug-2017.)

⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉 USGrph 𝐸 ↔ 𝐸:dom 𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}))

Theorem

usgraf0 25877*

The edge function of an undirected simple graph without loops is a one-to-one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 13-Aug-2017.)

⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})

Theorem

usgrafun 25878

The edge function of an undirected simple graph without loops is a function. (Contributed by Alexander van der Vekens, 18-Aug-2017.)

⊢ (𝑉 USGrph 𝐸 → Fun 𝐸)

Theorem

usgraop 25879*

An undirected simple graph without loops represented as ordered pair with a one-to-one edge function. (Contributed by AV, 1-Jan-2020.)

⊢ (𝐺 ∈ USGrph → ∃𝑣∃𝑒(𝐺 = ⟨𝑣, 𝑒⟩ ∧ 𝑒:dom 𝑒–1-1→{𝑥 ∈ 𝒫 𝑣 ∣ (#‘𝑥) = 2}))

Theorem

usgrac 25880

An undirected simple graph represented by a class induces a representation as binary relation. (Contributed by AV, 1-Jan-2020.)

⊢ (𝐺 ∈ USGrph → (1^st ‘𝐺) USGrph (2^nd ‘𝐺))

Theorem

edgss 25881*

The set of edges of an undirected simple graph without loops is a subset of the set of unordered pairs of vertices. (Contributed by AV, 1-Jan-2020.)

⊢ (𝐺 ∈ USGrph → (Edges‘𝐺) ⊆ {𝑥 ∈ 𝒫 (1^st ‘𝐺) ∣ (#‘𝑥) = 2})

Theorem

edg 25882

An edge of an undirected simple graph without loops is an unordered pair of vertices. (Contributed by AV, 1-Jan-2020.)

⊢ ((𝐺 ∈ USGrph ∧ 𝐸 ∈ (Edges‘𝐺)) → (𝐸 ∈ 𝒫 (1^st ‘𝐺) ∧ (#‘𝐸) = 2))

Theorem

isausgra 25883*

The property of an unordered pair to be an alternatively defined undirected simple graph without loops (defined as a pair (V,E) of a set V (vertex set) and a set of unordered pairs of elements of V (edge set). (Contributed by Alexander van der Vekens, 28-Aug-2017.)

⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (#‘𝑥) = 2}}    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉𝐺𝐸 ↔ 𝐸 ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}))

Theorem

ausisusgra 25884*

The equivalence of the definitions of an undirected simple graph without loops. (Contributed by Alexander van der Vekens, 28-Aug-2017.)

⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (#‘𝑥) = 2}}    ⇒   ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉𝐺𝐸 ↔ 𝑉 USGrph ( I ↾ 𝐸)))

Theorem

ausisusgraedg 25885*

The equivalence of the definitions of an undirected simple graph without loops, expressed with the set of edges. (Contributed by AV, 2-Jan-2020.)

⊢ 𝐺 = {⟨𝑣, 𝑒⟩ ∣ 𝑒 ⊆ {𝑥 ∈ 𝒫 𝑣 ∣ (#‘𝑥) = 2}}    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉𝐺(𝑉Edges𝐸) ↔ 𝑉 USGrph ( I ↾ ran 𝐸)))

Theorem

usgraedgop 25886

An edge of an undirected simple graph as second component of an ordered pair. (Contributed by Alexander van der Vekens, 17-Aug-2017.) (Proof shortened by Alexander van der Vekens, 16-Dec-2017.)

⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ dom 𝐸) → ((𝐸‘𝑋) = {𝑀, 𝑁} ↔ ⟨𝑋, {𝑀, 𝑁}⟩ ∈ 𝐸))

Theorem

usgraf1o 25887

The edge function of an undirected simple graph without loops is a bijective function onto its range. (Contributed by Alexander van der Vekens, 18-Nov-2017.)

⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1-onto→ran 𝐸)

Theorem

uslgraf1oedg 25888

The edge function of an undirected simple graph with loops is a bijective function onto the edges of the graph. (Contributed by AV, 2-Jan-2020.)

⊢ (𝑉 USLGrph 𝐸 → 𝐸:dom 𝐸–1-1-onto→(𝑉Edges𝐸))

Theorem

usgraf1 25889

The edge function of an undirected simple graph without loops is a one to one function. (Contributed by Alexander van der Vekens, 18-Nov-2017.)

⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1→ran 𝐸)

Theorem

usgrass 25890

An edge is a subset of vertices, analogous to umgrass 25848. (Contributed by Alexander van der Vekens, 19-Aug-2017.)

⊢ ((𝑉 USGrph 𝐸 ∧ 𝐹 ∈ dom 𝐸) → (𝐸‘𝐹) ⊆ 𝑉)

Theorem

usgraeq12d 25891

Equality of simple graphs without loops. (Contributed by Alexander van der Vekens, 11-Aug-2017.)

⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → (𝑉 USGrph 𝐸 ↔ 𝑊 USGrph 𝐹))

Theorem

uslisushgra 25892

An undirected simple graph with loops is an undirected simple hypergraph. (Contributed by AV, 19-Jan-2020.)

⊢ (𝑉 USLGrph 𝐸 → 𝑉 USHGrph 𝐸)

Theorem

uslisumgra 25893

An undirected simple graph with loops is an undirected multigraph. (Contributed by Alexander van der Vekens, 10-Aug-2017.)

⊢ (𝑉 USLGrph 𝐸 → 𝑉 UMGrph 𝐸)

Theorem

usisuslgra 25894

An undirected simple graph without loops is an undirected simple graph with loops. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Proof shortened by Alexander van der Vekens, 20-Mar-2018.)

⊢ (𝑉 USGrph 𝐸 → 𝑉 USLGrph 𝐸)

Theorem

usisumgra 25895

An undirected simple graph without loops is an undirected multigraph. (Contributed by Alexander van der Vekens, 20-Aug-2017.)

⊢ (𝑉 USGrph 𝐸 → 𝑉 UMGrph 𝐸)

Theorem

usisuhgra 25896

An undirected simple graph without loops is an undirected hypergraph. (Contributed by Alexander van der Vekens, 9-Feb-2018.)

⊢ (𝑉 USGrph 𝐸 → 𝑉 UHGrph 𝐸)

Theorem

elusuhgra 25897

An undirected simple graph without loops is an undirected hypergraph. (Contributed by AV, 9-Jan-2020.)

⊢ (𝐺 ∈ USGrph → 𝐺 ∈ UHGrph )

Theorem

usgrares 25898

A subgraph of a graph (formed by removing some edges from the original graph) is a graph, analogous to umgrares 25853. (Contributed by Alexander van der Vekens, 10-Aug-2017.)

⊢ (𝑉 USGrph 𝐸 → 𝑉 USGrph (𝐸 ↾ 𝐴))

Theorem

usgra0 25899

The empty graph, with vertices but no edges, is a graph, analogous to umgra0 25854. (Contributed by Alexander van der Vekens, 10-Aug-2017.) (Proof shortened by AV, 25-Nov-2020.)

⊢ (𝑉 ∈ 𝑊 → 𝑉 USGrph ∅)

Theorem

usgra0v 25900

The empty graph with no vertices is a graph if and only if the edge function is empty. (Contributed by Alexander van der Vekens, 30-Sep-2017.)

⊢ (∅ USGrph 𝐸 ↔ 𝐸 = ∅)