Theorems · Theorem · combinatorics

SimpleGraph.IsFiveWheelLike.symm

∀ {α : Type u_1} {s : Finset α} {G : SimpleGraph α} {r k : ℕ} [inst : DecidableEq α] {v w₁ w₂ : α} {t : Finset α},
  G.IsFiveWheelLike r k v w₁ w₂ s t → G.IsFiveWheelLike r k v w₂ w₁ t s

Defined in

Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEq