Commit 2025-05-19 08:29 06a7c060

View on Github →

chore(Order/RelSeries): induction principle for RelSeries (#22299) Adds many small API lemmas for the transition between List and RelSeries and an induction principle. Currently, the induction principle is only really useful for proofs, but with a more ambitious refactor of the basic definitions, it could also be used to construct data. Co-authored by: Sihan Su ssh@stu.pku.edu.cn Co-authored by: Yi Song sif4delta0@mail.ustc.edu.cn

Estimated changes

Modified Mathlib/Data/List/Chain.lean

added theorem List.Chain'.cons_of_ne_nil

Modified Mathlib/Order/RelSeries.lean

added theorem RelSeries.append_assoc

added theorem RelSeries.append_cons

added theorem RelSeries.append_singleton_left

added theorem RelSeries.apply_zero

added theorem RelSeries.cons_self_tail

added theorem RelSeries.fromListChain'_cons

added theorem RelSeries.getLast_toList

added theorem RelSeries.head_fromListChain'

added theorem RelSeries.head_toList

added def RelSeries.inductionOn'

added def RelSeries.inductionOn

added theorem RelSeries.snoc_self_eraseLast

added theorem RelSeries.tail_cons

added theorem RelSeries.toList_append

added theorem RelSeries.toList_cons

added theorem RelSeries.toList_eraseLast

added theorem RelSeries.toList_fromListChain'

added theorem RelSeries.toList_getElem_eq_apply

added theorem RelSeries.toList_getElem_eq_apply_of_lt_length

added theorem RelSeries.toList_getElem_zero_eq_head

added theorem RelSeries.toList_singleton

added theorem RelSeries.toList_snoc

added theorem RelSeries.toList_tail