Closed DyeKuu closed 2 years ago
Note:
Interestingly the natural language statements https://artofproblemsolving.com/wiki/index.php/1996_AIME_Problems/Problem_5 is not specifying the pairwise disjoint condition (another informal ambiguity example).
The other statements often explicitly say the pairwise prop. I here use https://leanprover-community.github.io/mathlib_docs/data/list/defs.html#list.pairwise to opt for a more compact form.
Note:
Interestingly the natural language statements https://artofproblemsolving.com/wiki/index.php/1996_AIME_Problems/Problem_5 is not specifying the pairwise disjoint condition (another informal ambiguity example).
The other statements often explicitly say the pairwise prop. I here use https://leanprover-community.github.io/mathlib_docs/data/list/defs.html#list.pairwise to opt for a more compact form.