English
If two induced subgraphs on sets s and t are connected and there is an edge between a vertex in s and a vertex in t, then the induced subgraph on s ∪ t is connected.
Русский
Если подграфы индукции по s и по t связны и существует ребро между вершиной из s и вершиной из t, то индукция по s ∪ t связна.
LaTeX
$$(G.induce s).Connected → (G.induce t).Connected → v ∈ s → w ∈ t → G.Adj v w → (G.induce (s ∪ t)).Connected$$
Lean4
theorem induce_connected_adj_union {v w : V} {s t : Set V} (sconn : (G.induce s).Connected)
(tconn : (G.induce t).Connected) (hv : v ∈ s) (hw : w ∈ t) (ha : G.Adj v w) : (G.induce (s ∪ t)).Connected :=
by
rw [connected_induce_iff] at sconn tconn ⊢
apply (sconn.adj_union tconn hv hw ha).mono
· simp only [sup_le_iff, Subgraph.le_induce_union_left, Subgraph.le_induce_union_right, and_true,
← Subgraph.subgraphOfAdj_eq_induce ha]
apply subgraphOfAdj_le_of_adj
simp [hv, hw, ha]
· simp only [Subgraph.verts_sup, Subgraph.induce_verts]
rw [Set.union_assoc]
simp [Set.insert_subset_iff, Set.singleton_subset_iff, hv, hw]
