connected_induce_iff — Mathlib

English

For any subset s of vertices, the connectivity of the induced subgraph G.induce s is the same as the connectivity of the induced subgraph of the top subgraph restricted to s.

Русский

Для любой подмножества вершин s связность индукцированного подграфа G.induce s равна связности индукцированного подграфа сверху, полученного на ограничении до s.

LaTeX

$$$ (G.induce\ s).Connected \iff ((\top : G.Subgraph).induce\ s).Connected $$$

Lean4

theorem connected_induce_iff {s : Set V} : (G.induce s).Connected ↔ ((⊤ : G.Subgraph).induce s).Connected := by
  rw [induce_eq_coe_induce_top, ← Subgraph.connected_iff']

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