Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-edga | Structured version Visualization version GIF version |
Description: 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 40360). 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.) |
Ref | Expression |
---|---|
df-edga | ⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cedga 40349 | . 2 class Edg | |
2 | vg | . . 3 setvar 𝑔 | |
3 | cvv 3168 | . . 3 class V | |
4 | 2 | cv 1473 | . . . . 5 class 𝑔 |
5 | ciedg 40228 | . . . . 5 class iEdg | |
6 | 4, 5 | cfv 5786 | . . . 4 class (iEdg‘𝑔) |
7 | 6 | crn 5025 | . . 3 class ran (iEdg‘𝑔) |
8 | 2, 3, 7 | cmpt 4633 | . 2 class (𝑔 ∈ V ↦ ran (iEdg‘𝑔)) |
9 | 1, 8 | wceq 1474 | 1 wff Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔)) |
Colors of variables: wff setvar class |
This definition is referenced by: edgaval 40351 |
Copyright terms: Public domain | W3C validator |