English
A second version of Arzelà–Ascoli with domain and range restrictions, proving compactness of A provided equicontinuity and compact image.
Русский
Вторая версия Арзеля–Азколи с ограничениями домена и образа; компактность A получена при экконтинуальности и компактности образа.
LaTeX
$$$\\text{arzela_ascoli₂} \\ (s \\subseteq β) \\rightarrow \\text{compactness of } A$$$
Lean4
/-- Second version, with pointwise equicontinuity and range in a compact subset. -/
theorem arzela_ascoli₂ (s : Set β) (hs : IsCompact s) (A : Set (α →ᵇ β)) (closed : IsClosed A)
(in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s) (H : Equicontinuous ((↑) : A → α → β)) : IsCompact A := by
/- This version is deduced from the previous one by restricting to the compact type in the target,
using compactness there and then lifting everything to the original space. -/
have M : LipschitzWith 1 Subtype.val := LipschitzWith.subtype_val s
let F : (α →ᵇ s) → α →ᵇ β := comp (↑) M
refine IsCompact.of_isClosed_subset ((?_ : IsCompact (F ⁻¹' A)).image (continuous_comp M)) closed fun f hf => ?_
· haveI : CompactSpace s := isCompact_iff_compactSpace.1 hs
refine arzela_ascoli₁ _ (continuous_iff_isClosed.1 (continuous_comp M) _ closed) ?_
rw [isUniformEmbedding_subtype_val.isUniformInducing.equicontinuous_iff]
exact H.comp (A.restrictPreimage F)
· let g := codRestrict s f fun x => in_s f x hf
rw [show f = F g by ext; rfl] at hf ⊢
exact ⟨g, hf, rfl⟩
