English
If F: ι → X → α is a closed embedding from a cover 𝔖, equicontinuous on 𝔖, and has pointwise compact values, then ι is compact.
Русский
Если отображение F: ι → X → α является вложением с замкнутого образа через покрытие 𝔖, равно равномерно эконтинуально на 𝔖, и для каждого x образ F i 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 uniform space,
and `F : ι → (X → α)`. 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` 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_isClosedEmbedding [TopologicalSpace ι] {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K)
(F_clemb : IsClosedEmbedding (UniformOnFun.ofFun 𝔖 ∘ F)) (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K)
(F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ i, F i x ∈ Q) : CompactSpace ι :=
compactSpace_of_closed_inducing' 𝔖_compact F_clemb.isInducing F_clemb.isClosed_range F_eqcont F_pointwiseCompact
