induce_union_connected — Mathlib

English

If the induced subgraphs on two vertex sets s and t are connected, their intersection is nonempty, then the induced subgraph on the union s ∪ t is connected.

Русский

Если подграфа, индукцированные по столбцам s и t, связны, а их пересечение непусто, то подграф индукции по союзу s ∪ t связен.

LaTeX

$$(G.induce s).Connected → (G.induce t).Connected → (s ∩ t).Nonempty → (G.induce (s ∪ t)).Connected$$

Lean4

theorem induce_union_connected {s t : Set V} (sconn : (G.induce s).Connected) (tconn : (G.induce t).Connected)
    (sintert : (s ∩ t).Nonempty) : (G.induce (s ∪ t)).Connected :=
  by
  rw [connected_induce_iff] at sconn tconn ⊢
  exact Subgraph.induce_union_connected sconn tconn sintert

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