connected_top_iff

Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

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

English

The completeGraph on V is connected iff V is nonempty.

Русский

Полный граф на V связан тогда, когда V непусто.

LaTeX

$$$(\mathrm{completeGraph}(V)).Connected \iff \mathrm{Nonempty}(V)$$$

Lean4

theorem connected_top_iff : (completeGraph V).Connected ↔ Nonempty V := by simp [connected_iff]

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

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

Разделы

Аффилиация

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