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 18 2021 at 07:19 UTC