From 41fa32b3ff6ebcdda51cd66da6dd8b71a0f4a0ac Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Tue, 30 Nov 2021 13:24:44 +0000 Subject: [PATCH] feat(data/nat/pairing): add an `equiv` version of `nat.mkpair`/`nat.unpair` (#10520) --- src/data/nat/pairing.lean | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/data/nat/pairing.lean b/src/data/nat/pairing.lean index f9ffbe624e911..e0fb1acdaf1c9 100644 --- a/src/data/nat/pairing.lean +++ b/src/data/nat/pairing.lean @@ -63,8 +63,15 @@ begin simp [unpair, ae, nat.not_lt_zero, add_assoc] } end +/-- An equivalence between `ℕ × ℕ` and `ℕ`. -/ +@[simps { fully_applied := ff }] def mkpair_equiv : ℕ × ℕ ≃ ℕ := +⟨uncurry mkpair, unpair, λ ⟨a, b⟩, unpair_mkpair a b, mkpair_unpair⟩ + lemma surjective_unpair : surjective unpair := -λ ⟨m, n⟩, ⟨mkpair m n, unpair_mkpair m n⟩ +mkpair_equiv.symm.surjective + +@[simp] lemma mkpair_eq_mkpair {a b c d : ℕ} : mkpair a b = mkpair c d ↔ a = c ∧ b = d := +mkpair_equiv.injective.eq_iff.trans (@prod.ext_iff ℕ ℕ (a, b) (c, d)) theorem unpair_lt {n : ℕ} (n1 : 1 ≤ n) : (unpair n).1 < n := let s := sqrt n in begin