diam_anti_of_ediam_ne_top

Mathlib.Combinatorics.SimpleGraph.Diam

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

English

If G ≤ G' and ediam ≠ ⊤, then G'.diam ≤ G.diam.

Русский

Если G ⊆ G' и ediam ≠ ⊤, тогда G'.diam ≤ G.diam.

LaTeX

$$$$ (G \\le G') \\land (G.ediam \\neq \\top) \\Rightarrow G'.diam \\le G.diam $$$$

Lean4

@[gcongr]
theorem diam_anti_of_ediam_ne_top (h : G ≤ G') (hn : G.ediam ≠ ⊤) : G'.diam ≤ G.diam :=
  ENat.toNat_le_toNat (ediam_anti h) hn

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

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

Разделы

Аффилиация

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