Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Graph theory (extension)
Closed neighborhood of a vertex
clnbgrn0
Next ⟩
clnbupgr
Metamath Proof Explorer
Ascii
Unicode
Theorem
clnbgrn0
Description:
The closed neighborhood of a vertex is never empty.
(Contributed by
AV
, 16-May-2025)
Ref
Expression
Hypothesis
clnbgrn0.v
⊢
V
=
Vtx
⁡
G
Assertion
clnbgrn0
⊢
N
∈
V
→
G
ClNeighbVtx
N
≠
∅
Proof
Step
Hyp
Ref
Expression
1
clnbgrn0.v
⊢
V
=
Vtx
⁡
G
2
1
clnbgrvtxel
⊢
N
∈
V
→
N
∈
G
ClNeighbVtx
N
3
ne0i
⊢
N
∈
G
ClNeighbVtx
N
→
G
ClNeighbVtx
N
≠
∅
4
2
3
syl
⊢
N
∈
V
→
G
ClNeighbVtx
N
≠
∅