Skip to content

Cantor の対関数についての証明は出典を示す #802

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Sep 16, 2024
Merged

Cantor の対関数についての証明は出典を示す #802

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
51c4bd6
Cantor の対関数についての証明は出典を示す
Seasawher Sep 15, 2024
b4e8322
Merge branch 'main' into pairing
Seasawher Sep 16, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion Examples/Solution/CantorPairing.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@

だいたいこのようにして一般の集合に拡張された「要素の個数」という概念を、濃度と呼びます。

無限集合の濃度に関しては、様々な興味深い事実が知られています。この演習問題では、自然数 `ℕ` とその直積 `ℕ × ℕ` の濃度が等しいということを Mathlib を使いながら示していきます。
無限集合の濃度に関しては、様々な興味深い事実が知られています。この演習問題では、自然数 `ℕ` とその直積 `ℕ × ℕ` の濃度が等しいということを Mathlib を使いながら示していきます。[^note]

## 問1: sum 関数

Expand Down Expand Up @@ -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) を参考にいたしました。 -/
4 changes: 3 additions & 1 deletion Exercise/CantorPairing.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@

だいたいこのようにして一般の集合に拡張された「要素の個数」という概念を、濃度と呼びます。

無限集合の濃度に関しては、様々な興味深い事実が知られています。この演習問題では、自然数 `ℕ` とその直積 `ℕ × ℕ` の濃度が等しいということを Mathlib を使いながら示していきます。
無限集合の濃度に関しては、様々な興味深い事実が知られています。この演習問題では、自然数 `ℕ` とその直積 `ℕ × ℕ` の濃度が等しいということを Mathlib を使いながら示していきます。[^note]

## 問1: sum 関数

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