Definition df-clnbgr

Description: Define the closedneighborhood resp. the class of all neighbors of a vertex (in a graph) and the vertex itself, see definition in section I.1 of Bollobas p. 3. The closed neighborhood of a vertex is the set of all vertices which are connected with this vertex by an edge and the vertex itself (in contrast to an open neighborhood, see df-nbgr ). Alternatively, a closed neighborhood of a vertex could have been defined as its open neighborhood enhanced by the vertex itself, see dfclnbgr4 . This definition is applicable even for arbitrary hypergraphs. (Contributed by AV, 7-May-2025)

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

Detailed syntax breakdown

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