instDecidableRel_deleteVerts_adj — Mathlib

English

If adjacency in G is decidable, then adjacency in the top-subgraph after deletion is decidable. More precisely, there is a computable decision procedure for whether (⊤ : G.Subgraph).deleteVerts u has an edge between x and y.

Русский

Если смежность в G разрешима, то и смежность в верхнем подграфе после удаления разрешима. Более точно, существует алгоритм решения, имеет ли (⊤ : G.Subgraph).deleteVerts u ребро между x и y.

LaTeX

$$$ \text{DecidableRel}((\top : G.Subgraph).deleteVerts u).coe.Adj $$$

Lean4

instance instDecidableRel_deleteVerts_adj (u : Set V) [r : DecidableRel G.Adj] :
    DecidableRel ((⊤ : G.Subgraph).deleteVerts u).coe.Adj := fun x y =>
  if h : G.Adj x y then
    .isTrue <| SimpleGraph.Subgraph.Adj.coe <| Subgraph.deleteVerts_adj.mpr ⟨by trivial, x.2.2, by trivial, y.2.2, h⟩
  else .isFalse <| fun hadj ↦ h <| Subgraph.coe_adj_sub _ _ _ hadj

Похожие утверждения