decidableMemIncidenceSet — Mathlib

English

Assuming decidable equality on V and decidable adjacency, membership in an incidence set is decidable.

Русский

При допустимых предположениях о равенстве вершин и смежности, принадлежность инцидентному множеству разрешима.

LaTeX

$$$[DecidableEq\\ V] \\, [DecidableRel\\ G.Adj] \\Rightarrow \\forall v, DecidablePred (e \\in G.incidenceSet(v))$$$

Lean4

instance decidableMemIncidenceSet [DecidableEq V] [DecidableRel G.Adj] (v : V) : DecidablePred (· ∈ G.incidenceSet v) :=
  inferInstanceAs <| DecidablePred fun e => e ∈ G.edgeSet ∧ v ∈ e

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