English
An equicontinuous subset of X → α is closed in the topology of uniform convergence on all 𝔖 if and only if it is closed in the topology of pointwise convergence on ⋃₀𝔖.
Русский
Эконтинуальное подмножество множества функций X → α замкнуто в топологии униформной сходимости на всех K ∈ 𝔖 тогда и только тогда, когда оно замкнуто в топологии точечной сходимости на ⋃₀𝔖.
LaTeX
$$$\\operatorname{IsClosed}\\bigl(\\operatorname{range} (\\mathrm{UniformOnFun.ofFun}\\,\\mathcal{S} \\circ F)\\bigr) \\iff \\operatorname{IsClosed}\\bigl(\\operatorname{range}\\bigl((\\bigcup_0 \\mathcal{S}).\\restrict \\circ F\\bigr)\\bigr)$$$
Lean4
/-- Let `X` be a topological space, `𝔖` a family of compact subsets of `X` 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 on `⋃₀ 𝔖`. -/
theorem isClosed_range_pi_of_uniformOnFun' {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K)
(F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) (H : IsClosed (range <| UniformOnFun.ofFun 𝔖 ∘ F)) :
IsClosed (range <| (⋃₀ 𝔖).restrict ∘ F) := by
-- Do we have no equivalent of `nontriviality`?
rcases isEmpty_or_nonempty α with _ | _
·
simp [isClosed_discrete]
-- 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,
Subtype.coe_injective.surjective_comp_right.forall, ← restrict_eq, ←
EquicontinuousOn.tendsto_uniformOnFun_iff_pi' 𝔖_compact F_eqcont]
exact fun f ⟨u, _, hu⟩ ↦ mem_image_of_mem _ <| H.mem_of_tendsto hu <| Eventually.of_forall mem_range_self
