Theorems · Theorem · combinatorics

SimpleGraph.IsCycles.snd_of_mem_support_of_isPath_of_adj

∀ {V : Type u_1} {G : SimpleGraph V} [Finite V] {v w w' : V},
  G.IsCycles → ∀ (p : G.Walk v w), w ≠ w' → w' ∈ p.support → p.IsPath → G.Adj v w' → p.snd = w'

Defined in

Mathlib.Combinatorics.SimpleGraph.Matching

Cited by

0 results in Mathlib

Foundations

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

Assumes

Finite