instDecidableRelAdjFromEdgeSetOfDecidablePredSym2MemSetOfDecidableEq

English

Given s subset of Sym2 V, if there is a DecidablePred for membership in s and V has decidable equality, then the adjacency relation of fromEdgeSet s is decidable.

Русский

Для множества s ⊆ Sym2 V, если есть разрешимое membership в s и для V задано разрешимое равенство, то смежность графа fromEdgeSet s разрешима.

LaTeX

$$$[\\operatorname{DecidablePred}(\\lambda x, x \\in s)] \\, [\\operatorname{DecidableEq} V] \\Rightarrow \\operatorname{DecidableRel}((\\mathrm{fromEdgeSet}(s)).\\mathrm{Adj})$$$

Lean4

instance [DecidablePred (· ∈ s)] [DecidableEq V] : DecidableRel (fromEdgeSet s).Adj :=
  inferInstanceAs <| DecidableRel fun v w ↦ s(v, w) ∈ s ∧ v ≠ w

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