girth_eq_zero

Mathlib.Combinatorics.SimpleGraph.Girth

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

English

girth(G) = 0 iff G is acyclic.

Русский

girth(G) = 0 эквивалентно тому, что G ацикличен.

LaTeX

$$$$\mathrm{girth}(G) = 0 \iff G.IsAcyclic.$$$$

Lean4

theorem girth_eq_zero : G.girth = 0 ↔ G.IsAcyclic :=
  ⟨fun h ↦ not_not.mp <| three_le_girth.mt <| by cutsat, fun h ↦ by simp [girth, h]⟩

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

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

Разделы

Аффилиация

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