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
|
пре 2 година | |
|---|---|---|
| eksperymenty | пре 2 година | |
| README.md | пре 2 година | |
| ciag-q-do-n.v | пре 2 година |
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).