ediam_anti

Mathlib.Combinatorics.SimpleGraph.Diam

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

English

If G is a subgraph of G' (G ≤ G'), then the extended diameter is nonincreasing: ediam(G') ≤ ediam(G).

Русский

Если G является подграфом G' (G ≤ G'), то расширенный диаметр не возрастает: ediam(G') ≤ ediam(G).

LaTeX

$$$$ G \\le G' \\Rightarrow G'.ediam \\le G.ediam $$$$

Lean4

@[gcongr]
theorem ediam_anti (h : G ≤ G') : G'.ediam ≤ G.ediam :=
  iSup₂_mono fun _ _ ↦ edist_anti h

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

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

Разделы

Аффилиация

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