rw [← not_exists, ← degree_pos_iff_exists_adj, not_lt, le_zero_iff]
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
v : V
inst✝ : Fintype ↑(neighborSet G v)
⊢ degree G v = 0 ↔ ∀ (w : V), ¬Adj G v w
no goals