girth_bot

Mathlib.Combinatorics.SimpleGraph.Girth

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

English

The girth of the bottom (empty) graph is 0.

Русский

Гирит нижнего (пустого) графа равен 0.

LaTeX

$$$$\mathrm{girth}(⊥) = 0.$$$$

Lean4

@[simp]
theorem girth_bot : girth (⊥ : SimpleGraph α) = 0 := by simp [girth]

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

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

Разделы

Аффилиация

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