egirth_le_length — Mathlib

English

Let G be a simple graph. For every cycle w in G, the girth of G is at most the length of w.

Русский

Пусть G — простой граф. Для любого цикла w на графе G верно: минимальная длина цикла графа ≤ длина w.

LaTeX

$$$$\forall G:\text{SimpleGraph }\alpha,\ \forall a:\alpha,\forall w:\, G.Walk a a,\ w.IsCycle\Rightarrow \text{girth}(G) \le w.length.$$$$

Lean4

theorem egirth_le_length {a} {w : G.Walk a a} (h : w.IsCycle) : G.egirth ≤ w.length :=
  le_egirth.mp le_rfl a w h

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