nonempty

Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Subgraph.Connected.nonempty

English

If H is connected, then its vertex set is nonempty.

Русский

Если подграф H связан, то множество вершин непусто.

LaTeX

$$$\forall H : G{\text Subgraph},\ H.Connected \Rightarrow H.verts.Nonempty$$$

Lean4

protected theorem nonempty {H : G.Subgraph} (h : H.Connected) : H.verts.Nonempty := by rw [H.connected_iff] at h;
  exact h.2

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

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

Разделы

Аффилиация

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