exists_girth_eq_length — Mathlib

English

There exists a cycle realizing the girth if and only if the graph is not acyclic.

Русский

Существует цикл, достигающий гирит графа, тогда и только тогда, когда граф не ацикличен.

LaTeX

$$$$\exists a\exists w\ (w.IsCycle \land G.girth = w.length) \iff \neg G.IsAcyclic.$$$$

Lean4

theorem exists_girth_eq_length : (∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.girth = w.length) ↔ ¬G.IsAcyclic :=
  by
  refine ⟨by tauto, fun h ↦ ?_⟩
  obtain ⟨_, _, _⟩ := exists_egirth_eq_length.mpr h
  simp_all only [girth, ENat.toNat_coe]
  tauto

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