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.

Русский

Вершины из β‑части не смежны друг с другом.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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