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 ), 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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cnbgr | ||
1 | vg | ||
2 | cvv | ||
3 | vv | ||
4 | cvtx | ||
5 | 1 | cv | |
6 | 5 4 | cfv | |
7 | vn | ||
8 | 3 | cv | |
9 | 8 | csn | |
10 | 6 9 | cdif | |
11 | ve | ||
12 | cedg | ||
13 | 5 12 | cfv | |
14 | 7 | cv | |
15 | 8 14 | cpr | |
16 | 11 | cv | |
17 | 15 16 | wss | |
18 | 17 11 13 | wrex | |
19 | 18 7 10 | crab | |
20 | 1 3 2 6 19 | cmpo | |
21 | 0 20 | wceq |