no goals
ι : Sort ?u.269390
𝕜 : Type ?u.269393
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
inst✝ : Fintype ↑(neighborSet G v)
⊢ 0 < degree G v ↔ ∃ w, Adj G v w
simp only [degree, card_pos, Finset.Nonempty, mem_neighborFinset]