top_induce_pair_connected_of_adj — Mathlib

English

There exists a connected component of G whose support equals H.verts, under suitable hypotheses; i.e., H.verts equals the support of some connected component of G.

Русский

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

LaTeX

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

Lean4

theorem top_induce_pair_connected_of_adj {u v : V} (huv : G.Adj u v) : ((⊤ : G.Subgraph).induce { u, v }).Connected :=
  by
  rw [← subgraphOfAdj_eq_induce huv]
  exact subgraphOfAdj_connected huv

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