English
Under the covering assumption, the closedness of the range of UniformOnFun.ofFun 𝔖 ∘ F is equivalent to the closedness of the range of F.
Русский
При условии покрытия 𝔖, замкнутость образа UniformOnFun.ofFun 𝔖 ∘ F эквивалентна замкнутости образа F.
LaTeX
$$$\\operatorname{IsClosed}(\\operatorname{range}(\\mathrm{UniformOnFun.ofFun}\\, \\mathcal{S} \\circ F)) \\iff \\operatorname{IsClosed}(\\operatorname{range} F)$$$
Lean4
/-- A version of the **Arzela-Ascoli theorem**.
Let `X` be a topological space, `𝔖` a family of compact subsets of `X`, `α` a uniform space,
and `F : ι → (X → α)`. Assume that:
* `F`, viewed as a function `ι → (X →ᵤ[𝔖] α)`, is closed and inducing
* `F` is equicontinuous on each `K ∈ 𝔖`
* For all `x ∈ ⋃₀ 𝔖`, the range of `i ↦ F i x` is contained in some fixed compact subset.
Then `ι` is compact. -/
theorem compactSpace_of_closed_inducing' [TopologicalSpace ι] {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K)
(F_ind : IsInducing (UniformOnFun.ofFun 𝔖 ∘ F)) (F_cl : IsClosed <| range <| UniformOnFun.ofFun 𝔖 ∘ F)
(F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K)
(F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ i, F i x ∈ Q) : CompactSpace ι := by
-- By equicontinuity, we know that the topology on `ι` is also the one induced by
-- `restrict (⋃₀ 𝔖) ∘ F`.
have : IsInducing (restrict (⋃₀ 𝔖) ∘ F) := by
rwa [EquicontinuousOn.inducing_uniformOnFun_iff_pi' 𝔖_compact F_eqcont] at F_ind
rw [← isCompact_univ_iff, this.isCompact_iff, image_univ]
-- But then we are working in a product space, where compactness can easily be proven using
-- Tykhonov's theorem! More precisely, for each `x ∈ ⋃₀ 𝔖`, choose a compact set `Q x`
-- containing all `F i x`s.
rw [← forall_sUnion] at F_pointwiseCompact
choose! Q Q_compact F_in_Q using F_pointwiseCompact
refine
IsCompact.of_isClosed_subset (isCompact_univ_pi fun x ↦ Q_compact x x.2)
(EquicontinuousOn.isClosed_range_pi_of_uniformOnFun' 𝔖_compact F_eqcont F_cl)
(range_subset_iff.mpr fun i x _ ↦ F_in_Q x x.2 i)
