Theorem: Digraph.edgeSet_bot (GraphProjects/Digraph.lean)

State before:
ι : Sort ?u.51631
𝕜 : Type ?u.51634
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
G₁ G₂ : Digraph V
⊢ edgeSet ⊥ = ∅
Tactic:
rw [Set.eq_empty_iff_forall_not_mem]
State after:
ι : Sort ?u.51631
𝕜 : Type ?u.51634
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
G₁ G₂ : Digraph V
⊢ ∀ (x : V × V), ¬x ∈ edgeSet ⊥

State before:
ι : Sort ?u.51631
𝕜 : Type ?u.51634
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
G₁ G₂ : Digraph V
⊢ ∀ (x : V × V), ¬x ∈ edgeSet ⊥
Tactic:
simp
State after:
no goals