From 5305d39a16f7a0771b163353f2e0d435c7d53e96 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Sun, 10 Jul 2022 15:28:34 +0000 Subject: [PATCH] =?UTF-8?q?feat(data/pnat/basic):=20`succ`=20as=20an=20ord?= =?UTF-8?q?er=20isomorphism=20between=20`=E2=84=95`=20and=20`=E2=84=95+`?= =?UTF-8?q?=20(#15183)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Couldn't find this in the library. Asked on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/order.20isomorphism.20between.20.E2.84.95.20and.20.E2.84.95.2B/near/288891689) in case anyone knew of this already. --- src/data/pnat/basic.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/data/pnat/basic.lean b/src/data/pnat/basic.lean index e67d52cbb6f8c..41f3f00d22bac 100644 --- a/src/data/pnat/basic.lean +++ b/src/data/pnat/basic.lean @@ -112,6 +112,14 @@ coe_injective.add_left_cancel_semigroup coe (λ _ _, rfl) instance : add_right_cancel_semigroup ℕ+ := coe_injective.add_right_cancel_semigroup coe (λ _ _, rfl) +/-- The order isomorphism between ℕ and ℕ+ given by `succ`. -/ +@[simps] def succ_order_iso : ℕ ≃o ℕ+ := +{ to_fun := λ n, ⟨_, succ_pos n⟩, + inv_fun := λ n, pred (n : ℕ), + left_inv := pred_succ, + right_inv := λ ⟨x, hx⟩, by simpa using succ_pred_eq_of_pos hx, + map_rel_iff' := @succ_le_succ_iff } + @[priority 10] instance : covariant_class ℕ+ ℕ+ ((+)) (≤) := ⟨by { rintro ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩, simp [←pnat.coe_le_coe] }⟩