exists_egirth_eq_length — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem exists_egirth_eq_length : (∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.egirth = w.length) ↔ ¬G.IsAcyclic :=
  by
  refine ⟨?_, fun h ↦ ?_⟩
  · rintro ⟨a, w, hw, _⟩ hG
    exact hG _ hw
  · simp_rw [← egirth_eq_top, ← Ne.eq_def, egirth, iInf_subtype', iInf_sigma', ENat.iInf_coe_ne_top, ← exists_prop,
      Subtype.exists', Sigma.exists', eq_comm] at h ⊢
    exact ciInf_mem _

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