induce_connected_of_patches — Mathlib

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

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