English
Let S be a nonempty family of vertex subsets with pairwise intersecting members. If each induced subgraph G.induce s is connected for s ∈ S, then the induced subgraph on the union of S is connected.
Русский
Пусть S — непустое семейство подмножеств вершин, члены которого попарно пересекаются. Если для каждого s ∈ S индукцированный подграф G.induce s связан, то индукция по ⋃S связна.
LaTeX
$$S.Nonempty → (∀ {s t}, s ∈ S → t ∈ S → (s ∩ t).Nonempty) → (∀ {s}, s ∈ S → (G.induce s).Connected) → (G.induce S.sUnion).Connected$$
Lean4
theorem induce_sUnion_connected_of_pairwise_not_disjoint {S : Set (Set V)} (Sn : S.Nonempty)
(Snd : ∀ {s t}, s ∈ S → t ∈ S → (s ∩ t).Nonempty) (Sc : ∀ {s}, s ∈ S → (G.induce s).Connected) :
(G.induce (⋃₀ S)).Connected := by
obtain ⟨s, sS⟩ := Sn
obtain ⟨v, vs⟩ := (Sc sS).nonempty
apply G.induce_connected_of_patches _ (Set.subset_sUnion_of_mem sS vs)
rintro w hw
simp only [Set.mem_sUnion] at hw
obtain ⟨t, tS, wt⟩ := hw
refine
⟨s ∪ t, Set.union_subset (Set.subset_sUnion_of_mem sS) (Set.subset_sUnion_of_mem tS), Or.inl vs, Or.inr wt,
induce_union_connected (Sc sS) (Sc tS) (Snd sS tS) _ _⟩
