case Adj.h.h.a
ι : Sort ?u.161200
𝕜 : Type ?u.161203
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
H : SimpleGraph V
h : H ≤ G
v w : V
⊢ Adj (deleteEdges G (edgeSet G \ edgeSet H)) v w ↔ Adj H v w
ι : Sort ?u.161200
𝕜 : Type ?u.161203
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
H : SimpleGraph V
h : H ≤ G
⊢ deleteEdges G (edgeSet G \ edgeSet H) = H
ext (v w)
no goals
case Adj.h.h.a
ι : Sort ?u.161200
𝕜 : Type ?u.161203
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
H : SimpleGraph V
h : H ≤ G
v w : V
⊢ Adj (deleteEdges G (edgeSet G \ edgeSet H)) v w ↔ Adj H v w
constructor <;> simp (config := { contextual := true }) [@h v w]