English
If adjacency is decidable for G and membership in s is decidable, then adjacency in G.deleteEdges s is decidable.
Русский
Если смежность графа G разрешима и принадлежность в s разрешима, то смежность в G.deleteEdges s разрешима.
LaTeX
$$[DecidableRel G.Adj] ∧ [DecidablePred (· ∈ s)] ∧ [DecidableEq V] ⇒ DecidableRel (G.deleteEdges s).Adj$$
Lean4
instance [DecidableRel G.Adj] [DecidablePred (· ∈ s)] [DecidableEq V] : DecidableRel (G.deleteEdges s).Adj :=
inferInstanceAs <| DecidableRel (G \ fromEdgeSet s).Adj
