Cantor's diagonal theorem

Stream: maths

[James Palmer]

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

[Patrick Massot]

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

[James Palmer]

Thank you!

[Yury G. Kudryashov]

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