subsingleton_connectedComponent — Mathlib

English

If G is preconnected, then its connected component is a singleton (all vertices lie in the same connected component).

Русский

Если граф G предсоединён, то его компонента связности единична, т.е. все вершины лежат в одной компоненте связности.

LaTeX

$$G.Preconnected \Rightarrow Subsingleton G.ConnectedComponent$$

Lean4

theorem _root_.SimpleGraph.Preconnected.subsingleton_connectedComponent (h : G.Preconnected) :
    Subsingleton G.ConnectedComponent :=
  ⟨ConnectedComponent.ind₂ fun v w => ConnectedComponent.sound (h v w)⟩

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