Commit 2024-04-07 22:24 2e7bb640

View on Github →

feat: general Ascoli theorem (#6844) This was discussed on Zulip recently and a while ago.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Constructions.lean

added theorem Pi.induced_restrict_sUnion

Created Mathlib/Topology/UniformSpace/Ascoli.lean

added theorem ArzelaAscoli.compactSpace_of_closedEmbedding

added theorem ArzelaAscoli.compactSpace_of_closed_inducing'

added theorem ArzelaAscoli.isCompact_closure_of_closedEmbedding

added theorem Equicontinuous.comap_uniformFun_eq

added theorem Equicontinuous.inducing_uniformFun_iff_pi

added theorem Equicontinuous.tendsto_uniformFun_iff_pi

added theorem Equicontinuous.uniformInducing_uniformFun_iff_pi

added theorem EquicontinuousOn.comap_uniformOnFun_eq

added theorem EquicontinuousOn.inducing_uniformOnFun_iff_pi'

added theorem EquicontinuousOn.inducing_uniformOnFun_iff_pi

added theorem EquicontinuousOn.isClosed_range_pi_of_uniformOnFun'

added theorem EquicontinuousOn.isClosed_range_uniformOnFun_iff_pi

added theorem EquicontinuousOn.tendsto_uniformOnFun_iff_pi'

added theorem EquicontinuousOn.tendsto_uniformOnFun_iff_pi

added theorem EquicontinuousOn.uniformInducing_uniformOnFun_iff_pi'

added theorem EquicontinuousOn.uniformInducing_uniformOnFun_iff_pi

Modified Mathlib/Topology/UniformSpace/Pi.lean

added theorem Pi.uniformSpace_comap_restrict_sUnion

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

added theorem UniformOnFun.uniformContinuous_restrict_toFun