Home | Metamath
Proof Explorer Theorem List (p. 260 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | basvtxval 25901 | 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 25902 | 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 | basvtxvalOLD 25903 | Obsolete version of basvtxval 25901 as of 12-Nov-2021. (Contributed by AV, 14-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐺 ∈ 𝑋) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → 2 ≤ (#‘dom 𝐺)) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 〈(Base‘ndx), 𝑉〉 ∈ 𝐺) ⇒ ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) | ||
Theorem | edgfiedgvalOLD 25904 | Obsolete version of edgfiedgval 25902 as of 12-Nov-2021. (Contributed by AV, 14-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝐺 ∈ 𝑋) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → 2 ≤ (#‘dom 𝐺)) & ⊢ (𝜑 → 𝐸 ∈ 𝑌) & ⊢ (𝜑 → 〈(.ef‘ndx), 𝐸〉 ∈ 𝐺) ⇒ ⊢ (𝜑 → (iEdg‘𝐺) = 𝐸) | ||
Theorem | funvtxval 25905 | 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 25906 | 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 | funvtxvalOLD 25907 | Obsolete version of funvtxval 25905 as of 12-Nov-2021. (Contributed by AV, 22-Sep-2020.) (Revised by AV, 7-Jun-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅}) ∧ {(Base‘ndx), (.ef‘ndx)} ⊆ dom 𝐺) → (Vtx‘𝐺) = (Base‘𝐺)) | ||
Theorem | funiedgvalOLD 25908 | Obsolete version of funiedgval 25906 as of 12-Nov-2021. (Contributed by AV, 21-Sep-2020.) (Revised by AV, 7-Jun-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅}) ∧ {(Base‘ndx), (.ef‘ndx)} ⊆ dom 𝐺) → (iEdg‘𝐺) = (.ef‘𝐺)) | ||
Theorem | structvtxvallem 25909 | Lemma for structvtxval 25910 and structiedg0val 25911. (Contributed by AV, 23-Sep-2020.) (Revised by AV, 12-Nov-2021.) |
⊢ 𝑆 ∈ ℕ & ⊢ (Base‘ndx) < 𝑆 & ⊢ 𝐺 = {〈(Base‘ndx), 𝑉〉, 〈𝑆, 𝐸〉} ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → 2 ≤ (#‘dom 𝐺)) | ||
Theorem | structvtxval 25910 | 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 25911 | 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 25912 | Lemma for structgrssvtx 25913 and structgrssiedg 25914. (Contributed by AV, 14-Oct-2020.) (Proof shortened by AV, 12-Nov-2021.) |
⊢ (𝜑 → 𝐺 Struct 𝑋) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 𝐸 ∈ 𝑍) & ⊢ (𝜑 → {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉} ⊆ 𝐺) ⇒ ⊢ (𝜑 → 2 ≤ (#‘dom 𝐺)) | ||
Theorem | structgrssvtx 25913 | 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 25914 | 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 | structgrssvtxlemOLD 25915 | Obsolete version of structgrssvtxlem 25912 as of 14-Nov-2021. (Contributed by AV, 14-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐺 ∈ 𝑋) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 𝐸 ∈ 𝑍) & ⊢ (𝜑 → {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉} ⊆ 𝐺) ⇒ ⊢ (𝜑 → 2 ≤ (#‘dom 𝐺)) | ||
Theorem | structgrssvtxOLD 25916 | Obsolete version of structgrssvtx 25913 as of 14-Nov-2021. (Contributed by AV, 14-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐺 ∈ 𝑋) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 𝐸 ∈ 𝑍) & ⊢ (𝜑 → {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉} ⊆ 𝐺) ⇒ ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) | ||
Theorem | structgrssiedgOLD 25917 | Obsolete version of structgrssiedg 25914 as of 14-Nov-2021. (Contributed by AV, 14-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐺 ∈ 𝑋) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 𝐸 ∈ 𝑍) & ⊢ (𝜑 → {〈(Base‘ndx), 𝑉〉, 〈(.ef‘ndx), 𝐸〉} ⊆ 𝐺) ⇒ ⊢ (𝜑 → (iEdg‘𝐺) = 𝐸) | ||
Theorem | struct2grstr 25918 | 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 25919 | 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 25920 | 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 25921 | 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 25922 | 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 25923* | 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 25924* | 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 25925* | 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 25926* | 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 25927 | 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 25928 | 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 25929 | 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 25933 for the (degenerated) case where 𝑉 = (Base‘ndx). (Contributed by AV, 23-Sep-2020.) |
⊢ 𝑉 ∈ V & ⊢ 𝐺 = {〈(Base‘ndx), 𝑉〉} ⇒ ⊢ (𝑉 ≠ (Base‘ndx) → (Vtx‘𝐺) = 𝑉) | ||
Theorem | snstriedgval 25930 | 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 25934 for the (degenerated) case where 𝑉 = (Base‘ndx). (Contributed by AV, 24-Sep-2020.) |
⊢ 𝑉 ∈ V & ⊢ 𝐺 = {〈(Base‘ndx), 𝑉〉} ⇒ ⊢ (𝑉 ≠ (Base‘ndx) → (iEdg‘𝐺) = ∅) | ||
Theorem | vtxval0 25931 | 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 25932 | 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 25933 | 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, 12-Nov-2021.) |
⊢ 𝐵 ∈ V & ⊢ 𝐺 = {〈𝐵, 𝐵〉} ⇒ ⊢ (Vtx‘𝐺) = {𝐵} | ||
Theorem | iedgvalsnop 25934 | 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, 12-Nov-2021.) |
⊢ 𝐵 ∈ V & ⊢ 𝐺 = {〈𝐵, 𝐵〉} ⇒ ⊢ (iEdg‘𝐺) = {𝐵} | ||
Theorem | vtxval3sn 25935 | 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.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (Vtx‘{{{𝐴}}}) = {𝐴} | ||
Theorem | iedgval3sn 25936 | 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.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (iEdg‘{{{𝐴}}}) = {𝐴} | ||
Theorem | vtxvalprc 25937 | 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 25938 | 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 25939 | Extend class notation with the set of edges (of an undirected simple (hyper-/pseudo-)graph). |
class Edg | ||
Definition | df-edg 25940 | 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 even needs not 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 26024). 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 25941 | 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 | edgvalOLD 25942 | Obsolete version of edgval 25941 as of 8-Dec-2021. (Contributed by AV, 1-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐺 ∈ 𝑉 → (Edg‘𝐺) = ran (iEdg‘𝐺)) | ||
Theorem | iedgedg 25943 | An indexed edge is an edge. (Contributed by AV, 19-Dec-2021.) |
⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((Fun 𝐸 ∧ 𝐼 ∈ dom 𝐸) → (𝐸‘𝐼) ∈ (Edg‘𝐺)) | ||
Theorem | edgopval 25944 | 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 25945 | 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 25944. 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 25946 | 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 25947* | 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 | edgiedgbOLD 25948* | Obsolete version of edgiedgb 25947 as of 8-Dec-2021. (Contributed by AV, 17-Oct-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ Fun 𝐼) → (𝐸 ∈ (Edg‘𝐺) ↔ ∃𝑥 ∈ dom 𝐼 𝐸 = (𝐼‘𝑥))) | ||
Theorem | edg0iedg0 25949 | 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 𝐼 → (𝐸 = ∅ ↔ 𝐼 = ∅)) | ||
Theorem | edg0iedg0OLD 25950 | Obsolete version of edg0iedg0 25949 as of 8-Dec-2021. (Contributed by AV, 15-Dec-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐼 = (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 25964) * Undirected Pseudograph: UPGraph => UPGraph ⊆ UHGraph (upgruhgr 25997) * 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 26071) and USPGraph ⊆ USHGraph (uspgrushgr 26070), see also uspgrupgrushgr 26072 * Undirected Muligraph: UMGraph => UMGraph ⊆ UPGraph (umgrupgr 25998) and UMGraph ⊆ ULFHGraph (umgrislfupgr 26018) * Undirected simple Graph: USGraph => USGraph ⊆ USPGraph (usgruspgr 26073) and USGraph ⊆ UMGraph (usgrumgr 26074) and USGraph ⊆ ULFSHGraph (usgrislfuspgr 26079) see also usgrumgruspgr 26075 | ||
Syntax | cuhgr 25951 | Extend class notation with undirected hypergraphs. |
class UHGraph | ||
Syntax | cushgr 25952 | Extend class notation with undirected simple hypergraphs. |
class USHGraph | ||
Definition | df-uhgr 25953* | 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 25954* | 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 non-empty 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 25955 | 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 25956 | 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 25957 | 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 25958 | 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 25959 | 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 25960 | 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 25961 | 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 25962 | 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 25963 | 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 25964 | An undirected simple hypergraph is an undirected hypergraph. (Contributed by AV, 19-Jan-2020.) (Revised by AV, 9-Oct-2020.) |
⊢ (𝐺 ∈ USHGraph → 𝐺 ∈ UHGraph ) | ||
Theorem | isuhgrop 25965 | 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 25966 | 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 25967 | 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 25968 | The null graph represented by an empty set is a hypergraph. (Contributed by AV, 9-Oct-2020.) |
⊢ ∅ ∈ UHGraph | ||
Theorem | uhgrun 25969 | 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 25970 | 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 25971 | 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 25972 | 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 25973 | 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 25974* | 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 25975 | Extend class notation with undirected pseudographs. |
class UPGraph | ||
Syntax | cumgr 25976 | Extend class notation with undirected multigraphs. |
class UMGraph | ||
Definition | df-upgr 25977* | 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 25978). (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 24-Nov-2020.) |
⊢ UPGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}} | ||
Definition | df-umgr 25978* | 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 13255 and isumgrs 25991). (Contributed by AV, 24-Nov-2020.) |
⊢ UMGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) = 2}} | ||
Theorem | isupgr 25979* | 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 25980* | 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 25981* | The edge function of an undirected pseudograph is a function into unordered pairs of vertices. Version of upgrfn 25982 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 25982* | 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}) | ||
Theorem | upgrss 25983 | An edge is a subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 29-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ dom 𝐸) → (𝐸‘𝐹) ⊆ 𝑉) | ||
Theorem | upgrn0 25984 | An edge is a nonempty subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ≠ ∅) | ||
Theorem | upgrle 25985 | An edge of an undirected pseudograph has at most two ends. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (#‘(𝐸‘𝐹)) ≤ 2) | ||
Theorem | upgrfi 25986 | An edge is a finite subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝐸‘𝐹) ∈ Fin) | ||
Theorem | upgrex 25987* | An edge is an unordered pair of vertices. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 10-Oct-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 (𝐸‘𝐹) = {𝑥, 𝑦}) | ||
Theorem | upgrbi 25988* | Show that an unordered pair is a valid edge in a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 28-Feb-2021.) |
⊢ 𝑋 ∈ 𝑉 & ⊢ 𝑌 ∈ 𝑉 ⇒ ⊢ {𝑋, 𝑌} ∈ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} | ||
Theorem | upgrop 25989 | A pseudograph represented by an ordered pair. (Contributed by AV, 12-Dec-2021.) |
⊢ (𝐺 ∈ UPGraph → 〈(Vtx‘𝐺), (iEdg‘𝐺)〉 ∈ UPGraph ) | ||
Theorem | isumgr 25990* | The property of being an undirected multigraph. (Contributed by AV, 24-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ UMGraph ↔ 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) = 2})) | ||
Theorem | isumgrs 25991* | The simplified property of being an undirected multigraph. (Contributed by AV, 24-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ UMGraph ↔ 𝐸:dom 𝐸⟶{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) | ||
Theorem | wrdumgr 25992* | The property of being an undirected multigraph, expressing the edges as "words". (Contributed by AV, 24-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ Word 𝑋) → (𝐺 ∈ UMGraph ↔ 𝐸 ∈ Word {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2})) | ||
Theorem | umgrf 25993* | The edge function of an undirected multigraph is a function into unordered pairs of vertices. Version of umgrfn 25994 without explicitly specified domain of the edge function. (Contributed by AV, 24-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UMGraph → 𝐸:dom 𝐸⟶{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) | ||
Theorem | umgrfn 25994* | The edge function of an undirected multigraph is a function into unordered pairs of vertices. (Contributed by AV, 24-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝐸 Fn 𝐴) → 𝐸:𝐴⟶{𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2}) | ||
Theorem | umgredg2 25995 | An edge of a multigraph has exactly two ends. (Contributed by AV, 24-Nov-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑋 ∈ dom 𝐸) → (#‘(𝐸‘𝑋)) = 2) | ||
Theorem | umgrbi 25996* | Show that an unordered pair is a valid edge in a multigraph. (Contributed by AV, 9-Mar-2021.) |
⊢ 𝑋 ∈ 𝑉 & ⊢ 𝑌 ∈ 𝑉 & ⊢ 𝑋 ≠ 𝑌 ⇒ ⊢ {𝑋, 𝑌} ∈ {𝑥 ∈ 𝒫 𝑉 ∣ (#‘𝑥) = 2} | ||
Theorem | upgruhgr 25997 | An undirected pseudograph is an undirected hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017.) (Revised by AV, 10-Oct-2020.) |
⊢ (𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph ) | ||
Theorem | umgrupgr 25998 | An undirected multigraph is an undirected pseudograph. (Contributed by AV, 25-Nov-2020.) |
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈ UPGraph ) | ||
Theorem | umgruhgr 25999 | An undirected multigraph is an undirected hypergraph. (Contributed by AV, 26-Nov-2020.) |
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈ UHGraph ) | ||
Theorem | upgrle2 26000 | An edge of an undirected pseudograph has at most two ends. (Contributed by AV, 6-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑋 ∈ dom 𝐼) → (#‘(𝐼‘𝑋)) ≤ 2) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |