Commit 2025-11-01 17:18 147805a9

feat(Topology/Semicontinuous): lower bounds on compact sets (#29976) Prove that lower semicontinuous functions attain their lower bound on nonempty compact sets, and the analogous lemma for upper semicontinuous functions. By the way, add several basic results for semicontinuous functions, relating the WithinAt, At, On versions. Co-authored with @ADedecker