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.

Estimated changes