instDecidableRelR

Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

URI: https://scilib.ai/kg/mathlib#SimpleGraph.IsTuranMaximal.instDecidableRelR

English

There is a decidable relation on the setoid induced by non-adjacency in a Turán-maximal graph.

Русский

Существует разрешимое отношение на множество классов по не-смежности в графе Турэна.

LaTeX

$$$\text{DecidableRel } (h. setoid.r).$$$

Lean4

instance : DecidableRel h.setoid.r :=
  inferInstanceAs <| DecidableRel (¬G.Adj · ·)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru