Commit 2024-09-02 00:34 003d3b4f

View on Github →

feat(Data/List/Change): add forwards induction for List.Chain and List.Chain' (#16346) Moves:

List.Chain.induction -> List.Chain.backwards_induction
List.Chain.induction_head -> List.Chain.backwards_induction_head

Estimated changes

Modified Mathlib/CategoryTheory/ConnectedComponents.lean

Modified Mathlib/Data/List/Chain.lean

added theorem List.Chain'.chain

added theorem List.Chain'.induction

added theorem List.Chain'.iterate_eq_of_apply_eq

added theorem List.Chain.backwards_induction

added theorem List.Chain.backwards_induction_head

deleted theorem List.Chain.induction_head