memDecidable — Mathlib

English

If the adjacency relation is decidable, then membership in the neighbor set of any vertex is decidable.

Русский

Если отношение смежности решаемо, то принадлежность вершке v множеству соседей разрешима (решаема).

LaTeX

$$$$ (\forall v:V, DecidablePred (\cdot \in G.neighborSet(v))) $$$$

Lean4

instance memDecidable (v : V) [DecidableRel G.Adj] : DecidablePred (· ∈ G.neighborSet v) :=
  inferInstanceAs <| DecidablePred (Adj G v)

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