Theorems · Theorem · combinatorics

SimpleGraph.Connected.induce_compl_singleton_of_degree_eq_one

∀ {V : Type u_1} {G : SimpleGraph V},
  G.Connected → ∀ {v : V} [inst : Fintype ↑(G.neighborSet v)], G.degree v = 1 → (SimpleGraph.induce {v}ᶜ G).Connected

The graph resulting from removing a vertex of degree one from a connected graph is connected.

Defined in

Mathlib.Combinatorics.SimpleGraph.Acyclic

Cited by

1 results in Mathlib

Foundations

Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fintype