case Adj.h.h.a
ι : Sort ?u.159844
𝕜 : Type ?u.159847
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
s : Set (Sym2 V)
x✝¹ x✝ : V
⊢ Adj (deleteEdges G s) x✝¹ x✝ ↔ Adj (deleteEdges G (s ∩ edgeSet G)) x✝¹ x✝
ι : Sort ?u.159844
𝕜 : Type ?u.159847
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
s : Set (Sym2 V)
⊢ deleteEdges G s = deleteEdges G (s ∩ edgeSet G)
ext
no goals
case Adj.h.h.a
ι : Sort ?u.159844
𝕜 : Type ?u.159847
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
s : Set (Sym2 V)
x✝¹ x✝ : V
⊢ Adj (deleteEdges G s) x✝¹ x✝ ↔ Adj (deleteEdges G (s ∩ edgeSet G)) x✝¹ x✝
simp (config := { contextual := true }) [imp_false]