three_le_egirth — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem three_le_egirth : 3 ≤ G.egirth := by
  by_cases h : G.IsAcyclic
  · rw [← egirth_eq_top] at h
    rw [h]
    apply le_top
  · rw [← exists_egirth_eq_length] at h
    have ⟨_, _, _⟩ := h
    simp_all only [Nat.cast_inj, Nat.ofNat_le_cast, Walk.IsCycle.three_le_length]

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