Commit 2025-01-05 12:29 1d1c8c25
View on Github →feat: Ico, Ioc, and Ioo are not closed or compact (#20479)
Inspired by this Zulip thread which tried to prove a false result.
Also includes 12 stupid lemmas about interval equalities to make simp slightly more helpful.
I don't know if the topological results can be generalized further, but these lemmas at least work for Real as was needed on Zulip.