Commit 2026-08-19 02:29 ffbfefae

feat(Topology/Semicontinuity/Michael): michael's selection theorem (#39116) Michael's selection theorem states that a correspondence f : α → Set β from a normal, paracompact topological space α to a Frechet space β that is lower hemicontinuous, and has nonempty, closed, convex values admits a continuous selection, i.e., a map g : α → β such that g x ∈ f x for all x. This theorem is used in many places, e.g., to find continuous sections to certain functions. This PR proves this theorem.