Theorem: SimpleGraph.degree_eq_zero_iff (ExponentialRamsey/Prereq/Mathlib/Combinatorics/SimpleGraph/Basic.lean)

State before:
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
Tactic:
rw [← not_exists, ← degree_pos_iff_exists_adj, not_lt, le_zero_iff]
State after:
no goals