not_preconnected_bot — Mathlib

English

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

Русский

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

LaTeX

$$$[\text{Nontrivial}(V)] \Rightarrow \neg (\perp_{\mathrm{SimpleGraph}(V)}).Preconnected$$$

Lean4

theorem not_preconnected_bot [Nontrivial V] : ¬(⊥ : SimpleGraph V).Preconnected :=
  preconnected_bot_iff_subsingleton.not.mpr <| not_subsingleton_iff_nontrivial.mpr ‹_›

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