three_le_girth

Mathlib.Combinatorics.SimpleGraph.Girth

URI: https://scilib.ai/kg/mathlib#SimpleGraph.three_le_girth

English

If G is not acyclic, then the girth is at least 3.

Русский

Если граф не ацикличен, то гирит не меньше 3.

LaTeX

$$$$3 \le \mathrm{girth}(G).$$$$

Lean4

theorem three_le_girth (hG : ¬G.IsAcyclic) : 3 ≤ G.girth :=
  ENat.toNat_le_toNat three_le_egirth <| egirth_eq_top.not.mpr hG

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

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

Разделы

Аффилиация

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