girth_le_length

Mathlib.Combinatorics.SimpleGraph.Girth

URI: https://scilib.ai/kg/mathlib#SimpleGraph.girth_le_length

← MathLib Explorer

English

The natural girth equals the natural part of the ENat girth.

Русский

Натуральная гирит равна натуральной части ENat-гирит.

LaTeX

$$$$\mathrm{girth}(G) = \operatorname{toNat}(\mathrm{egirth}(G)).$$$$

Lean4

theorem girth_le_length {a} {w : G.Walk a a} (h : w.IsCycle) : G.girth ≤ w.length :=
  ENat.coe_le_coe.mp <| G.egirth.coe_toNat_le_self.trans <| egirth_le_length h

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru