preconnected_bot_iff_subsingleton

English

The bottom graph is preconnected iff the vertex type is subsingleton (has at most one element).

Русский

Пусть же нижний граф предсвязанный тогда и только тогда, когда множество вершин является одиночным (существует не более одной вершины).

LaTeX

$$$(\perp : SimpleGraph V).Preconnected \iff Subsingleton\ V.$$$

Lean4

theorem preconnected_bot_iff_subsingleton : (⊥ : SimpleGraph V).Preconnected ↔ Subsingleton V :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ by simpa [subsingleton_iff, ← reachable_bot] using h⟩
  contrapose! h
  simp [nontrivial_iff.mp h, Preconnected, reachable_bot]

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