mathlib3
4b05a42d - feat(data/list/pairwise): `pairwise_of_forall_mem_list` (#12968)

Commit
3 years ago
feat(data/list/pairwise): `pairwise_of_forall_mem_list` (#12968) A relation holds pairwise on a list when it does on any two of its elements.
Author
Parents
Loading