Documentation

Mathlib.Topology.UniformSpace.Ascoli

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 #

Implementation details #

TODO #

References #

Tags #

equicontinuity, uniform convergence, ascoli

theorem Equicontinuous.comap_uniformFun_eq {ฮน : Type u_1} {X : Type u_2} {ฮฑ : Type u_4} [TopologicalSpace X] [UniformSpace ฮฑ] {F : ฮน โ†’ X โ†’ ฮฑ} [CompactSpace X] (F_eqcont : Equicontinuous 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 โ†’ ฮฑ.

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

theorem Equicontinuous.uniformInducing_uniformFun_iff_pi {ฮน : Type u_1} {X : Type u_2} {ฮฑ : Type u_4} [TopologicalSpace X] [UniformSpace ฮฑ] {F : ฮน โ†’ X โ†’ ฮฑ} [UniformSpace ฮน] [CompactSpace X] (F_eqcont : Equicontinuous F) :
UniformInducing (โ‡‘UniformFun.ofFun โˆ˜ F) โ†” UniformInducing 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 UniformInducing for convenuence.

theorem Equicontinuous.inducing_uniformFun_iff_pi {ฮน : Type u_1} {X : Type u_2} {ฮฑ : Type u_4} [TopologicalSpace X] [UniformSpace ฮฑ] {F : ฮน โ†’ X โ†’ ฮฑ} [TopologicalSpace ฮน] [CompactSpace X] (F_eqcont : Equicontinuous F) :
Inducing (โ‡‘UniformFun.ofFun โˆ˜ F) โ†” Inducing 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 Inducing for convenuence.

theorem Equicontinuous.tendsto_uniformFun_iff_pi {ฮน : Type u_1} {X : Type u_2} {ฮฑ : Type u_4} [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_4} [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.uniformInducing_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.uniformInducing_uniformOnFun_iff_pi' {ฮน : Type u_1} {X : Type u_2} {ฮฑ : Type u_4} [TopologicalSpace X] [UniformSpace ฮฑ] {F : ฮน โ†’ X โ†’ ฮฑ} [UniformSpace ฮน] {๐”– : Set (Set X)} (๐”–_compact : โˆ€ K โˆˆ ๐”–, IsCompact K) (F_eqcont : โˆ€ K โˆˆ ๐”–, EquicontinuousOn F K) :

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 UniformInducing for convenuence.

theorem EquicontinuousOn.uniformInducing_uniformOnFun_iff_pi {ฮน : Type u_1} {X : Type u_2} {ฮฑ : Type u_4} [TopologicalSpace X] [UniformSpace ฮฑ] {F : ฮน โ†’ X โ†’ ฮฑ} [UniformSpace ฮน] {๐”– : Set (Set X)} (๐”–_covers : โ‹ƒโ‚€ ๐”– = Set.univ) (๐”–_compact : โˆ€ K โˆˆ ๐”–, IsCompact K) (F_eqcont : โˆ€ K โˆˆ ๐”–, EquicontinuousOn F K) :

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.uniformInducing_uniformOnFun_iff_pi' to the case where ๐”– covers X.

theorem EquicontinuousOn.inducing_uniformOnFun_iff_pi' {ฮน : Type u_1} {X : Type u_2} {ฮฑ : Type u_4} [TopologicalSpace X] [UniformSpace ฮฑ] {F : ฮน โ†’ X โ†’ ฮฑ} [TopologicalSpace ฮน] {๐”– : Set (Set X)} (๐”–_compact : โˆ€ K โˆˆ ๐”–, IsCompact K) (F_eqcont : โˆ€ K โˆˆ ๐”–, EquicontinuousOn F K) :
Inducing (โ‡‘(UniformOnFun.ofFun ๐”–) โˆ˜ F) โ†” Inducing ((โ‹ƒโ‚€ ๐”–).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 Inducing for convenuence.

theorem EquicontinuousOn.inducing_uniformOnFun_iff_pi {ฮน : Type u_1} {X : Type u_2} {ฮฑ : Type u_4} [TopologicalSpace X] [UniformSpace ฮฑ] {F : ฮน โ†’ X โ†’ ฮฑ} [TopologicalSpace ฮน] {๐”– : Set (Set X)} (๐”–_covers : โ‹ƒโ‚€ ๐”– = Set.univ) (๐”–_compact : โˆ€ K โˆˆ ๐”–, IsCompact K) (F_eqcont : โˆ€ K โˆˆ ๐”–, EquicontinuousOn F K) :

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_4} [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_4} [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_4} [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_4} [TopologicalSpace X] [UniformSpace ฮฑ] {F : ฮน โ†’ X โ†’ ฮฑ} {๐”– : Set (Set X)} (๐”–_compact : โˆ€ K โˆˆ ๐”–, IsCompact K) (๐”–_covers : โ‹ƒโ‚€ ๐”– = Set.univ) (F_eqcont : โˆ€ K โˆˆ ๐”–, EquicontinuousOn F K) :

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_4} [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_4} [TopologicalSpace X] [UniformSpace ฮฑ] {F : ฮน โ†’ X โ†’ ฮฑ} [TopologicalSpace ฮน] {๐”– : Set (Set X)} (๐”–_compact : โˆ€ K โˆˆ ๐”–, IsCompact K) (F_ind : Inducing (โ‡‘(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) :

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_closedEmbedding {ฮน : Type u_1} {X : Type u_2} {ฮฑ : Type u_4} [TopologicalSpace X] [UniformSpace ฮฑ] {F : ฮน โ†’ X โ†’ ฮฑ} [TopologicalSpace ฮน] {๐”– : Set (Set X)} (๐”–_compact : โˆ€ K โˆˆ ๐”–, IsCompact K) (F_clemb : ClosedEmbedding (โ‡‘(UniformOnFun.ofFun ๐”–) โˆ˜ F)) (F_eqcont : โˆ€ K โˆˆ ๐”–, EquicontinuousOn F K) (F_pointwiseCompact : โˆ€ K โˆˆ ๐”–, โˆ€ x โˆˆ K, โˆƒ (Q : Set ฮฑ), IsCompact Q โˆง โˆ€ (i : ฮน), F i x โˆˆ Q) :

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_closedEmbedding {ฮน : Type u_1} {X : Type u_2} {ฮฑ : Type u_4} [TopologicalSpace X] [UniformSpace ฮฑ] {F : ฮน โ†’ X โ†’ ฮฑ} [TopologicalSpace ฮน] [T2Space ฮฑ] {๐”– : Set (Set X)} (๐”–_compact : โˆ€ K โˆˆ ๐”–, IsCompact K) (F_clemb : ClosedEmbedding (โ‡‘(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) :

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_4} [TopologicalSpace X] [UniformSpace ฮฑ] (S : Set C(X, ฮฑ)) (hS1 : IsCompact (ContinuousMap.toFun '' S)) (hS2 : Equicontinuous fun (x : โ†‘S) => โ‡‘โ†‘x) :

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.