English
If an equicontinuous family of continuous functions is compact in the pointwise topology, then it is compact in the compact-open topology.
Русский
Если равномерно непрерывная (эконтинуированная) семейство непрерывных функций компактно в точечной топологии, то оно компактно в топологии компакт-открытых множеств.
LaTeX
$$$\\text{IsCompact}(S) \\text{ given } S \\subset C(X,α), \\text{ with } hS1,hS2$$$
Lean4
/-- A version of the **Arzela-Ascoli theorem**.
If an equicontinuous family of continuous functions is compact in the pointwise topology, then it
is compact in the compact open topology. -/
theorem isCompact_of_equicontinuous (S : Set C(X, α)) (hS1 : IsCompact (ContinuousMap.toFun '' S))
(hS2 : Equicontinuous ((↑) : S → X → α)) : IsCompact S :=
by
suffices h : IsInducing (Equiv.Set.image _ S DFunLike.coe_injective)
by
rw [isCompact_iff_compactSpace] at hS1 ⊢
exact (Equiv.toHomeomorphOfIsInducing _ h).symm.compactSpace
rw [← IsInducing.subtypeVal.of_comp_iff, ← EquicontinuousOn.isInducing_uniformOnFun_iff_pi _ _ _]
· exact ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact.isInducing.comp .subtypeVal
· exact eq_univ_iff_forall.mpr (fun x ↦ mem_sUnion_of_mem (mem_singleton x) isCompact_singleton)
· exact fun _ ↦ id
· exact fun K _ ↦ hS2.equicontinuousOn K
