Commit 2026-07-02 11:53 52b549a2

View on Github →

feat(Data/List/Chain): generalize WellFounded.asymmetric₃ to chains (#36922) The existing WellFounded.asymmetric shows r a b → ¬r b a, and WellFounded.asymmetric₃ shows r a b → r b c → ¬r c a. This adds WellFounded.asymmetricₙ which shows l.IsChain r → ¬r l.getLast l.head.

Estimated changes

Modified Mathlib/Data/List/Chain.lean

added theorem List.IsChain.rel_getLast_dropLast

added theorem List.IsChain.rel_getLast_head_of_append

deleted theorem List.IsChain.rel_head

added theorem WellFounded.asymmetricₙ

added theorem WellFounded.listPairwise_reverse_compl

added theorem WellFoundedRelation.asymmetricₙ

Modified Mathlib/Data/List/Pairwise.lean

added theorem List.pairwise_iff_forall_infix