English
If F is a closed embedding from 𝔖 covering X and equicontinuous on 𝔖 with a pointwise compact bound, then ι is compact.
Русский
Если F — замкнутое вложение из 𝔖, покрывающего X, и равномерноэконтинуально на 𝔖, и имеются точечные компактные границы, то ι компактно.
LaTeX
$$$\\text{CompactSpace }\\iota$$$
Lean4
/-- A version of the **Arzela-Ascoli theorem**.
Let `X, ι` be topological spaces, `𝔖` a covering of `X` by compact subsets, `α` a T2 uniform space,
`F : ι → (X → α)`, and `s` a subset of `ι`. Assume that:
* `F`, viewed as a function `ι → (X →ᵤ[𝔖] α)`, is a closed embedding (in other words, `ι`
identifies to a closed subset of `X →ᵤ[𝔖] α` through `F`)
* `F '' s` is equicontinuous on each `K ∈ 𝔖`
* For all `x ∈ ⋃₀ 𝔖`, the image of `s` under `i ↦ F i x` is contained in some fixed compact subset.
Then `s` has compact closure in `ι`. -/
theorem isCompact_closure_of_isClosedEmbedding [TopologicalSpace ι] [T2Space α] {𝔖 : Set (Set X)}
(𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (F_clemb : IsClosedEmbedding (UniformOnFun.ofFun 𝔖 ∘ F)) {s : Set ι}
(s_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ ((↑) : s → ι)) K)
(s_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q) : IsCompact (closure s) := by
-- We apply `ArzelaAscoli.compactSpace_of_isClosedEmbedding` to the map
-- `F ∘ (↑) : closure s → (X → α)`, for which all the hypotheses are easily verified.
rw [isCompact_iff_compactSpace]
have : ∀ K ∈ 𝔖, ∀ x ∈ K, Continuous (eval x ∘ F) := fun K hK x hx ↦
UniformOnFun.uniformContinuous_eval_of_mem _ _ hx hK |>.continuous.comp F_clemb.continuous
have cls_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ ((↑) : closure s → ι)) K := fun K hK ↦
(s_eqcont K hK).closure' <| show Continuous (K.restrict ∘ F) from continuous_pi fun ⟨x, hx⟩ ↦ this K hK x hx
have cls_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ i ∈ closure s, F i x ∈ Q := fun K hK x hx ↦
(s_pointwiseCompact K hK x hx).imp fun Q hQ ↦
⟨hQ.1, closure_minimal hQ.2 <| hQ.1.isClosed.preimage (this K hK x hx)⟩
exact
ArzelaAscoli.compactSpace_of_isClosedEmbedding 𝔖_compact
(F_clemb.comp isClosed_closure.isClosedEmbedding_subtypeVal) cls_eqcont fun K hK x hx ↦
(cls_pointwiseCompact K hK x hx).imp fun Q hQ ↦ ⟨hQ.1, by simpa using hQ.2⟩
