Commit 2025-09-22 15:52 ea6c1124

feat: some lemmas about closed maps (#29144) This is a compilation of (1) some observations by @PatrickMassot and (2) some lemmas written by @AntoineChambert-Loir and I for a specific application, which turned out to have a nice proof using (1). The most interesting results are:

• isClosedMap_iff_kernImage: a map is closed iff the Set.kernImage of any open set is open (+ similar result for open maps)
• isClosedMap_iff_comap_nhds_le: as a consequence, the map f is closed iff for any y, one has comap f (𝓝 y) ≤ 𝓝ˢ (f ⁻¹' {y}) (with equality if f is also continuous)
• IsClosedMap.eventually_nhds_fiber is a restatement of this in eventually terms: assuming f is closed, if some property holds in the neighborhood of the fiber at y₀, then it holds on the fiber at y for all y close enough to y₀.