not_connected_bot

Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

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

English

If V is nontrivial, then the bottom SimpleGraph on V is not connected.

Русский

Если V ненулевой, то нижний граф на V не является связанным.

LaTeX

$$$[\text{Nontrivial}(V)] : \neg (\perp : \mathrm{SimpleGraph}(V)).Connected$$$

Lean4

theorem not_connected_bot [Nontrivial V] : ¬(⊥ : SimpleGraph V).Connected := by
  simp [not_preconnected_bot, connected_iff]

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

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

Разделы

Аффилиация

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