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

Definition df-nbgr 39450
Description: Define the (open) neighborhood resp. the class of all neighbors of a vertex (in a graph), see definition in section I.1 of [Bollobas] p. 3 or definition in section 1.1 of [Diestel] p. 3. The neighborhood/neighbors of a vertex are all (other) vertices which are connected with this vertex by an edge. In contrast to a closed neighborhood, a vertex is not a neighbor of itself. This definition is applicable even for arbitrary hypergraphs.

Remark: To distinguish this definition from other definitions for neighborhoods resp. neighbors (e.g.,  nei in Topology, see df-nei 20162), the suffix Vtx is added to the class constant NeighbVtx. (Contributed by Alexander van der Vekens and Mario Carneiro, 7-Oct-2017.) (Revised by AV, 24-Oct-2020.)

Assertion
Ref Expression
df-nbgr  |- NeighbVtx  =  ( g  e.  _V , 
v  e.  (Vtx `  g )  |->  { n  e.  ( (Vtx `  g
)  \  { v } )  |  E. e  e.  (Edg `  g
) { v ,  n }  C_  e } )
Distinct variable group:    e, g, n, v

Detailed syntax breakdown of Definition df-nbgr
StepHypRef Expression
1 cnbgr 39446 . 2  class NeighbVtx
2 vg . . 3  setvar  g
3 vv . . 3  setvar  v
4 cvv 3056 . . 3  class  _V
52cv 1453 . . . 4  class  g
6 cvtx 39146 . . . 4  class Vtx
75, 6cfv 5600 . . 3  class  (Vtx `  g )
83cv 1453 . . . . . . 7  class  v
9 vn . . . . . . . 8  setvar  n
109cv 1453 . . . . . . 7  class  n
118, 10cpr 3981 . . . . . 6  class  { v ,  n }
12 ve . . . . . . 7  setvar  e
1312cv 1453 . . . . . 6  class  e
1411, 13wss 3415 . . . . 5  wff  { v ,  n }  C_  e
15 cedga 39257 . . . . . 6  class Edg
165, 15cfv 5600 . . . . 5  class  (Edg `  g )
1714, 12, 16wrex 2749 . . . 4  wff  E. e  e.  (Edg `  g ) { v ,  n }  C_  e
188csn 3979 . . . . 5  class  { v }
197, 18cdif 3412 . . . 4  class  ( (Vtx
`  g )  \  { v } )
2017, 9, 19crab 2752 . . 3  class  { n  e.  ( (Vtx `  g
)  \  { v } )  |  E. e  e.  (Edg `  g
) { v ,  n }  C_  e }
212, 3, 4, 7, 20cmpt2 6316 . 2  class  ( g  e.  _V ,  v  e.  (Vtx `  g
)  |->  { n  e.  ( (Vtx `  g
)  \  { v } )  |  E. e  e.  (Edg `  g
) { v ,  n }  C_  e } )
221, 21wceq 1454 1  wff NeighbVtx  =  ( g  e.  _V , 
v  e.  (Vtx `  g )  |->  { n  e.  ( (Vtx `  g
)  \  { v } )  |  E. e  e.  (Edg `  g
) { v ,  n }  C_  e } )
Colors of variables: wff setvar class
This definition is referenced by:  nbgrprc0  39451  nbgrval  39455  nbgrnvtx0  39458  nbgrel  39459
  Copyright terms: Public domain W3C validator