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: Dec 20 2023 at 11:08 UTC