exists_verts_eq_connectedComponentSupp

English

There exists a connected component c of G such that H.verts = c.supp.

Русский

Существует компонента связности графа G с опорой, совпадающей с множеством вершин H.

LaTeX

$$$\exists c : G.ConnectedComponent,\ H.verts = c.supp$$$

Lean4

/-- This lemma establishes a condition under which a subgraph is the same as a connected component.
Note the asymmetry in the hypothesis `h`: `v` is in `H.verts`, but `w` is not required to be.
-/
theorem exists_verts_eq_connectedComponentSupp {H : Subgraph G} (hc : H.Connected)
    (h : ∀ v ∈ H.verts, ∀ w, G.Adj v w → H.Adj v w) : ∃ c : G.ConnectedComponent, H.verts = c.supp :=
  by
  rw [SimpleGraph.ConnectedComponent.exists]
  obtain ⟨v, hv⟩ := hc.nonempty
  use v
  ext w
  simp only [ConnectedComponent.mem_supp_iff, ConnectedComponent.eq]
  exact ⟨fun hw ↦ by simpa using (hc ⟨w, hw⟩ ⟨v, hv⟩).map H.hom, fun a ↦ a.symm.mem_subgraphVerts h hv⟩

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