The Arzelà–Ascoli theorem for bounded continuous functions

Arzelà–Ascoli asserts that, on a compact space, a set of functions sharing a common modulus of continuity and taking values in a compact set forms a compact subset for the topology of uniform convergence. This file proves the theorem and several useful variations around it.

theorem BoundedContinuousFunction.arzela_ascoli₁ {α : Type u} {β : Type v} [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] [CompactSpace β] (A : Set (BoundedContinuousFunction α β)) (closed : IsClosed A) (H : Equicontinuous fun (x : ↑A) => ⇑↑x) : IsCompact A

First version, with pointwise equicontinuity and range in a compact space.

theorem BoundedContinuousFunction.arzela_ascoli₂ {α : Type u} {β : Type v} [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] (s : Set β) (hs : IsCompact s) (A : Set (BoundedContinuousFunction α β)) (closed : IsClosed A) (in_s : ∀ (f : BoundedContinuousFunction α β) (x : α), f ∈ A → f x ∈ s) (H : Equicontinuous fun (x : ↑A) => ⇑↑x) : IsCompact A

Second version, with pointwise equicontinuity and range in a compact subset.

theorem BoundedContinuousFunction.arzela_ascoli {α : Type u} {β : Type v} [TopologicalSpace α] [CompactSpace α] [PseudoMetricSpace β] [T2Space β] (s : Set β) (hs : IsCompact s) (A : Set (BoundedContinuousFunction α β)) (in_s : ∀ (f : BoundedContinuousFunction α β) (x : α), f ∈ A → f x ∈ s) (H : Equicontinuous fun (x : ↑A) => ⇑↑x) : IsCompact (closure A)

Third (main) version, with pointwise equicontinuity and range in a compact subset, but without closedness. The closure is then compact.