CICM 2016 tutorial - exercises
Vocabulary file (should be in dict subdirectory)
- Define Liouville numbers
- Show that in the definition of Liouville numbers taken from Wikipedia
the quantification of n can be replaced from "every positive integer"
into "non-zero natural number".
Prove auxiliary lemma that powers of two are unbounded, i.e.,
for any integer d, there exists a non-zero natural number
such that 2 to_power (n - 1) > d.
- Prove that no Liouville number can be rational (follow
Exercises with skeletons of proofs
(should be in text directory)
mizar.el should be copied to your Mizar home
directory (original file can be replaced).