Commit 2026-02-11 17:47 002cb648

feat: variant of isOpen_setOf_mapsTo for continuous maps out of compact spaces (#34862) I introduce 3 lemmas:

1. MapsTo f univ t ↔ range f ⊆ t
2. IsOpen {f : C(X, Y) | range f ⊆ U}
3. ∀ᶠ g : C(X, Y) in 𝓝 f, range g ⊆ U There are multiple ways to spell number 1, including ∀ x, f x ∈ t, that are acceptable. However, I find range f ⊆ t the most natural and least verbose. In my use case, I have had to reasoning about range f, where f is a ContinuousMap out of a compact space, so lemmas using range f and CompactSpace are much more direct.