preconnected_top

Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

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

English

For any vertex set V, the top simple graph on V is Preconnected.

Русский

Для любого множества вершин V верхний простой граф на V является предсвязанным.

LaTeX

$$$\forall V,\ (\top : \mathrm{SimpleGraph}(V)).Preconnected$$$

Lean4

@[simp]
theorem preconnected_top : (⊤ : SimpleGraph V).Preconnected := fun x y => by
  if h : x = y then rw [h] else exact Adj.reachable h

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

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

Разделы

Аффилиация

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