Home | Metamath
Proof Explorer Theorem List (p. 268 of 449) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eengtrkge 26701 | The geometry structure for 𝔼↑𝑁 is a Euclidean geometry. (Contributed by Thierry Arnoux, 15-Mar-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑁 ∈ ℕ → (EEG‘𝑁) ∈ TarskiGE) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Basic concepts:
Basic kinds of graphs:
Terms and properties of graphs:
Special kinds of graphs:
For the terms "Path", "Walk", "Trail", "Circuit", "Cycle" see the remarks below and the definitions in Section I.1 in [Bollobas] p. 4-5. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
In the following, the vertices and (indexed) edges for an arbitrary class 𝐺 (called "graph" in the following) are defined and examined. The main result of this section is to show that the set of vertices (Vtx‘𝐺) of a graph 𝐺 is the first component 𝑉 of the graph 𝐺 if it is represented by an ordered pair 〈𝑉, 𝐸〉 (see opvtxfv 26717), or the base set (Base‘𝐺) of the graph 𝐺 if it is represented as extensible structure (see basvtxval 26729), and that the set of indexed edges resp. the edge function (iEdg‘𝐺) is the second component 𝐸 of the graph 𝐺 if it is represented by an ordered pair 〈𝑉, 𝐸〉 (see opiedgfv 26720), or the component (.ef‘𝐺) of the graph 𝐺 if it is represented as extensible structure (see edgfiedgval 26730). Finally, it is shown that the set of edges of a graph 𝐺 is the range of its edge function: (Edg‘𝐺) = ran (iEdg‘𝐺), see edgval 26762. Usually, a graph 𝐺 is a set. If 𝐺 is a proper class, however, it represents the null graph (without vertices and edges), because (Vtx‘𝐺) = ∅ and (iEdg‘𝐺) = ∅ holds, see vtxvalprc 26758 and iedgvalprc 26759. Up to the end of this section, the edges need not be related to the vertices. Once undirected hypergraphs are defined (see df-uhgr 26771), the edges become nonempty sets of vertices, and by this obtain their meaning as "connectors" of vertices. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cedgf 26702 | Extend class notation with an edge function. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class .ef | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-edgf 26703 | Define the edge function (indexed edges) of a graph. (Contributed by AV, 18-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ .ef = Slot ;18 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgfid 26704 | Utility theorem: index-independent form of df-edgf 26703. (Contributed by AV, 16-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ .ef = Slot (.ef‘ndx) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgfndxnn 26705 | The index value of the edge function extractor is a positive integer. This property should be ensured for every concrete coding because otherwise it could not be used in an extensible structure (slots must be positive integers). (Contributed by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (.ef‘ndx) ∈ ℕ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgfndxid 26706 | The value of the edge function extractor is the value of the corresponding slot of the structure. (Contributed by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ 𝑉 → (.ef‘𝐺) = (𝐺‘(.ef‘ndx))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | baseltedgf 26707 | The index value of the Base slot is less than the index value of the .ef slot. (Contributed by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (Base‘ndx) < (.ef‘ndx) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | slotsbaseefdif 26708 | The slots Base and .ef are different. (Contributed by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (Base‘ndx) ≠ (.ef‘ndx) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
The key concepts in graph theory are vertices and edges. In general, a graph "consists" (at least) of two sets: the set of vertices and the set of edges. The edges "connect" vertices. The meaning of "connect" is different for different kinds of graphs (directed/undirected graphs, hyper-/pseudo-/ multi-/simple graphs, etc.). The simplest way to represent a graph (of any kind) is to define a graph as "an ordered pair of disjoint sets (V, E)" (see section I.1 in [Bollobas] p. 1), or in the notation of Metamath: 〈𝑉, 𝐸〉. Another way is to regard a graph as a mathematical structure, which consistes at least of a set (of vertices) and a relation between the vertices (edge function), but which can be enhanced by additional features (see Wikipedia "Mathematical structure", 24-Sep-2020, https://en.wikipedia.org/wiki/Mathematical_structure): "In mathematics, a structure is a set endowed with some additional features on the set (e.g., operation, relation, metric, topology). Often, the additional features are attached or related to the set, so as to provide it with some additional meaning or significance.". Such structures are provided as "extensible structures" in Metamath, see df-struct 16475. To allow for expressing and proving most of the theorems for graphs independently from their representation, the functions Vtx and iEdg are defined (see df-vtx 26711 and df-iedg 26712), which provide the vertices resp. (indexed) edges of an arbitrary class 𝐺 which represents a graph: (Vtx‘𝐺) resp. (iEdg‘𝐺). In literature, these functions are often denoted also by "V" and "E", see section I.1 in [Bollobas] p. 1 ("If G is a graph, then V = V(G) is the vertex set of G, and E = E(G) is the edge set.") or section 1.1 in [Diestel] p. 2 ("The vertex set of graph G is referred to as V(G), its edge set as E(G)."). Instead of providing edges themselves, iEdg is intended to provide a function as mapping of "indices" (the domain of the function) to the edges (therefore called "set of indexed edges"), which allows for hyper-/pseudo-/multigraphs with more than one edge between two (or more) vertices. For example, e1 = e(1) = { a, b } and e2 = e(2) = { a, b } are two different edges connecting the same two vertices a and b (in a pseudograph). In section 1.10 of [Diestel] p. 28, the edge function is defined differently: as "map E -> V u. [V]^2 assigning to every edge either one or two vertices, its end.". Here, the domain is the set of abstract edges: for two different edges e1 and e2 connecting the same two vertices a and b, we would have e(e1) = e(e2) = { a, b }. Since the set of abstract edges can be chosen as index set, these definitions are equivalent. The result of these functions are as expected: for a graph represented as ordered pair (𝐺 ∈ (V × V)), the set of vertices is (Vtx‘𝐺) = (1st ‘𝐺) (see opvtxval 26716) and the set of (indexed) edges is (iEdg‘𝐺) = (2nd ‘𝐺) (see opiedgval 26719), or if 𝐺 is given as ordered pair 𝐺 = 〈𝑉, 𝐸〉, the set of vertices is (Vtx‘𝐺) = 𝑉 (see opvtxfv 26717) and the set of (indexed) edges is (iEdg‘𝐺) = 𝐸 (see opiedgfv 26720). And for a graph represented as extensible structure (𝐺 Struct 〈(Base‘ndx), (.ef‘ndx)〉), the set of vertices is (Vtx‘𝐺) = (Base‘𝐺) (see funvtxval 26731) and the set of (indexed) edges is (iEdg‘𝐺) = (.ef‘𝐺) (see funiedgval 26732), or if 𝐺 is given in its simplest form as extensible structure with two slots (𝐺 = {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉}), the set of vertices is (Vtx‘𝐺) = 𝑉 (see struct2grvtx 26740) and the set of (indexed) edges is (iEdg‘𝐺) = 𝐸 (see struct2griedg 26741). These two representations are convertible, see graop 26742 and grastruct 26743: If 𝐺 is a graph (for example 𝐺 = 〈𝑉, 𝐸〉), then 𝐻 = {〈(Base‘ndx), (Vtx‘𝐺)〉, 〈(.ef‘ndx), (iEdg‘𝐺)〉} represents essentially the same graph, and if 𝐺 is a graph (for example 𝐺 = {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉}), then 𝐻 = 〈(Vtx‘𝐺), (iEdg‘𝐺)〉 represents essentially the same graph. In both cases, (Vtx‘𝐺) = (Vtx‘𝐻) and (iEdg‘𝐺) = (iEdg‘𝐻) hold. Theorems gropd 26744 and gropeld 26746 show that if any representation of a graph with vertices 𝑉 and edges 𝐸 has a certain property, then the ordered pair 〈𝑉, 𝐸〉 of the set of vertices and the set of edges (which is such a representation of a graph with vertices 𝑉 and edges 𝐸) has this property. Analogously, theorems grstructd 26745 and grstructeld 26747 show that if any representation of a graph with vertices 𝑉 and edges 𝐸 has a certain property, then any extensible structure with base set 𝑉 and value 𝐸 in the slot for edge functions (which is also such a representation of a graph with vertices 𝑉 and edges 𝐸) has this property. Besides the usual way to represent graphs without edges (consisting of unconnected vertices only), which would be 𝐺 = 〈𝑉, ∅〉 or 𝐺 = {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), ∅〉}, a structure without a slot for edges can be used: 𝐺 = {〈(Base‘ndx), 𝑉〉}, see snstrvtxval 26750 and snstriedgval 26751. Analogously, the empty set ∅ can be used to represent the null graph, see vtxval0 26752 and iedgval0 26753, which can also be represented by 𝐺 = 〈∅, ∅〉 or 𝐺 = {〈(Base‘ndx), ∅〉, 〈(.ef‘ndx), ∅〉}. Even proper classes can be used to represent the null graph, see vtxvalprc 26758 and iedgvalprc 26759. Other classes should not be used to represent graphs, because there could be a degenerate behavior of the vertex set and (indexed) edge functions, see vtxvalsnop 26754 resp. iedgvalsnop 26755, and vtxval3sn 26756 resp. iedgval3sn 26757. Avoid directly depending on this detail so that theorems will not depend on the Kuratowski construction of ordered pairs, see also the comment for df-op 4566. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cvtx 26709 | Extend class notation with the vertices of "graphs". | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class Vtx | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | ciedg 26710 | Extend class notation with the indexed edges of "graphs". | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class iEdg | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-vtx 26711 | Define the function mapping a graph to the set of its vertices. This definition is very general: It defines the set of vertices for any ordered pair as its first component, and for any other class as its "base set". It is meaningful, however, only if the ordered pair represents a graph resp. the class is an extensible structure representing a graph. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 20-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Vtx = (𝑔 ∈ V ↦ if(𝑔 ∈ (V × V), (1st ‘𝑔), (Base‘𝑔))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-iedg 26712 | Define the function mapping a graph to its indexed edges. This definition is very general: It defines the indexed edges for any ordered pair as its second component, and for any other class as its "edge function". It is meaningful, however, only if the ordered pair represents a graph resp. the class is an extensible structure (containing a slot for "edge functions") representing a graph. (Contributed by AV, 20-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ iEdg = (𝑔 ∈ V ↦ if(𝑔 ∈ (V × V), (2nd ‘𝑔), (.ef‘𝑔))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | vtxval 26713 | The set of vertices of a graph. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (Vtx‘𝐺) = if(𝐺 ∈ (V × V), (1st ‘𝐺), (Base‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iedgval 26714 | The set of indexed edges of a graph. (Contributed by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (iEdg‘𝐺) = if(𝐺 ∈ (V × V), (2nd ‘𝐺), (.ef‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 1vgrex 26715 | A graph with at least one vertex is a set. (Contributed by AV, 2-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → 𝐺 ∈ V) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opvtxval 26716 | The set of vertices of a graph represented as an ordered pair of vertices and indexed edges. (Contributed by AV, 9-Jan-2020.) (Revised by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ (V × V) → (Vtx‘𝐺) = (1st ‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opvtxfv 26717 | The set of vertices of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘〈𝑉, 𝐸〉) = 𝑉) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opvtxov 26718 | The set of vertices of a graph represented as an ordered pair of vertices and indexed edges as operation value. (Contributed by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉Vtx𝐸) = 𝑉) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opiedgval 26719 | The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges. (Contributed by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ (V × V) → (iEdg‘𝐺) = (2nd ‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opiedgfv 26720 | The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (iEdg‘〈𝑉, 𝐸〉) = 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opiedgov 26721 | The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges as operation value. (Contributed by AV, 21-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉iEdg𝐸) = 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opvtxfvi 26722 | The set of vertices of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 4-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 ∈ V & ⊢ 𝐸 ∈ V ⇒ ⊢ (Vtx‘〈𝑉, 𝐸〉) = 𝑉 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | opiedgfvi 26723 | The set of indexed edges of a graph represented as an ordered pair of vertices and indexed edges as function value. (Contributed by AV, 4-Mar-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 ∈ V & ⊢ 𝐸 ∈ V ⇒ ⊢ (iEdg‘〈𝑉, 𝐸〉) = 𝐸 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funvtxdmge2val 26724 | The set of vertices of an extensible structure with (at least) two slots. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((Fun (𝐺 ∖ {∅}) ∧ 2 ≤ (♯‘dom 𝐺)) → (Vtx‘𝐺) = (Base‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funiedgdmge2val 26725 | The set of indexed edges of an extensible structure with (at least) two slots. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((Fun (𝐺 ∖ {∅}) ∧ 2 ≤ (♯‘dom 𝐺)) → (iEdg‘𝐺) = (.ef‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funvtxdm2val 26726 | The set of vertices of an extensible structure with (at least) two slots. (Contributed by AV, 22-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((Fun (𝐺 ∖ {∅}) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵} ⊆ dom 𝐺) → (Vtx‘𝐺) = (Base‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funiedgdm2val 26727 | The set of indexed edges of an extensible structure with (at least) two slots. (Contributed by AV, 22-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((Fun (𝐺 ∖ {∅}) ∧ 𝐴 ≠ 𝐵 ∧ {𝐴, 𝐵} ⊆ dom 𝐺) → (iEdg‘𝐺) = (.ef‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funvtxval0 26728 | The set of vertices of an extensible structure with a base set and (at least) another slot. (Contributed by AV, 22-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑆 ∈ V ⇒ ⊢ ((Fun (𝐺 ∖ {∅}) ∧ 𝑆 ≠ (Base‘ndx) ∧ {(Base‘ndx), 𝑆} ⊆ dom 𝐺) → (Vtx‘𝐺) = (Base‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | basvtxval 26729 | The set of vertices of a graph represented as an extensible structure with the set of vertices as base set. (Contributed by AV, 14-Oct-2020.) (Revised by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → 2 ≤ (♯‘dom 𝐺)) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 〈(Base‘ndx), 𝑉〉 ∈ 𝐺) ⇒ ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgfiedgval 26730 | The set of indexed edges of a graph represented as an extensible structure with the indexed edges in the slot for edge functions. (Contributed by AV, 14-Oct-2020.) (Revised by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → 2 ≤ (♯‘dom 𝐺)) & ⊢ (𝜑 → 𝐸 ∈ 𝑌) & ⊢ (𝜑 → 〈(.ef‘ndx), 𝐸〉 ∈ 𝐺) ⇒ ⊢ (𝜑 → (iEdg‘𝐺) = 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funvtxval 26731 | The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 22-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((Fun (𝐺 ∖ {∅}) ∧ {(Base‘ndx), (.ef‘ndx)} ⊆ dom 𝐺) → (Vtx‘𝐺) = (Base‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funiedgval 26732 | The set of indexed edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 21-Sep-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((Fun (𝐺 ∖ {∅}) ∧ {(Base‘ndx), (.ef‘ndx)} ⊆ dom 𝐺) → (iEdg‘𝐺) = (.ef‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | structvtxvallem 26733 | Lemma for structvtxval 26734 and structiedg0val 26735. (Contributed by AV, 23-Sep-2020.) (Revised by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑆 ∈ ℕ & ⊢ (Base‘ndx) < 𝑆 & ⊢ 𝐺 = {〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉} ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 2 ≤ (♯‘dom 𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | structvtxval 26734 | The set of vertices of an extensible structure with a base set and another slot. (Contributed by AV, 23-Sep-2020.) (Proof shortened by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑆 ∈ ℕ & ⊢ (Base‘ndx) < 𝑆 & ⊢ 𝐺 = {〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉} ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘𝐺) = 𝑉) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | structiedg0val 26735 | The set of indexed edges of an extensible structure with a base set and another slot not being the slot for edge functions is empty. (Contributed by AV, 23-Sep-2020.) (Proof shortened by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑆 ∈ ℕ & ⊢ (Base‘ndx) < 𝑆 & ⊢ 𝐺 = {〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉} ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑆 ≠ (.ef‘ndx)) → (iEdg‘𝐺) = ∅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | structgrssvtxlem 26736 | Lemma for structgrssvtx 26737 and structgrssiedg 26738. (Contributed by AV, 14-Oct-2020.) (Proof shortened by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 𝐸 ∈ 𝑍) & ⊢ (𝜑 → {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉} ⊆ 𝐺) ⇒ ⊢ (𝜑 → 2 ≤ (♯‘dom 𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | structgrssvtx 26737 | The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 14-Oct-2020.) (Proof shortened by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 𝐸 ∈ 𝑍) & ⊢ (𝜑 → {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉} ⊆ 𝐺) ⇒ ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | structgrssiedg 26738 | The set of indexed edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 14-Oct-2020.) (Proof shortened by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 𝐸 ∈ 𝑍) & ⊢ (𝜑 → {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉} ⊆ 𝐺) ⇒ ⊢ (𝜑 → (iEdg‘𝐺) = 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | struct2grstr 26739 | A graph represented as an extensible structure with vertices as base set and indexed edges is actually an extensible structure. (Contributed by AV, 23-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐺 = {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉} ⇒ ⊢ 𝐺 Struct 〈(Base‘ndx), (.ef‘ndx)〉 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | struct2grvtx 26740 | The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 23-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐺 = {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉} ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (Vtx‘𝐺) = 𝑉) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | struct2griedg 26741 | The set of indexed edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 23-Sep-2020.) (Proof shortened by AV, 12-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐺 = {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉} ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (iEdg‘𝐺) = 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | graop 26742 | Any representation of a graph 𝐺 (especially as extensible structure 𝐺 = {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉}) is convertible in a representation of the graph as ordered pair. (Contributed by AV, 7-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐻 = 〈(Vtx‘𝐺), (iEdg‘𝐺)〉 ⇒ ⊢ ((Vtx‘𝐺) = (Vtx‘𝐻) ∧ (iEdg‘𝐺) = (iEdg‘𝐻)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | grastruct 26743 | Any representation of a graph 𝐺 (especially as ordered pair 𝐺 = 〈𝑉, 𝐸〉) is convertible in a representation of the graph as extensible structure. (Contributed by AV, 8-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐻 = {〈(Base‘ndx), (Vtx‘𝐺)〉, 〈(.ef‘ndx), (iEdg‘𝐺)〉} ⇒ ⊢ ((Vtx‘𝐺) = (Vtx‘𝐻) ∧ (iEdg‘𝐺) = (iEdg‘𝐻)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gropd 26744* | If any representation of a graph with vertices 𝑉 and edges 𝐸 has a certain property 𝜓, then the ordered pair 〈𝑉, 𝐸〉 of the set of vertices and the set of edges (which is such a representation of a graph with vertices 𝑉 and edges 𝐸) has this property. (Contributed by AV, 11-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → ∀𝑔(((Vtx‘𝑔) = 𝑉 ∧ (iEdg‘𝑔) = 𝐸) → 𝜓)) & ⊢ (𝜑 → 𝑉 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) ⇒ ⊢ (𝜑 → [〈𝑉, 𝐸〉 / 𝑔]𝜓) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | grstructd 26745* | If any representation of a graph with vertices 𝑉 and edges 𝐸 has a certain property 𝜓, then any structure with base set 𝑉 and value 𝐸 in the slot for edge functions (which is such a representation of a graph with vertices 𝑉 and edges 𝐸) has this property. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 9-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → ∀𝑔(((Vtx‘𝑔) = 𝑉 ∧ (iEdg‘𝑔) = 𝐸) → 𝜓)) & ⊢ (𝜑 → 𝑉 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑋) & ⊢ (𝜑 → Fun (𝑆 ∖ {∅})) & ⊢ (𝜑 → 2 ≤ (♯‘dom 𝑆)) & ⊢ (𝜑 → (Base‘𝑆) = 𝑉) & ⊢ (𝜑 → (.ef‘𝑆) = 𝐸) ⇒ ⊢ (𝜑 → [𝑆 / 𝑔]𝜓) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gropeld 26746* | If any representation of a graph with vertices 𝑉 and edges 𝐸 is an element of an arbitrary class 𝐶, then the ordered pair 〈𝑉, 𝐸〉 of the set of vertices and the set of edges (which is such a representation of a graph with vertices 𝑉 and edges 𝐸) is an element of this class 𝐶. (Contributed by AV, 11-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → ∀𝑔(((Vtx‘𝑔) = 𝑉 ∧ (iEdg‘𝑔) = 𝐸) → 𝑔 ∈ 𝐶)) & ⊢ (𝜑 → 𝑉 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) ⇒ ⊢ (𝜑 → 〈𝑉, 𝐸〉 ∈ 𝐶) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | grstructeld 26747* | If any representation of a graph with vertices 𝑉 and edges 𝐸 is an element of an arbitrary class 𝐶, then any structure with base set 𝑉 and value 𝐸 in the slot for edge functions (which is such a representation of a graph with vertices 𝑉 and edges 𝐸) is an element of this class 𝐶. (Contributed by AV, 12-Oct-2020.) (Revised by AV, 9-Jun-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → ∀𝑔(((Vtx‘𝑔) = 𝑉 ∧ (iEdg‘𝑔) = 𝐸) → 𝑔 ∈ 𝐶)) & ⊢ (𝜑 → 𝑉 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑋) & ⊢ (𝜑 → Fun (𝑆 ∖ {∅})) & ⊢ (𝜑 → 2 ≤ (♯‘dom 𝑆)) & ⊢ (𝜑 → (Base‘𝑆) = 𝑉) & ⊢ (𝜑 → (.ef‘𝑆) = 𝐸) ⇒ ⊢ (𝜑 → 𝑆 ∈ 𝐶) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | setsvtx 26748 | The vertices of a structure with a base set and an inserted resp. replaced slot for the edge function. (Contributed by AV, 18-Jan-2020.) (Revised by AV, 16-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐼 = (.ef‘ndx) & ⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝐺) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) ⇒ ⊢ (𝜑 → (Vtx‘(𝐺 sSet 〈𝐼, 𝐸〉)) = (Base‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | setsiedg 26749 | The (indexed) edges of a structure with a base set and an inserted resp. replaced slot for the edge function. (Contributed by AV, 7-Jun-2021.) (Revised by AV, 16-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐼 = (.ef‘ndx) & ⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝐺) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) ⇒ ⊢ (𝜑 → (iEdg‘(𝐺 sSet 〈𝐼, 𝐸〉)) = 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | snstrvtxval 26750 | The set of vertices of a graph without edges represented as an extensible structure with vertices as base set and no indexed edges. See vtxvalsnop 26754 for the (degenerate) case where 𝑉 = (Base‘ndx). (Contributed by AV, 23-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 ∈ V & ⊢ 𝐺 = {〈(Base‘ndx), 𝑉〉} ⇒ ⊢ (𝑉 ≠ (Base‘ndx) → (Vtx‘𝐺) = 𝑉) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | snstriedgval 26751 | The set of indexed edges of a graph without edges represented as an extensible structure with vertices as base set and no indexed edges. See iedgvalsnop 26755 for the (degenerate) case where 𝑉 = (Base‘ndx). (Contributed by AV, 24-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 ∈ V & ⊢ 𝐺 = {〈(Base‘ndx), 𝑉〉} ⇒ ⊢ (𝑉 ≠ (Base‘ndx) → (iEdg‘𝐺) = ∅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | vtxval0 26752 | Degenerated case 1 for vertices: The set of vertices of the empty set is the empty set. (Contributed by AV, 24-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (Vtx‘∅) = ∅ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iedgval0 26753 | Degenerated case 1 for edges: The set of indexed edges of the empty set is the empty set. (Contributed by AV, 24-Sep-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (iEdg‘∅) = ∅ | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | vtxvalsnop 26754 | Degenerated case 2 for vertices: The set of vertices of a singleton containing an ordered pair with equal components is the singleton containing the component. (Contributed by AV, 24-Sep-2020.) (Proof shortened by AV, 15-Jul-2022.) (Avoid depending on this detail.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐵 ∈ V & ⊢ 𝐺 = {〈𝐵, 𝐵〉} ⇒ ⊢ (Vtx‘𝐺) = {𝐵} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iedgvalsnop 26755 | Degenerated case 2 for edges: The set of indexed edges of a singleton containing an ordered pair with equal components is the singleton containing the component. (Contributed by AV, 24-Sep-2020.) (Proof shortened by AV, 15-Jul-2022.) (Avoid depending on this detail.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐵 ∈ V & ⊢ 𝐺 = {〈𝐵, 𝐵〉} ⇒ ⊢ (iEdg‘𝐺) = {𝐵} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | vtxval3sn 26756 | Degenerated case 3 for vertices: The set of vertices of a singleton containing a singleton containing a singleton is the innermost singleton. (Contributed by AV, 24-Sep-2020.) (Avoid depending on this detail.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 ∈ V ⇒ ⊢ (Vtx‘{{{𝐴}}}) = {𝐴} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iedgval3sn 26757 | Degenerated case 3 for edges: The set of indexed edges of a singleton containing a singleton containing a singleton is the innermost singleton. (Contributed by AV, 24-Sep-2020.) (Avoid depending on this detail.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 ∈ V ⇒ ⊢ (iEdg‘{{{𝐴}}}) = {𝐴} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | vtxvalprc 26758 | Degenerated case 4 for vertices: The set of vertices of a proper class is the empty set. (Contributed by AV, 12-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐶 ∉ V → (Vtx‘𝐶) = ∅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iedgvalprc 26759 | Degenerated case 4 for edges: The set of indexed edges of a proper class is the empty set. (Contributed by AV, 12-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐶 ∉ V → (iEdg‘𝐶) = ∅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cedg 26760 | Extend class notation with the set of edges (of an undirected simple (hyper-/pseudo-)graph). | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class Edg | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-edg 26761 | 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 of a class as the range of its edge function (which does not even need to be a function). Therefore, this definition could also be used for hypergraphs, pseudographs and multigraphs. In these cases, however, the (possibly more than one) edges connecting the same vertices could not be distinguished anymore. In some cases, this is no problem, so theorems with Edg are meaningful nevertheless (e.g., edguhgr 26842). Usually, however, this definition is used only for undirected simple (hyper-/pseudo-)graphs (with or without loops). (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgval 26762 | The edges of a graph. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.) (Revised by AV, 8-Dec-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (Edg‘𝐺) = ran (iEdg‘𝐺) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iedgedg 26763 | An indexed edge is an edge. (Contributed by AV, 19-Dec-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((Fun 𝐸 ∧ 𝐼 ∈ dom 𝐸) → (𝐸‘𝐼) ∈ (Edg‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgopval 26764 | The edges of a graph represented as ordered pair. (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (Edg‘〈𝑉, 𝐸〉) = ran 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgov 26765 | The edges of a graph represented as ordered pair, 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 26764. The representation ran 𝐸 for the set of edges is even shorter, though. (Contributed by AV, 2-Jan-2020.) (Revised by AV, 13-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (𝑉Edg𝐸) = ran 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgstruct 26766 | The edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 13-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐺 = {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉} ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (Edg‘𝐺) = ran 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edgiedgb 26767* | A set is an edge iff it is an indexed edge. (Contributed by AV, 17-Oct-2020.) (Revised by AV, 8-Dec-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (Fun 𝐼 → (𝐸 ∈ (Edg‘𝐺) ↔ ∃𝑥 ∈ dom 𝐼 𝐸 = (𝐼‘𝑥))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | edg0iedg0 26768 | There is no edge in a graph iff its edge function is empty. (Contributed by AV, 15-Dec-2020.) (Revised by AV, 8-Dec-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (Fun 𝐼 → (𝐸 = ∅ ↔ 𝐼 = ∅)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
For undirected graphs, we will have the following hierarchy/taxonomy: * Undirected Hypergraph: UHGraph * Undirected loop-free graphs: ULFGraph (not defined formally yet) * Undirected simple Hypergraph: USHGraph => USHGraph ⊆ UHGraph (ushgruhgr 26782) * Undirected Pseudograph: UPGraph => UPGraph ⊆ UHGraph (upgruhgr 26815) * Undirected loop-free hypergraph: ULFHGraph (not defined formally yet) => ULFHGraph ⊆ UHGraph and ULFHGraph ⊆ ULFGraph * Undirected loop-free simple hypergraph: ULFSHGraph (not defined formally yet) => ULFSHGraph ⊆ USHGraph and ULFSHGraph ⊆ ULFHGraph * Undirected simple Pseudograph: USPGraph => USPGraph ⊆ UPGraph (uspgrupgr 26889) and USPGraph ⊆ USHGraph (uspgrushgr 26888), see also uspgrupgrushgr 26890 * Undirected Muligraph: UMGraph => UMGraph ⊆ UPGraph (umgrupgr 26816) and UMGraph ⊆ ULFHGraph (umgrislfupgr 26836) * Undirected simple Graph: USGraph => USGraph ⊆ USPGraph (usgruspgr 26891) and USGraph ⊆ UMGraph (usgrumgr 26892) and USGraph ⊆ ULFSHGraph (usgrislfuspgr 26897) see also usgrumgruspgr 26893 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cuhgr 26769 | Extend class notation with undirected hypergraphs. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class UHGraph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cushgr 26770 | Extend class notation with undirected simple hypergraphs. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class USHGraph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-uhgr 26771* | Define the class of all undirected hypergraphs. An undirected hypergraph consists of a set 𝑣 (of "vertices") and a function 𝑒 (representing indexed "edges") into the power set of this set (the empty set excluded). (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 8-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ UHGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅})} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-ushgr 26772* | Define the class of all undirected simple hypergraphs. An undirected simple hypergraph is a special (non-simple, multiple, multi-) hypergraph for which the edge function 𝑒 is an injective (one-to-one) function into subsets of the set of vertices 𝑣, representing the (one or more) vertices incident to the edge. This definition corresponds to the definition of hypergraphs in section I.1 of [Bollobas] p. 7 (except that the empty set seems to be allowed to be an "edge") or section 1.10 of [Diestel] p. 27, where "E is a subset of [...] the power set of V, that is the set of all subsets of V" resp. "the elements of E are nonempty subsets (of any cardinality) of V". (Contributed by AV, 19-Jan-2020.) (Revised by AV, 8-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ USHGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→(𝒫 𝑣 ∖ {∅})} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isuhgr 26773 | The predicate "is an undirected hypergraph." (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 9-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ UHGraph ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isushgr 26774 | The predicate "is an undirected simple hypergraph." (Contributed by AV, 19-Jan-2020.) (Revised by AV, 9-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ USHGraph ↔ 𝐸:dom 𝐸–1-1→(𝒫 𝑉 ∖ {∅}))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgrf 26775 | 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.) (Revised by AV, 9-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UHGraph → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ushgrf 26776 | The edge function of an undirected simple hypergraph is a one-to-one function into the power set of the set of vertices. (Contributed by AV, 9-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ USHGraph → 𝐸:dom 𝐸–1-1→(𝒫 𝑉 ∖ {∅})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgrss 26777 | An edge is a subset of vertices. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 18-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝐹 ∈ dom 𝐸) → (𝐸‘𝐹) ⊆ 𝑉) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgreq12g 26778 | If two sets have the same vertices and the same edges, one set is a hypergraph iff the other set is a hypergraph. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 18-Jan-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝑊 = (Vtx‘𝐻) & ⊢ 𝐹 = (iEdg‘𝐻) ⇒ ⊢ (((𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌) ∧ (𝑉 = 𝑊 ∧ 𝐸 = 𝐹)) → (𝐺 ∈ UHGraph ↔ 𝐻 ∈ UHGraph)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgrfun 26779 | The edge function of an undirected hypergraph is a function. (Contributed by Alexander van der Vekens, 26-Dec-2017.) (Revised by AV, 15-Dec-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UHGraph → Fun 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgrn0 26780 | An edge is a nonempty subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 15-Dec-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ≠ ∅) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | lpvtx 26781 | The endpoints of a loop (which is an edge at index 𝐽) are two (identical) vertices 𝐴. (Contributed by AV, 1-Feb-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ (𝐼‘𝐽) = {𝐴}) → 𝐴 ∈ (Vtx‘𝐺)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ushgruhgr 26782 | An undirected simple hypergraph is an undirected hypergraph. (Contributed by AV, 19-Jan-2020.) (Revised by AV, 9-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐺 ∈ USHGraph → 𝐺 ∈ UHGraph) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isuhgrop 26783 | 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.) (Revised by AV, 9-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋) → (〈𝑉, 𝐸〉 ∈ UHGraph ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgr0e 26784 | The empty graph, with vertices but no edges, is a hypergraph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 25-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → (iEdg‘𝐺) = ∅) ⇒ ⊢ (𝜑 → 𝐺 ∈ UHGraph) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgr0vb 26785 | 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.) (Revised by AV, 9-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅) → (𝐺 ∈ UHGraph ↔ (iEdg‘𝐺) = ∅)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgr0 26786 | The null graph represented by an empty set is a hypergraph. (Contributed by AV, 9-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ∅ ∈ UHGraph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgrun 26787 | The union 𝑈 of two (undirected) hypergraphs 𝐺 and 𝐻 with the same vertex set 𝑉 is a hypergraph with the vertex 𝑉 and the union (𝐸 ∪ 𝐹) of the (indexed) edges. (Contributed by AV, 11-Oct-2020.) (Revised by AV, 24-Oct-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐺 ∈ UHGraph) & ⊢ (𝜑 → 𝐻 ∈ UHGraph) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅) & ⊢ (𝜑 → 𝑈 ∈ 𝑊) & ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑈) = (𝐸 ∪ 𝐹)) ⇒ ⊢ (𝜑 → 𝑈 ∈ UHGraph) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgrunop 26788 | The union of two (undirected) hypergraphs (with the same vertex set) represented as ordered pair: 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). (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 11-Oct-2020.) (Revised by AV, 24-Oct-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐺 ∈ UHGraph) & ⊢ (𝜑 → 𝐻 ∈ UHGraph) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅) ⇒ ⊢ (𝜑 → 〈𝑉, (𝐸 ∪ 𝐹)〉 ∈ UHGraph) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ushgrun 26789 | The union 𝑈 of two (undirected) simple hypergraphs 𝐺 and 𝐻 with the same vertex set 𝑉 is a (not necessarily simple) hypergraph with the vertex 𝑉 and the union (𝐸 ∪ 𝐹) of the (indexed) edges. (Contributed by AV, 29-Nov-2020.) (Revised by AV, 24-Oct-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐺 ∈ USHGraph) & ⊢ (𝜑 → 𝐻 ∈ USHGraph) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅) & ⊢ (𝜑 → 𝑈 ∈ 𝑊) & ⊢ (𝜑 → (Vtx‘𝑈) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑈) = (𝐸 ∪ 𝐹)) ⇒ ⊢ (𝜑 → 𝑈 ∈ UHGraph) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | ushgrunop 26790 | The union of two (undirected) simple hypergraphs (with the same vertex set) represented as ordered pair: If 〈𝑉, 𝐸〉 and 〈𝑉, 𝐹〉 are simple hypergraphs, then 〈𝑉, 𝐸 ∪ 𝐹〉 is a (not necessarily simple) hypergraph - the vertex set stays the same, but the edges from both graphs are kept, possibly resulting in two edges between two vertices. (Contributed by AV, 29-Nov-2020.) (Revised by AV, 24-Oct-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐺 ∈ USHGraph) & ⊢ (𝜑 → 𝐻 ∈ USHGraph) & ⊢ 𝐸 = (iEdg‘𝐺) & ⊢ 𝐹 = (iEdg‘𝐻) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) & ⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅) ⇒ ⊢ (𝜑 → 〈𝑉, (𝐸 ∪ 𝐹)〉 ∈ UHGraph) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uhgrstrrepe 26791 | Replacing (or adding) the edges (between elements of the base set) of an extensible structure results in a hypergraph. Instead of requiring (𝜑 → 𝐺 Struct 𝑋), it would be sufficient to require (𝜑 → Fun (𝐺 ∖ {∅})) and (𝜑 → 𝐺 ∈ V). (Contributed by AV, 18-Jan-2020.) (Revised by AV, 7-Jun-2021.) (Revised by AV, 16-Nov-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 = (Base‘𝐺) & ⊢ 𝐼 = (.ef‘ndx) & ⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝐺) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) & ⊢ (𝜑 → 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅})) ⇒ ⊢ (𝜑 → (𝐺 sSet 〈𝐼, 𝐸〉) ∈ UHGraph) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | incistruhgr 26792* | An incidence structure 〈𝑃, 𝐿, 𝐼〉 "where 𝑃 is a set whose elements are called points, 𝐿 is a distinct set whose elements are called lines and 𝐼 ⊆ (𝑃 × 𝐿) is the incidence relation" (see Wikipedia "Incidence structure" (24-Oct-2020), https://en.wikipedia.org/wiki/Incidence_structure) implies an undirected hypergraph, if the incidence relation is right-total (to exclude empty edges). The points become the vertices, and the edge function is derived from the incidence relation by mapping each line ("edge") to the set of vertices incident to the line/edge. With 𝑃 = (Base‘𝑆) and by defining two new slots for lines and incidence relations (analogous to LineG and Itv) and enhancing the definition of iEdg accordingly, it would even be possible to express that a corresponding incidence structure is an undirected hypergraph. By choosing the incident relation appropriately, other kinds of undirected graphs (pseudographs, multigraphs, simple graphs, etc.) could be defined. (Contributed by AV, 24-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐼 ⊆ (𝑃 × 𝐿) ∧ ran 𝐼 = 𝐿) → ((𝑉 = 𝑃 ∧ 𝐸 = (𝑒 ∈ 𝐿 ↦ {𝑣 ∈ 𝑃 ∣ 𝑣𝐼𝑒})) → 𝐺 ∈ UHGraph)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cupgr 26793 | Extend class notation with undirected pseudographs. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class UPGraph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cumgr 26794 | Extend class notation with undirected multigraphs. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class UMGraph | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-upgr 26795* | Define the class of all undirected pseudographs. An (undirected) pseudograph consists of a set 𝑣 (of "vertices") and a function 𝑒 (representing indexed "edges") 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. This is according to Chartrand, Gary and Zhang, Ping (2012): "A First Course in Graph Theory.", Dover, ISBN 978-0-486-48368-9, section 1.4, p. 26: "In a pseudograph, not only are parallel edges permitted but an edge is also permitted to join a vertex to itself. Such an edge is called a loop." (in contrast to a multigraph, see df-umgr 26796). (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 24-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ UPGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-umgr 26796* | Define the class of all undirected multigraphs. An (undirected) multigraph consists of a set 𝑣 (of "vertices") and a function 𝑒 (representing indexed "edges") into subsets of 𝑣 of cardinality two, representing the two vertices incident to the edge. In contrast to a pseudograph, a multigraph has no loop. This is according to Chartrand, Gary and Zhang, Ping (2012): "A First Course in Graph Theory.", Dover, ISBN 978-0-486-48368-9, section 1.4, p. 26: "A multigraph M consists of a finite nonempty set V of vertices and a set E of edges, where every two vertices of M are joined by a finite number of edges (possibly zero). If two or more edges join the same pair of (distinct) vertices, then these edges are called parallel edges." To provide uniform definitions for all kinds of graphs, 𝑥 ∈ (𝒫 𝑣 ∖ {∅}) is used as restriction of the class abstraction, although 𝑥 ∈ 𝒫 𝑣 would be sufficient (see prprrab 13821 and isumgrs 26809). (Contributed by AV, 24-Nov-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ UMGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (♯‘𝑥) = 2}} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isupgr 26797* | The property of being an undirected pseudograph. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ UPGraph ↔ 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | wrdupgr 26798* | The property of being an undirected pseudograph, expressing the edges as "words". (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ Word 𝑋) → (𝐺 ∈ UPGraph ↔ 𝐸 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | upgrf 26799* | The edge function of an undirected pseudograph is a function into unordered pairs of vertices. Version of upgrfn 26800 without explicitly specified domain of the edge function. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 10-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UPGraph → 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | upgrfn 26800* | The edge function of an undirected pseudograph is a function into unordered pairs of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴) → 𝐸:𝐴⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |