Commit 2026-10-17 11:31 9d4de8d8

View on Github →

feat(Data/List): add List.IsChain.iterate and List.getLast_iterate (#44661) Add two basic lemmas about List.iterate:

  • List.IsChain.iterate: if r a (f a) holds for every a, then List.iterate f a n is an r-chain.
  • List.getLast_iterate (@[simp]): the last element of a nonempty List.iterate f a n is f^[n - 1] a, complementing the existing getElem_iterate.

Estimated changes

added theorem List.getLast_iterate