English
In a locally compact pair, given a continuous map f, a compact K, an open U containing f[K], there exists a compact L ⊇ K with MapsTo f L U.
Русский
В локально компактной паре при непрерывном отображении f, компактном K и открытом U, содержащем f[K], существует компактное L, содержащее K в собственно внутренности, такое что MapsTo f L U.
LaTeX
$$$[LocallyCompactPair\;X\;Y] {f:X\to Y} {K:Set\;X} {U:Set\;Y},\ Continuous\;f\rightarrow IsCompact\;K\rightarrow IsOpen\;U\rightarrow MapsTo\;f\;K\;U\rightarrow \exists L\;L\in 𝓝^s\;K\;\land IsCompact\;L\land MapsTo\;f\;L\;U$$$
Lean4
/-- If `f : X → Y` is a continuous map in a locally compact pair of topological spaces,
`K : set X` is a compact set, and `U` is an open neighbourhood of `f '' K`,
then there exists a compact neighbourhood `L` of `K` such that `f` maps `L` to `U`.
This is a generalization of `exists_mem_nhds_isCompact_mapsTo`. -/
theorem exists_mem_nhdsSet_isCompact_mapsTo [LocallyCompactPair X Y] {f : X → Y} {K : Set X} {U : Set Y}
(hf : Continuous f) (hK : IsCompact K) (hU : IsOpen U) (hKU : MapsTo f K U) :
∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U :=
by
choose! V hxV hVc hVU using fun x (hx : x ∈ K) ↦ exists_mem_nhds_isCompact_mapsTo hf (hU.mem_nhds (hKU hx))
rcases hK.elim_nhds_subcover_nhdsSet hxV with ⟨s, hsK, hKs⟩
exact ⟨_, hKs, s.isCompact_biUnion fun x hx ↦ hVc x (hsK x hx), mapsTo_iUnion₂.2 fun x hx ↦ hVU x (hsK x hx)⟩
