Commit 2023-02-24 07:37 4458fc31

View on Github →

feat: port Topology.UniformSpace.Equicontinuity (#2457)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Set/Image.lean

Created Mathlib/Topology/UniformSpace/Equicontinuity.lean

added theorem Equicontinuous.closure'

added theorem Equicontinuous.closure

added theorem Equicontinuous.comp

added theorem Equicontinuous.continuous

added def Equicontinuous

added theorem EquicontinuousAt.closure'

added theorem EquicontinuousAt.closure

added theorem EquicontinuousAt.comp

added theorem EquicontinuousAt.continuousAt

added def EquicontinuousAt

added theorem Filter.HasBasis.equicontinuousAt_iff

added theorem Filter.HasBasis.equicontinuousAt_iff_left

added theorem Filter.HasBasis.equicontinuousAt_iff_right

added theorem Filter.HasBasis.uniformEquicontinuous_iff

added theorem Filter.HasBasis.uniformEquicontinuous_iff_left

added theorem Filter.HasBasis.uniformEquicontinuous_iff_right

added theorem Filter.Tendsto.continuousAt_of_equicontinuousAt

added theorem Filter.Tendsto.continuous_of_equicontinuous_at

added theorem Filter.Tendsto.uniformContinuous_of_uniformEquicontinuous

added theorem UniformEquicontinuous.closure'

added theorem UniformEquicontinuous.closure

added theorem UniformEquicontinuous.comp

added theorem UniformEquicontinuous.equicontinuous

added theorem UniformEquicontinuous.uniformContinuous

added def UniformEquicontinuous

added theorem UniformInducing.equicontinuousAt_iff

added theorem UniformInducing.equicontinuous_iff

added theorem UniformInducing.uniformEquicontinuous_iff

added theorem equicontinuousAt_iff_continuousAt

added theorem equicontinuousAt_iff_pair

added theorem equicontinuousAt_iff_range

added theorem equicontinuous_iff_continuous

added theorem equicontinuous_iff_range

added theorem uniformEquicontinuous_at_iff_range

added theorem uniformEquicontinuous_iff_uniformContinuous