Definition df-nbgr

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 (see df-clnbgr ), a vertex is not a neighbor of itself (see nbgrnself ). 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 ), 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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnbgr	|- NeighbVtx
1		vg	|- g
2		cvv	|- _V
3		vv	|- v
4		cvtx	|- Vtx
5	1	cv	|- g
6	5 4	cfv	|- ( Vtx ` g )
7		vn	|- n
8	3	cv	|- v
9	8	csn	|- { v }
10	6 9	cdif	|- ( ( Vtx ` g ) \ { v } )
11		ve	|- e
12		cedg	|- Edg
13	5 12	cfv	|- ( Edg ` g )
14	7	cv	|- n
15	8 14	cpr	|- { v , n }
16	11	cv	|- e
17	15 16	wss	|- { v , n } C_ e
18	17 11 13	wrex	|- E. e e. ( Edg ` g ) { v , n } C_ e
19	18 7 10	crab	|- { n e. ( ( Vtx ` g ) \ { v } ) | E. e e. ( Edg ` g ) { v , n } C_ e }
20	1 3 2 6 19	cmpo	|- ( g e. _V , v e. ( Vtx ` g ) |-> { n e. ( ( Vtx ` g ) \ { v } ) | E. e e. ( Edg ` g ) { v , n } C_ e } )
21	0 20	wceq	|- NeighbVtx = ( g e. _V , v e. ( Vtx ` g ) |-> { n e. ( ( Vtx ` g ) \ { v } ) | E. e e. ( Edg ` g ) { v , n } C_ e } )