instDecidableRelAdjToGraphOfDecidableEq

English

If A is an adjacency matrix for a simple graph, then the corresponding adjacency relation is decidable.

Русский

Если A является матрицей смежности для простого графа, тогда соответствующее отношение смежности разрешимо.

LaTeX

$$$\\\\operatorname{DecidableRel}(h.toGraph.Adj)$$$

Lean4

instance [MulZeroOneClass α] [Nontrivial α] [DecidableEq α] (h : IsAdjMatrix A) : DecidableRel h.toGraph.Adj :=
  by
  simp only [toGraph]
  infer_instance

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