Theorems · Definition · order theory

RelSeries.inductionOn

{α : Type u_1} →
  {r : SetRel α α} →
    (motive : RelSeries r → Sort u_3) →
      ((x : α) → motive (RelSeries.singleton r x)) →
        ((p : RelSeries r) → (x : α) → (hx : (x, p.head) ∈ r) → motive p → motive (p.cons x hx)) →
          (p : RelSeries r) → motive p

To show a proposition p for xs : RelSeries r it suffices to show it for all singletons and to show that when p holds for xs it also holds for xs prepended with one element. Note: This can also be used to construct data, but it does not have good definitional properties, since (p.cons x hx).tail _ = p is not a definitional equality.

Defined in

Mathlib.Order.RelSeries

Cited by

3 results in Mathlib

Foundations

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