Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-edga Structured version   Visualization version   Unicode version

Definition df-edga 39355
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 39365). 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.)
Assertion
Ref Expression
df-edga  |- Edg  =  ( g  e.  _V  |->  ran  (iEdg `  g )
)

Detailed syntax breakdown of Definition df-edga
StepHypRef Expression
1 cedga 39354 . 2  class Edg
2 vg . . 3  setvar  g
3 cvv 3057 . . 3  class  _V
42cv 1454 . . . . 5  class  g
5 ciedg 39244 . . . . 5  class iEdg
64, 5cfv 5605 . . . 4  class  (iEdg `  g )
76crn 4857 . . 3  class  ran  (iEdg `  g )
82, 3, 7cmpt 4477 . 2  class  ( g  e.  _V  |->  ran  (iEdg `  g ) )
91, 8wceq 1455 1  wff Edg  =  ( g  e.  _V  |->  ran  (iEdg `  g )
)
Colors of variables: wff setvar class
This definition is referenced by:  edgaval  39356
  Copyright terms: Public domain W3C validator