Dowód, że każdy skończony ciąg liczb wymiernych da się zakodować jedną liczbą naturalną
Wojciech Karpiel
32f9a36675
eksperymenty do osobnego folderu, żeby nie zawadzały
|
%!s(int64=2) %!d(string=hai) anos | |
|---|---|---|
| eksperymenty | %!s(int64=2) %!d(string=hai) anos | |
| README.md | %!s(int64=2) %!d(string=hai) anos | |
| ciag-q-do-n.v | %!s(int64=2) %!d(string=hai) anos |
README.md
[ℚ] ≅ ℕ
Dowód, że każdy skończony ciąg liczb wymiernych można zakodować jedną liczbą naturalną
Zależności
W nawiasie podano wersje, które na pewno działają:
- Coq (8.14.1)
- Mathematical Components: ssreflect, algebra (1.14.0)
Do zrobienia
Udowdnić, że istnieje bijekcja między skończonymi ciągami liczb wymiernych a liczbami naturalnymi (wzmocnienie obecnego wyniku, który mówi tylko o funkcji różnowartościowej z [Q] w N).