ediam_eq_top_of_not_preconnected

Mathlib.Combinatorics.SimpleGraph.Diam

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

← MathLib Explorer

English

If G is not preconnected, then ediam equals ⊤.

Русский

Если G не предсвязан, то ediam(G) = ⊤.

LaTeX

$$$ (\\neg G.\\mathrm{Preconnected}) \\Rightarrow G.ediam = \\top $$$

Lean4

theorem ediam_eq_top_of_not_preconnected (h : ¬G.Preconnected) : G.ediam = ⊤ :=
  by
  cases isEmpty_or_nonempty α
  · exfalso
    exact h <| IsEmpty.forall_iff.mpr trivial
  · apply ediam_eq_top_of_not_connected
    rw [connected_iff]
    tauto

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

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

Разделы

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

Аффилиация

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