English
If 𝔖 covers X by compacts and F is equicontinuous on each K, then range of UniformOnFun.ofFun 𝔖 ∘ F is closed if and only if range of F is closed.
Русский
Если 𝔖 покрывает X компактом и F равномерно непрерывно на каждом K, то замкнутость образа UniformOnFun.ofFun 𝔖 ∘ F эквивалентна замкнутости образа F.
LaTeX
$$$\\operatorname{IsClosed}(\\operatorname{range}(\\mathrm{UniformOnFun.ofFun}\\, \\mathcal{S} \\circ F)) \\iff \\operatorname{IsClosed}(\\operatorname{range} F)$$$
Lean4
/-- Let `X` be a topological space, `𝔖` a covering of `X` by compact subsets, and
`α` a uniform space. An equicontinuous subset of `X → α` is closed in the topology of uniform
convergence on all `K ∈ 𝔖` iff it is closed in the topology of pointwise convergence.
This is a specialization of `EquicontinuousOn.isClosed_range_pi_of_uniformOnFun'` to the case where
`𝔖` covers `X`. -/
theorem isClosed_range_uniformOnFun_iff_pi {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (𝔖_covers : ⋃₀ 𝔖 = univ)
(F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) : IsClosed (range <| UniformOnFun.ofFun 𝔖 ∘ F) ↔ IsClosed (range F) := by
-- This follows from the previous lemmas and the characterization of the closure using filters.
simp_rw [isClosed_iff_clusterPt, ← Filter.map_top, ← mapClusterPt_def, mapClusterPt_iff_ultrafilter, range_comp,
(UniformOnFun.ofFun 𝔖).surjective.forall, ←
EquicontinuousOn.tendsto_uniformOnFun_iff_pi 𝔖_compact 𝔖_covers F_eqcont,
(UniformOnFun.ofFun 𝔖).injective.mem_set_image]
