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 c,c'\\;\\neg((graph\\ t).Adj(\\mathrm{in}_2 c)(\\mathrm{in}_2 c')).$$$

Lean4

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

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

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

Разделы

Аффилиация

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