CICM 2016 tutorial - exercises
- 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
the
proof
from Wikipedia).
Vocabulary file (should be in dict subdirectory)
Exercises with skeletons of proofs
(should be in text directory)
Complete formalization
mizar.el should be copied to your Mizar home
directory (original file can be replaced).