Zulip Chat Archive

Stream: maths

Topic: Cantor's diagonal theorem


view this post on Zulip James Palmer (Aug 10 2020 at 13:23):

Hi everyone - I was wondering if there was any material on Cantor's proof that the real numbers are uncountable in Lean. Many thanks :)

view this post on Zulip Patrick Massot (Aug 10 2020 at 18:29):

https://leanprover-community.github.io/mathlib_docs/data/real/cardinality.html#cardinal.not_countable_real

view this post on Zulip James Palmer (Aug 11 2020 at 14:27):

Thank you!

view this post on Zulip Yury G. Kudryashov (Aug 13 2020 at 04:39):

See also docs#function.cantor_surjective and docs#function.cantor_injective


Last updated: May 19 2021 at 02:10 UTC