decidableMemEdgeSet — Mathlib

English

Let G be a simple graph on V. If the adjacency relation G.Adj is decidable, then the edge membership predicate e ↦ e ∈ G.edgeSet is decidable.

Русский

Пусть G — простой граф над V. Если отношение смежности G.Adj разрешимо, то проверка принадлежности ребра e графу (e ∈ edgeSet) разрешима.

LaTeX

$$$[\\operatorname{DecidableRel}(G\\.\\mathrm{Adj})] \\Rightarrow \\operatorname{DecidablePred}(\\lambda e : \\mathrm{Sym}^2 V, e \\in G\\.\\mathrm{edgeSet})$$$

Lean4

instance decidableMemEdgeSet [DecidableRel G.Adj] : DecidablePred (· ∈ G.edgeSet) :=
  Sym2.fromRel.decidablePred G.symm

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