Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-11 06:01 4231b681

View on Github →

feat(data/list): add a few lemmas (#14047)

  • add list.reverse_surjective and list.reverse_bijective;
  • add list.chain_iff_forall₂, list.chain_append_singleton_iff_forall₂, and list.all₂_zip_with.

Estimated changes

added theorem list.reverse_bijective
modified theorem list.reverse_injective
modified theorem list.reverse_involutive
added theorem list.all₂_zip_with