Zulip Chat Archive
Stream: general
Topic: unordered pairs
Kevin Buzzard (Jul 05 2018 at 11:24):
TPIL explains how to construct unordered pairs of terms here: https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#quotients . But is this actually in Lean somewhere?
Kevin Buzzard (Jul 05 2018 at 14:47):
I'll take that as a no and cut and paste Jeremy's code :-)
Last updated: May 02 2025 at 03:31 UTC