English
If G is preconnected and t is a nonempty finite set of vertices, there exists a finite superset t' ⊇ t such that the induced subgraph on t' is connected.
Русский
Если G предварительно связен, и t — непустое конечное множество вершин, то существует конечное надмножество t' ⊇ t такое, что G.induce t' связано.
LaTeX
$$G.Preconnected → t.Nonempty → ∃ t' : Finset V, t ⊆ t' ∧ (G.induce t'.toSet).Connected$$
Lean4
theorem extend_finset_to_connected (Gpc : G.Preconnected) {t : Finset V} (tn : t.Nonempty) :
∃ (t' : Finset V), t ⊆ t' ∧ (G.induce (t' : Set V)).Connected := by
classical
obtain ⟨u, ut⟩ := tn
refine ⟨t.biUnion (fun v => (Gpc u v).some.support.toFinset), fun v vt => ?_, ?_⟩
· simp only [Finset.mem_biUnion, List.mem_toFinset]
exact ⟨v, vt, Walk.end_mem_support _⟩
· apply G.induce_connected_of_patches u
· simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset, Set.mem_iUnion, Set.mem_setOf_eq,
Walk.start_mem_support, exists_prop, and_true]
exact ⟨u, ut⟩
intro v hv
simp only [Finset.mem_coe, Finset.mem_biUnion, List.mem_toFinset] at hv
obtain ⟨w, wt, hw⟩ := hv
refine ⟨{x | x ∈ (Gpc u w).some.support}, ?_, ?_⟩
· simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset]
exact fun x xw => Set.mem_iUnion₂.mpr ⟨w, wt, xw⟩
· simp only [Set.mem_setOf_eq, Walk.start_mem_support, exists_true_left]
refine ⟨hw, Walk.connected_induce_support _ _ _⟩
