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) を参考にいたしました。 -/