Theorems · Theorem · combinatorics

Cycle.induction_on

∀ {α : Type u_1} {motive : Cycle α → Prop} (s : Cycle α),
  motive Cycle.nil → (∀ (a : α) (l : List α), motive ↑l → motive ↑(a :: l)) → motive s

An induction principle for Cycle. Use as induction s.

Defined in

Mathlib.Data.List.Cycle

Cited by

4 results in Mathlib

Foundations

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