From 51c4bd639382fcf89d705c69f3085eac1ae93e77 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Mon, 16 Sep 2024 03:24:45 +0900 Subject: [PATCH] =?UTF-8?q?Cantor=20=E3=81=AE=E5=AF=BE=E9=96=A2=E6=95=B0?= =?UTF-8?q?=E3=81=AB=E3=81=A4=E3=81=84=E3=81=A6=E3=81=AE=E8=A8=BC=E6=98=8E?= =?UTF-8?q?=E3=81=AF=E5=87=BA=E5=85=B8=E3=82=92=E7=A4=BA=E3=81=99=20Fixes?= =?UTF-8?q?=20#800?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Examples/Solution/CantorPairing.lean | 4 +++- Exercise/CantorPairing.lean | 4 +++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/Examples/Solution/CantorPairing.lean b/Examples/Solution/CantorPairing.lean index 046c56f0..94109332 100644 --- a/Examples/Solution/CantorPairing.lean +++ b/Examples/Solution/CantorPairing.lean @@ -8,7 +8,7 @@ だいたいこのようにして一般の集合に拡張された「要素の個数」という概念を、濃度と呼びます。 -無限集合の濃度に関しては、様々な興味深い事実が知られています。この演習問題では、自然数 `ℕ` とその直積 `ℕ × ℕ` の濃度が等しいということを Mathlib を使いながら示していきます。 +無限集合の濃度に関しては、様々な興味深い事実が知られています。この演習問題では、自然数 `ℕ` とその直積 `ℕ × ℕ` の濃度が等しいということを Mathlib を使いながら示していきます。[^note] ## 問1: sum 関数 @@ -188,3 +188,5 @@ theorem unpair_pair_eq_id (m n : ℕ) : unpair (pair (m, n)) = (m, n) := by specialize ih m' (n + 1) this simp [unpair, ih] -- sorry + +/- [^note]: 本項での証明を書くにあたって [Cantor の対関数の全単射性の証明](http://iso.2022.jp/math/pairing_function.pdf) を参考にいたしました。 -/ diff --git a/Exercise/CantorPairing.lean b/Exercise/CantorPairing.lean index 5a4794f7..9da84c22 100644 --- a/Exercise/CantorPairing.lean +++ b/Exercise/CantorPairing.lean @@ -8,7 +8,7 @@ だいたいこのようにして一般の集合に拡張された「要素の個数」という概念を、濃度と呼びます。 -無限集合の濃度に関しては、様々な興味深い事実が知られています。この演習問題では、自然数 `ℕ` とその直積 `ℕ × ℕ` の濃度が等しいということを Mathlib を使いながら示していきます。 +無限集合の濃度に関しては、様々な興味深い事実が知られています。この演習問題では、自然数 `ℕ` とその直積 `ℕ × ℕ` の濃度が等しいということを Mathlib を使いながら示していきます。[^note] ## 問1: sum 関数 @@ -152,3 +152,5 @@ theorem unpair_pair_eq_id (m n : ℕ) : unpair (pair (m, n)) = (m, n) := by -- 後は帰納法の仮定から従う。 sorry + +/- [^note]: 本項での証明を書くにあたって [Cantor の対関数の全単射性の証明](http://iso.2022.jp/math/pairing_function.pdf) を参考にいたしました。 -/