Commit 2022-04-26 13:36 3d5e5ee1

View on Github →

feat(data/list/*): Miscellaneous lemmas (#13577) A few lemmas about list.chain, list.pairwise. Also rename list.chain_of_pairwise to list.pairwise.chain for dot notation.

Estimated changes

Modified src/data/list/basic.lean

added theorem list.set_of_mem_cons

Modified src/data/list/chain.lean

deleted theorem list.chain_of_pairwise

Modified src/data/list/cycle.lean

Modified src/data/list/pairwise.lean

added theorem list.pairwise.forall_of_forall_of_flip

Modified src/logic/basic.lean

added theorem congr_fun₂

added theorem congr_fun₃

added theorem funext₂

added theorem funext₃

Modified src/logic/relation.lean

added theorem flip_eq_iff

added theorem swap_eq_iff

added theorem symmetric.flip_eq

added theorem symmetric.swap_eq