Commit 2026-10-20 13:30 6e31548e

feat: add some lemmas that closures of some sets are compact (#39382)

• Also tag them with closedness/compactness.
• This can be refactored to use RelativelyCompact once we define that notion.
• Note: this is only equivalent to IsBounded in ProperSpace. It is equivalent to @IsBounded _ (inCompact X) s in a T2-space, but the latter thing is cumbersome to write.