instDecidablePredMemSetSupport — Mathlib

English

The predicate x ∈ G.support is decidable, i.e., membership in the support can be determined algorithmically given G.Adj is decidable and V is finite.

Русский

Предикат x ∈ G.support разрешим: принадлежность вершины к поддержке графа может быть определена алгоритмически при заданном G.Adj и конечности V.

LaTeX

$$DecidablePred (\\cdot ∈ G.support)$$

Lean4

instance : DecidablePred (· ∈ G.support) :=
  inferInstanceAs <| DecidablePred (· ∈ {v | ∃ w, G.Adj v w})

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