connected_iff_forall_exists_walk_subgraph

English

Let G be a simple graph and H a subgraph of G. Then H is connected if and only if its vertex set is nonempty and for any two vertices u and v in H, there exists a walk in G from u to v whose vertex set lies entirely inside H.

Русский

Пусть G — простой граф, а H — подграф G. Тогда H связен тогда и только тогда, когда множество вершин H непусто, и для любых вершин u, v из вершин H существует ход в G от u к v, такой что все вершины прого ходa принадлежат H.

LaTeX

$$$H\text{ Connected} \iff H.verts.Nonempty \land \forall\{u\ v\}, u \in H.verts \to v \in H.verts \to \exists p: G.Walk\,u\,v,\ p.toSubgraph \le H$$$

Lean4

theorem connected_iff_forall_exists_walk_subgraph (H : G.Subgraph) :
    H.Connected ↔ H.verts.Nonempty ∧ ∀ {u v}, u ∈ H.verts → v ∈ H.verts → ∃ p : G.Walk u v, p.toSubgraph ≤ H := by
  rw [H.connected_iff, preconnected_iff_forall_exists_walk_subgraph, and_comm]

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