Theorem: SimpleGraph.edgeSet_eq_empty_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
G : SimpleGraph V
⊢ edgeSet G = ∅ ↔ G = ⊥
Tactic:
rw [← edgeSet_bot, edgeSet_inj]
State after:
no goals