preconnected_iff_forall_exists_walk_subgraph

English

A subgraph H is preconnected iff for every pair of vertices in H, there exists a walk in G whose subgraph is contained in H and connects them.

Русский

Пусть подграф H предсвязан тогда и только тогда, когда для любых вершин в H существует ход в G, обход которого лежит внутри H и соединяет их.

LaTeX

$$$ H.Preconnected \iff \forall {u v}, u \in H.verts \to v \in H.verts \to \exists p : G.Walk u v, p.toSubgraph ≤ H $$$

Lean4

theorem preconnected_iff_forall_exists_walk_subgraph (H : G.Subgraph) :
    H.Preconnected ↔ ∀ {u v}, u ∈ H.verts → v ∈ H.verts → ∃ p : G.Walk u v, p.toSubgraph ≤ H :=
  by
  constructor
  · intro hc u v hu hv
    refine (hc ⟨_, hu⟩ ⟨_, hv⟩).elim fun p => ?_
    exists p.map (Subgraph.hom _)
    simp [coeSubgraph_le]
  · intro hw
    rw [Subgraph.preconnected_iff]
    rintro ⟨u, hu⟩ ⟨v, hv⟩
    obtain ⟨p, h⟩ := hw hu hv
    exact
      Reachable.map (Subgraph.inclusion h)
        (p.toSubgraph_connected ⟨_, p.start_mem_verts_toSubgraph⟩ ⟨_, p.end_mem_verts_toSubgraph⟩)

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