Ascoli Theorem

In this file, we prove the general Arzela-Ascoli theorem, and various related statements about the topology of equicontinuous subsetes of X →ᵤ[𝔖] α, where X is a topological space, 𝔖 is a family of compact subsets of X, and α is a uniform space.

Main statements

• If X is a compact space, then the uniform structures of uniform convergence and pointwise convergence coincide on equicontinuous subsets. This is the key fact that makes equicontinuity important in functional analysis. We state various versions of it:
  • as an equality of UniformSpaces: Equicontinuous.comap_uniformFun_eq
  • in terms of IsUniformInducing: Equicontinuous.isUniformInducing_uniformFun_iff_pi
  • in terms of IsInducing: Equicontinuous.inducing_uniformFun_iff_pi
  • in terms of convergence along a filter: Equicontinuous.tendsto_uniformFun_iff_pi
• As a consequence, if 𝔖 is a family of compact subsets of X, then the uniform structures of uniform convergence on 𝔖 and pointwise convergence on ⋃₀ 𝔖 coincide on equicontinuous subsets. Again, we prove multiple variations:
  • as an equality of UniformSpaces: EquicontinuousOn.comap_uniformOnFun_eq
  • in terms of IsUniformInducing: EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi'
  • in terms of IsInducing: EquicontinuousOn.inducing_uniformOnFun_iff_pi'
  • in terms of convergence along a filter: EquicontinuousOn.tendsto_uniformOnFun_iff_pi'
• The Arzela-Ascoli theorem follows from the previous fact and Tykhonov's theorem. All of its variations can be found under the ArzelaAscoli namespace.

Implementation details

• The statements in this file may be a bit daunting because we prove everything for families and embeddings instead of subspaces with the subspace topology. This is done because, in practice, one would rarely work with X →ᵤ[𝔖] α directly, so we need to provide API for bringing back the statements to various other types, such as C(X, Y) or E →L[𝕜] F. To counteract this, all statements (as well as most proofs!) are documented quite thoroughly.

• A lot of statements assume ∀ K ∈ 𝔖, EquicontinuousOn F K instead of the more natural EquicontinuousOn F (⋃₀ 𝔖). This is in order to keep the most generality, as the first statement is strictly weaker.

• In Bourbaki, the usual Arzela-Ascoli compactness theorem follows from a similar total boundedness result. Here we go directly for the compactness result, which is the most useful in practice, but this will be an easy addition/refactor if we ever need it.

TODO

• Prove that, on an equicontinuous family, pointwise convergence and pointwise convergence on a dense subset coincide, and deduce metrizability criterions for equicontinuous subsets.

• Prove the total boundedness version of the theorem

• Prove the converse statement: if a subset of X →ᵤ[𝔖] α is compact, then it is equicontinuous on each K ∈ 𝔖.

References

• N. Bourbaki, General Topology, Chapter X

Tags

equicontinuity, uniform convergence, ascoli

theorem Equicontinuous.comap_uniformFun_eq {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} [CompactSpace X] (F_eqcont : Equicontinuous F) : UniformSpace.comap F (UniformFun.uniformSpace X α) = UniformSpace.comap F (Pi.uniformSpace fun (i : X) => α)

Let X be a compact topological space, α a uniform space, and F : ι → (X → α) an equicontinuous family. Then, the uniform structures of uniform convergence and pointwise convergence induce the same uniform structure on ι.

In other words, pointwise convergence and uniform convergence coincide on an equicontinuous subset of X → α.

Consider using Equicontinuous.isUniformInducing_uniformFun_iff_pi and Equicontinuous.inducing_uniformFun_iff_pi instead, to avoid rewriting instances.

theorem Equicontinuous.isUniformInducing_uniformFun_iff_pi {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} [UniformSpace ι] [CompactSpace X] (F_eqcont : Equicontinuous F) : IsUniformInducing (⇑UniformFun.ofFun ∘ F) ↔ IsUniformInducing F

Let X be a compact topological space, α a uniform space, and F : ι → (X → α) an equicontinuous family. Then, the uniform structures of uniform convergence and pointwise convergence induce the same uniform structure on ι.

In other words, pointwise convergence and uniform convergence coincide on an equicontinuous subset of X → α.

This is a version of Equicontinuous.comap_uniformFun_eq stated in terms of IsUniformInducing for convenuence.

@[deprecated Equicontinuous.isUniformInducing_uniformFun_iff_pi]

theorem Equicontinuous.uniformInducing_uniformFun_iff_pi {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} [UniformSpace ι] [CompactSpace X] (F_eqcont : Equicontinuous F) : IsUniformInducing (⇑UniformFun.ofFun ∘ F) ↔ IsUniformInducing F

Alias of Equicontinuous.isUniformInducing_uniformFun_iff_pi.

---

Let X be a compact topological space, α a uniform space, and F : ι → (X → α) an equicontinuous family. Then, the uniform structures of uniform convergence and pointwise convergence induce the same uniform structure on ι.

In other words, pointwise convergence and uniform convergence coincide on an equicontinuous subset of X → α.

This is a version of Equicontinuous.comap_uniformFun_eq stated in terms of IsUniformInducing for convenuence.

theorem Equicontinuous.inducing_uniformFun_iff_pi {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} [TopologicalSpace ι] [CompactSpace X] (F_eqcont : Equicontinuous F) : Topology.IsInducing (⇑UniformFun.ofFun ∘ F) ↔ Topology.IsInducing F

Let X be a compact topological space, α a uniform space, and F : ι → (X → α) an equicontinuous family. Then, the topologies of uniform convergence and pointwise convergence induce the same topology on ι.

In other words, pointwise convergence and uniform convergence coincide on an equicontinuous subset of X → α.

This is a consequence of Equicontinuous.comap_uniformFun_eq, stated in terms of IsInducing for convenuence.

theorem Equicontinuous.tendsto_uniformFun_iff_pi {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} [CompactSpace X] (F_eqcont : Equicontinuous F) (ℱ : Filter ι) (f : X → α) : Filter.Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (nhds (UniformFun.ofFun f)) ↔ Filter.Tendsto F ℱ (nhds f)

Let X be a compact topological space, α a uniform space, F : ι → (X → α) an equicontinuous family, and ℱ a filter on ι. Then, F tends uniformly to f : X → α along ℱ iff it tends to f pointwise along ℱ.

theorem EquicontinuousOn.comap_uniformOnFun_eq {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) : UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) = UniformSpace.comap ((⋃₀ 𝔖).restrict ∘ F) (Pi.uniformSpace fun (i : ↑(⋃₀ 𝔖)) => α)

Let X be a topological space, 𝔖 a family of compact subsets of X, α a uniform space, and F : ι → (X → α) a family which is equicontinuous on each K ∈ 𝔖. Then, the uniform structures of uniform convergence on 𝔖 and pointwise convergence on ⋃₀ 𝔖 induce the same uniform structure on ι.

In particular, pointwise convergence and compact convergence coincide on an equicontinuous subset of X → α.

Consider using EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi' and EquicontinuousOn.inducing_uniformOnFun_iff_pi' instead to avoid rewriting instances, as well as their unprimed versions in case 𝔖 covers X.

theorem EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi' {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} [UniformSpace ι] {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) : IsUniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsUniformInducing ((⋃₀ 𝔖).restrict ∘ F)

Let X be a topological space, 𝔖 a family of compact subsets of X, α a uniform space, and F : ι → (X → α) a family which is equicontinuous on each K ∈ 𝔖. Then, the uniform structures of uniform convergence on 𝔖 and pointwise convergence on ⋃₀ 𝔖 induce the same uniform structure on ι.

In particular, pointwise convergence and compact convergence coincide on an equicontinuous subset of X → α.

This is a version of EquicontinuousOn.comap_uniformOnFun_eq stated in terms of IsUniformInducing for convenuence.

@[deprecated EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi']

theorem EquicontinuousOn.uniformInducing_uniformOnFun_iff_pi' {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} [UniformSpace ι] {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) : IsUniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsUniformInducing ((⋃₀ 𝔖).restrict ∘ F)

Alias of EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi'.

---

Let X be a topological space, 𝔖 a family of compact subsets of X, α a uniform space, and F : ι → (X → α) a family which is equicontinuous on each K ∈ 𝔖. Then, the uniform structures of uniform convergence on 𝔖 and pointwise convergence on ⋃₀ 𝔖 induce the same uniform structure on ι.

In particular, pointwise convergence and compact convergence coincide on an equicontinuous subset of X → α.

This is a version of EquicontinuousOn.comap_uniformOnFun_eq stated in terms of IsUniformInducing for convenuence.

theorem EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} [UniformSpace ι] {𝔖 : Set (Set X)} (𝔖_covers : ⋃₀ 𝔖 = Set.univ) (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) : IsUniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsUniformInducing F

Let X be a topological space, 𝔖 a covering of X by compact subsets, α a uniform space, and F : ι → (X → α) a family which is equicontinuous on each K ∈ 𝔖. Then, the uniform structures of uniform convergence on 𝔖 and pointwise convergence induce the same uniform structure on ι.

This is a specialization of EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi' to the case where 𝔖 covers X.

@[deprecated EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi]

theorem EquicontinuousOn.uniformInducing_uniformOnFun_iff_pi {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} [UniformSpace ι] {𝔖 : Set (Set X)} (𝔖_covers : ⋃₀ 𝔖 = Set.univ) (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) : IsUniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsUniformInducing F

Alias of EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi.

---

Let X be a topological space, 𝔖 a covering of X by compact subsets, α a uniform space, and F : ι → (X → α) a family which is equicontinuous on each K ∈ 𝔖. Then, the uniform structures of uniform convergence on 𝔖 and pointwise convergence induce the same uniform structure on ι.

This is a specialization of EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi' to the case where 𝔖 covers X.

theorem EquicontinuousOn.inducing_uniformOnFun_iff_pi' {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} [TopologicalSpace ι] {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) : Topology.IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ Topology.IsInducing ((⋃₀ 𝔖).restrict ∘ F)

Let X be a topological space, 𝔖 a family of compact subsets of X, α a uniform space, and F : ι → (X → α) a family which is equicontinuous on each K ∈ 𝔖. Then, the topologies of uniform convergence on 𝔖 and pointwise convergence on ⋃₀ 𝔖 induce the same topology on ι.

In particular, pointwise convergence and compact convergence coincide on an equicontinuous subset of X → α.

This is a consequence of EquicontinuousOn.comap_uniformOnFun_eq stated in terms of IsInducing for convenience.

theorem EquicontinuousOn.isInducing_uniformOnFun_iff_pi {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} [TopologicalSpace ι] {𝔖 : Set (Set X)} (𝔖_covers : ⋃₀ 𝔖 = Set.univ) (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) : Topology.IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ Topology.IsInducing F

Let X be a topological space, 𝔖 a covering of X by compact subsets, α a uniform space, and F : ι → (X → α) a family which is equicontinuous on each K ∈ 𝔖. Then, the topologies of uniform convergence on 𝔖 and pointwise convergence induce the same topology on ι.

This is a specialization of EquicontinuousOn.inducing_uniformOnFun_iff_pi' to the case where 𝔖 covers X.

@[deprecated EquicontinuousOn.isInducing_uniformOnFun_iff_pi]

theorem EquicontinuousOn.inducing_uniformOnFun_iff_pi {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} [TopologicalSpace ι] {𝔖 : Set (Set X)} (𝔖_covers : ⋃₀ 𝔖 = Set.univ) (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) : Topology.IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ Topology.IsInducing F

Alias of EquicontinuousOn.isInducing_uniformOnFun_iff_pi.

---

Let X be a topological space, 𝔖 a covering of X by compact subsets, α a uniform space, and F : ι → (X → α) a family which is equicontinuous on each K ∈ 𝔖. Then, the topologies of uniform convergence on 𝔖 and pointwise convergence induce the same topology on ι.

This is a specialization of EquicontinuousOn.inducing_uniformOnFun_iff_pi' to the case where 𝔖 covers X.

theorem EquicontinuousOn.tendsto_uniformOnFun_iff_pi' {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) (ℱ : Filter ι) (f : X → α) : Filter.Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (nhds ((UniformOnFun.ofFun 𝔖) f)) ↔ Filter.Tendsto ((⋃₀ 𝔖).restrict ∘ F) ℱ (nhds ((⋃₀ 𝔖).restrict f))

Let X be a topological space, 𝔖 a family of compact subsets of X, α a uniform space, F : ι → (X → α) a family equicontinuous on each K ∈ 𝔖, and ℱ a filter on ι. Then, F tends to f : X → α along ℱ uniformly on each K ∈ 𝔖 iff it tends to f pointwise on ⋃₀ 𝔖 along ℱ.

theorem EquicontinuousOn.tendsto_uniformOnFun_iff_pi {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (𝔖_covers : ⋃₀ 𝔖 = Set.univ) (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) (ℱ : Filter ι) (f : X → α) : Filter.Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (nhds ((UniformOnFun.ofFun 𝔖) f)) ↔ Filter.Tendsto F ℱ (nhds f)

Let X be a topological space, 𝔖 a covering of X by compact subsets, α a uniform space, F : ι → (X → α) a family equicontinuous on each K ∈ 𝔖, and ℱ a filter on ι. Then, F tends to f : X → α along ℱ uniformly on each K ∈ 𝔖 iff it tends to f pointwise along ℱ.

This is a specialization of EquicontinuousOn.tendsto_uniformOnFun_iff_pi' to the case where 𝔖 covers X.

theorem EquicontinuousOn.isClosed_range_pi_of_uniformOnFun' {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) (H : IsClosed (Set.range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))) : IsClosed (Set.range ((⋃₀ 𝔖).restrict ∘ F))

Let X be a topological space, 𝔖 a family of compact subsets of X and α a uniform space. An equicontinuous subset of X → α is closed in the topology of uniform convergence on all K ∈ 𝔖 iff it is closed in the topology of pointwise convergence on ⋃₀ 𝔖.

theorem EquicontinuousOn.isClosed_range_uniformOnFun_iff_pi {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (𝔖_covers : ⋃₀ 𝔖 = Set.univ) (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) : IsClosed (Set.range (⇑(UniformOnFun.ofFun 𝔖) ∘ F)) ↔ IsClosed (Set.range F)

Let X be a topological space, 𝔖 a covering of X by compact subsets, and α a uniform space. An equicontinuous subset of X → α is closed in the topology of uniform convergence on all K ∈ 𝔖 iff it is closed in the topology of pointwise convergence.

This is a specialization of EquicontinuousOn.isClosed_range_pi_of_uniformOnFun' to the case where 𝔖 covers X.

theorem EquicontinuousOn.isClosed_range_pi_of_uniformOnFun {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (𝔖_covers : ⋃₀ 𝔖 = Set.univ) (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) : IsClosed (Set.range (⇑(UniformOnFun.ofFun 𝔖) ∘ F)) → IsClosed (Set.range F)

Alias of the forward direction of EquicontinuousOn.isClosed_range_uniformOnFun_iff_pi.

---

Let X be a topological space, 𝔖 a covering of X by compact subsets, and α a uniform space. An equicontinuous subset of X → α is closed in the topology of uniform convergence on all K ∈ 𝔖 iff it is closed in the topology of pointwise convergence.

This is a specialization of EquicontinuousOn.isClosed_range_pi_of_uniformOnFun' to the case where 𝔖 covers X.

theorem ArzelaAscoli.compactSpace_of_closed_inducing' {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} [TopologicalSpace ι] {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (F_ind : Topology.IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F)) (F_cl : IsClosed (Set.range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))) (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) (F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ (Q : Set α), IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q) : CompactSpace ι

A version of the Arzela-Ascoli theorem.

Let X be a topological space, 𝔖 a family of compact subsets of X, α a uniform space, and F : ι → (X → α). Assume that:

• F, viewed as a function ι → (X →ᵤ[𝔖] α), is closed and inducing
• F is equicontinuous on each K ∈ 𝔖
• For all x ∈ ⋃₀ 𝔖, the range of i ↦ F i x is contained in some fixed compact subset.

Then ι is compact.

theorem ArzelaAscoli.compactSpace_of_isClosedEmbedding {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} [TopologicalSpace ι] {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (F_clemb : Topology.IsClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F)) (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) (F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ (Q : Set α), IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q) : CompactSpace ι

A version of the Arzela-Ascoli theorem.

Let X, ι be topological spaces, 𝔖 a covering of X by compact subsets, α a uniform space, and F : ι → (X → α). Assume that:

• F, viewed as a function ι → (X →ᵤ[𝔖] α), is a closed embedding (in other words, ι identifies to a closed subset of X →ᵤ[𝔖] α through F)
• F is equicontinuous on each K ∈ 𝔖
• For all x, the range of i ↦ F i x is contained in some fixed compact subset.

Then ι is compact.

@[deprecated ArzelaAscoli.compactSpace_of_isClosedEmbedding]

theorem ArzelaAscoli.compactSpace_of_closedEmbedding {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} [TopologicalSpace ι] {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (F_clemb : Topology.IsClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F)) (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) (F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ (Q : Set α), IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q) : CompactSpace ι

Alias of ArzelaAscoli.compactSpace_of_isClosedEmbedding.

---

A version of the Arzela-Ascoli theorem.

Let X, ι be topological spaces, 𝔖 a covering of X by compact subsets, α a uniform space, and F : ι → (X → α). Assume that:

• F, viewed as a function ι → (X →ᵤ[𝔖] α), is a closed embedding (in other words, ι identifies to a closed subset of X →ᵤ[𝔖] α through F)
• F is equicontinuous on each K ∈ 𝔖
• For all x, the range of i ↦ F i x is contained in some fixed compact subset.

Then ι is compact.

theorem ArzelaAscoli.isCompact_closure_of_isClosedEmbedding {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} [TopologicalSpace ι] [T2Space α] {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (F_clemb : Topology.IsClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F)) {s : Set ι} (s_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K) (s_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ (Q : Set α), IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q) : IsCompact (closure s)

A version of the Arzela-Ascoli theorem.

Let X, ι be topological spaces, 𝔖 a covering of X by compact subsets, α a T2 uniform space, F : ι → (X → α), and s a subset of ι. Assume that:

• F, viewed as a function ι → (X →ᵤ[𝔖] α), is a closed embedding (in other words, ι identifies to a closed subset of X →ᵤ[𝔖] α through F)
• F '' s is equicontinuous on each K ∈ 𝔖
• For all x ∈ ⋃₀ 𝔖, the image of s under i ↦ F i x is contained in some fixed compact subset.

Then s has compact closure in ι.

@[deprecated ArzelaAscoli.isCompact_closure_of_isClosedEmbedding]

theorem ArzelaAscoli.isCompact_closure_of_closedEmbedding {ι : Type u_1} {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} [TopologicalSpace ι] [T2Space α] {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K) (F_clemb : Topology.IsClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F)) {s : Set ι} (s_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K) (s_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ (Q : Set α), IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q) : IsCompact (closure s)

Alias of ArzelaAscoli.isCompact_closure_of_isClosedEmbedding.

---

A version of the Arzela-Ascoli theorem.

Let X, ι be topological spaces, 𝔖 a covering of X by compact subsets, α a T2 uniform space, F : ι → (X → α), and s a subset of ι. Assume that:

• F, viewed as a function ι → (X →ᵤ[𝔖] α), is a closed embedding (in other words, ι identifies to a closed subset of X →ᵤ[𝔖] α through F)
• F '' s is equicontinuous on each K ∈ 𝔖
• For all x ∈ ⋃₀ 𝔖, the image of s under i ↦ F i x is contained in some fixed compact subset.

Then s has compact closure in ι.

theorem ArzelaAscoli.isCompact_of_equicontinuous {X : Type u_2} {α : Type u_3} [TopologicalSpace X] [UniformSpace α] (S : Set C(X, α)) (hS1 : IsCompact (ContinuousMap.toFun '' S)) (hS2 : Equicontinuous fun (x : ↑S) => ⇑↑x) : IsCompact S

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.