English
Let s ⊆ V and u ∈ s. If for every v ∈ s there exists a patch s' ⊆ s containing u and v such that the induced subgraph on s' connects u to v, then the induced subgraph on s is connected.
Русский
Пусть s ⊆ V и u ∈ s. Если для каждого v ∈ s существует подмножество s' ⊆ s, содержащее u и v, такое что в_induced s' есть путь от u до v, то индукцированный подграф по s связан.
LaTeX
$$Let s ⊆ V, u ∈ s, and patches as given, then (G.induce s).Connected$$
Lean4
theorem induce_connected_of_patches {s : Set V} (u : V) (hu : u ∈ s)
(patches : ∀ {v}, v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (G.induce s').Reachable ⟨u, hu'⟩ ⟨v, hv'⟩) :
(G.induce s).Connected := by
rw [connected_iff_exists_forall_reachable]
refine ⟨⟨u, hu⟩, ?_⟩
rintro ⟨v, hv⟩
obtain ⟨sv, svs, hu', hv', uv⟩ := patches hv
exact uv.map (induceHomOfLE _ svs).toHom