Zulip Chat Archive

Stream: maths

Topic: Cantor's intersection thm

Yury G. Kudryashov (Feb 04 2020 at 21:16):

Hi, do we have https://en.wikipedia.org/wiki/Cantor%27s_intersection_theorem ? It should be easy to formalize but I want to avoid reinventing the wheel.

Patrick Massot (Feb 04 2020 at 21:17):

I don't think so. It should be in subset_properties.lean hence easy to find.

Last updated: May 02 2025 at 03:31 UTC