diam_def

Mathlib.Combinatorics.SimpleGraph.Diam

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

English

Diameter equals the Natified supremum of extended distances: diam(G) = toNat(sup_{p} edist p.1 p.2).

Русский

Диаметр графа равен toNat( sup_{p} edist p.1 p.2 ).

LaTeX

$$$$ G.diam = \\operatorname{toNat}\\left( \\sup_{p \\in \\alpha \\times \\alpha} G.edist(p.1,p.2) \\right) $$$$

Lean4

theorem diam_def : G.diam = (⨆ p : α × α, G.edist p.1 p.2).toNat := by rw [diam, ediam_def]

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

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

Разделы

Аффилиация

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