not_farFromTriangleFree

Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

URI: https://scilib.ai/kg/mathlib#SimpleGraph.CliqueFree.not_farFromTriangleFree

English

If a graph is far from triangle-free, then its 3-clique set is nonempty.

Русский

Если граф далёк от треугольников, множество 3‑клик не пусто.

LaTeX

$$G.FarFromTriangleFree ε → (G.cliqueFinset 3).Nonempty$$

Lean4

theorem not_farFromTriangleFree (hG : G.CliqueFree 3) (hε : 0 < ε) : ¬G.FarFromTriangleFree ε := fun h =>
  (h.nonpos hG).not_gt hε

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

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

Разделы

Аффилиация

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