egirth_anti

Mathlib.Combinatorics.SimpleGraph.Girth

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

← MathLib Explorer

English

If G is a subgraph of G', then the girth of G' is at most the girth of G.

Русский

Если G является подграфом G', то гирит(G') ≤ гирит(G).

LaTeX

$$$$G \le H \Rightarrow \mathrm{girth}(H) \le \mathrm{girth}(G).$$$$

Lean4

theorem egirth_anti : Antitone (egirth : SimpleGraph α → ℕ∞) := fun G H h ↦
  iInf_mono fun a ↦ iInf₂_mono' fun w hw ↦ ⟨w.mapLe h, hw.mapLe _, by simp⟩

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

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

Разделы

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

Аффилиация

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