instDecidableRelAdj — Mathlib

English

The Turán graph (turanGraph n r) has a decidable edge relation, i.e., whether two vertices are adjacent can be decided.

Русский

У графа Турэна отношение смежности между двумя вершинами разрешимо определить.

LaTeX

$$$\text{DecidableRel}((\mathrm{turanGraph}\, n\, r).\mathrm{Adj}).$$$

Lean4

instance instDecidableRelAdj : DecidableRel (turanGraph n r).Adj := by dsimp only [turanGraph]; infer_instance

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