Source result 1 · theorem
BoundedContinuousFunction.arzela_ascoli
Mathlib/Topology/ContinuousMap/Bounded/ArzelaAscoli.lean:109 to 119 · bbc4475e9e8f · Apache-2.0
Exact Lean statement
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)