not_in₀₀

Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

URI: https://scilib.ai/kg/mathlib#SimpleGraph.TripartiteFromTriangles.Graph.not_in₀₀

English

Vertices from the α-part are never adjacent to each other in the tripartite-from-triangles graph.

Русский

Вершины из α‑части никогда не смежны друг с другом в графе, построенном из треугольников.

LaTeX

$$$\\forall a,a'\\;\\neg((graph\\ t).Adj(\\mathrm{in}_0 a)(\\mathrm{in}_0 a')).$$$

Lean4

@[simp]
theorem not_in₀₀ : ¬(graph t).Adj (in₀ a) (in₀ a') := fun h ↦ nomatch h

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

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

Разделы

Аффилиация

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