case a
ι : Sort ?u.165735
𝕜 : Type ?u.165738
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 (Sym2 V)
inst✝² : DecidableEq V
inst✝¹ : DecidableRel G.Adj
s : Finset (Sym2 V)
inst✝ : DecidableRel (deleteEdges G ↑s).Adj
e : Sym2 V
⊢ e ∈ edgeFinset (deleteEdges G ↑s) ↔ e ∈ edgeFinset G \ s
ι : Sort ?u.165735
𝕜 : Type ?u.165738
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 (Sym2 V)
inst✝² : DecidableEq V
inst✝¹ : DecidableRel G.Adj
s : Finset (Sym2 V)
inst✝ : DecidableRel (deleteEdges G ↑s).Adj
⊢ edgeFinset (deleteEdges G ↑s) = edgeFinset G \ s
ext e
no goals
case a
ι : Sort ?u.165735
𝕜 : Type ?u.165738
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 (Sym2 V)
inst✝² : DecidableEq V
inst✝¹ : DecidableRel G.Adj
s : Finset (Sym2 V)
inst✝ : DecidableRel (deleteEdges G ↑s).Adj
e : Sym2 V
⊢ e ∈ edgeFinset (deleteEdges G ↑s) ↔ e ∈ edgeFinset G \ s
simp [edgeSet_deleteEdges]