decidableMemCommonNeighbors — Mathlib

English

There is a decidable predicate for membership in G.commonNeighbors v w given decidable Rel G.Adj.

Русский

Существует разрешимое предикат для принадлежности в G.commonNeighbors(v,w) при условии разрешимой relation G.Adj.

LaTeX

$$$[DecidableRel G.Adj] \\Rightarrow [DecidablePred (e \\in G.commonNeighbors(v,w))]$$$

Lean4

instance decidableMemCommonNeighbors [DecidableRel G.Adj] (v w : V) : DecidablePred (· ∈ G.commonNeighbors v w) :=
  inferInstanceAs <| DecidablePred fun u => u ∈ G.neighborSet v ∧ u ∈ G.neighborSet w

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