Theorems · Theorem · combinatorics

SimpleGraph.induce_connected_of_patches

∀ {V : Type u} {G : SimpleGraph V} {s : Set V},
  ∀ u ∈ s,
    (∀ {v : V},
        v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (SimpleGraph.induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩) →
      (SimpleGraph.induce s G).Connected

Defined in

Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Cited by

2 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound