Commit 2022-04-10 06:10 36fceb91

View on Github →

feat(data/list/cycle): Define cycle.chain analog to list.chain (#12970) We define cycle.chain, which means that a relation holds in all adjacent elements in a cyclic list. We then show that for r a transitive relation, cycle.chain r l is equivalent to r holding for all pairs of elements in l.

Estimated changes

Modified src/data/list/cycle.lean

added theorem cycle.chain.nil

added def cycle.chain

added theorem cycle.chain_coe_cons

added theorem cycle.chain_iff_pairwise

added theorem cycle.chain_map

added theorem cycle.chain_ne_nil

added theorem cycle.chain_of_pairwise

added theorem cycle.chain_singleton

added theorem cycle.coe_cons_eq_coe_append

added theorem cycle.coe_to_finset

added theorem cycle.forall_eq_of_chain