girth — Mathlib

English

The girth of a simple graph is the length of its shortest cycle, or 0 if the graph is acyclic.

Русский

Гирт простого графа — длина кратчайшего цикла; 0, если граф ацикличен.

LaTeX

$$$$\mathrm{girth}(G) = 0 \text{ if and only if } G \text{ is acyclic}.$$$$

Lean4

/-- The girth of a simple graph is the length of its smallest cycle, or junk value `0` if the graph is
acyclic.
-/
noncomputable def girth (G : SimpleGraph α) : ℕ :=
  G.egirth.toNat

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