English
The main Arzelà–Ascoli theorem for a set A of bounded continuous functions with pointwise equicontinuity and compact image; the closure of A is compact.
Русский
Главная теорема Арзеля–Азколи для множества A ограниченных непрерывных функций с поком по точке экконтинуальность и компактное образ; замыкание A компактно.
LaTeX
$$$\\text{arzela_ascoli} \\ s \\rightarrow \\text{closure}(A) \\text{ is compact}$$$
Lean4
/-- Third (main) version, with pointwise equicontinuity and range in a compact subset, but
without closedness. The closure is then compact. -/
theorem arzela_ascoli [T2Space β] (s : Set β) (hs : IsCompact s) (A : Set (α →ᵇ β))
(in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s) (H : Equicontinuous ((↑) : A → α → β)) : IsCompact (closure A) :=
/- This version is deduced from the previous one by checking that the closure of `A`, in
addition to being closed, still satisfies the properties of compact range and equicontinuity. -/
arzela_ascoli₂ s hs (closure A) isClosed_closure
(fun _ x hf =>
(mem_of_closed' hs.isClosed).2 fun ε ε0 =>
let ⟨g, gA, dist_fg⟩ := Metric.mem_closure_iff.1 hf ε ε0
⟨g x, in_s g x gA, lt_of_le_of_lt (dist_coe_le_dist _) dist_fg⟩)
(H.closure' continuous_coe)
