ι : Sort ?u.255030
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
v w : ↑(deleteEdges G' s).verts
⊢ SimpleGraph.Adj (Subgraph.coe (deleteEdges G' s)) v w → SimpleGraph.Adj (Subgraph.coe G') v w
ι : Sort ?u.255030
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
⊢ Subgraph.coe (deleteEdges G' s) ≤ Subgraph.coe G'
intro v w
no goals
ι : Sort ?u.255030
V : Type u
W : Type v
G : SimpleGraph V
G' : Subgraph G
s : Set (Sym2 V)
v w : ↑(deleteEdges G' s).verts
⊢ SimpleGraph.Adj (Subgraph.coe (deleteEdges G' s)) v w → SimpleGraph.Adj (Subgraph.coe G') v w
simp (config := { contextual := true })