Commit 2024-02-02 14:03 935c0797

View on Github →

feat: relative versions of equicontinuity (#9286)

depends on: #7568

Estimated changes

Modified Mathlib/Analysis/LocallyConvex/Barrelled.lean

Modified Mathlib/Topology/UniformSpace/Equicontinuity.lean

deleted theorem Equicontinuous.closure

added theorem Equicontinuous.equicontinuousOn

added theorem EquicontinuousAt.equicontinuousWithinAt

added theorem EquicontinuousOn.closure'

added theorem EquicontinuousOn.comp

added theorem EquicontinuousOn.continuousOn

added theorem EquicontinuousOn.mono

added def EquicontinuousOn

added theorem EquicontinuousWithinAt.closure'

added theorem EquicontinuousWithinAt.comp

added theorem EquicontinuousWithinAt.continuousWithinAt

added theorem EquicontinuousWithinAt.mono

added def EquicontinuousWithinAt

modified theorem Filter.HasBasis.equicontinuousAt_iff_left

modified theorem Filter.HasBasis.equicontinuousAt_iff_right

added theorem Filter.HasBasis.equicontinuousWithinAt_iff

added theorem Filter.HasBasis.equicontinuousWithinAt_iff_left

added theorem Filter.HasBasis.equicontinuousWithinAt_iff_right

added theorem Filter.HasBasis.uniformEquicontinuousOn_iff

added theorem Filter.HasBasis.uniformEquicontinuousOn_iff_left

added theorem Filter.HasBasis.uniformEquicontinuousOn_iff_right

modified theorem Filter.HasBasis.uniformEquicontinuous_iff_left

modified theorem Filter.HasBasis.uniformEquicontinuous_iff_right

added theorem Filter.Tendsto.continuousOn_of_equicontinuousOn

added theorem Filter.Tendsto.continuousWithinAt_of_equicontinuousWithinAt

added theorem Filter.Tendsto.continuous_of_equicontinuous

deleted theorem Filter.Tendsto.continuous_of_equicontinuousAt

added theorem Filter.Tendsto.uniformContinuousOn_of_uniformEquicontinuousOn

deleted theorem UniformEquicontinuous.closure

added theorem UniformEquicontinuous.uniformEquicontinuousOn

added theorem UniformEquicontinuousOn.closure'

added theorem UniformEquicontinuousOn.comp

added theorem UniformEquicontinuousOn.equicontinuousOn

added theorem UniformEquicontinuousOn.mono

added theorem UniformEquicontinuousOn.uniformContinuousOn

added def UniformEquicontinuousOn

added theorem UniformInducing.equicontinuousOn_iff

added theorem UniformInducing.equicontinuousWithinAt_iff

added theorem UniformInducing.uniformEquicontinuousOn_iff

modified theorem equicontinuousAt_iInf_dom

modified theorem equicontinuousAt_iInf_rng

added theorem equicontinuousAt_restrict_iff

added theorem equicontinuousOn_empty

added theorem equicontinuousOn_finite

added theorem equicontinuousOn_iInf_dom

added theorem equicontinuousOn_iInf_rng

added theorem equicontinuousOn_iff_continuousOn

added theorem equicontinuousOn_iff_range

added theorem equicontinuousOn_unique

added theorem equicontinuousOn_univ

added theorem equicontinuousWithinAt_empty

added theorem equicontinuousWithinAt_finite

added theorem equicontinuousWithinAt_iInf_dom

added theorem equicontinuousWithinAt_iInf_rng

added theorem equicontinuousWithinAt_iff_continuousWithinAt

added theorem equicontinuousWithinAt_iff_pair

added theorem equicontinuousWithinAt_iff_range

added theorem equicontinuousWithinAt_unique

added theorem equicontinuousWithinAt_univ

modified theorem equicontinuous_iInf_dom

modified theorem equicontinuous_iInf_rng

added theorem equicontinuous_restrict_iff

added theorem uniformEquicontinuousOn_empty

added theorem uniformEquicontinuousOn_finite

added theorem uniformEquicontinuousOn_iInf_dom

added theorem uniformEquicontinuousOn_iInf_rng

added theorem uniformEquicontinuousOn_iff_range

added theorem uniformEquicontinuousOn_iff_uniformContinuousOn

added theorem uniformEquicontinuousOn_unique

added theorem uniformEquicontinuousOn_univ

deleted theorem uniformEquicontinuous_at_iff_range

added theorem uniformEquicontinuous_iInf_dom

modified theorem uniformEquicontinuous_iInf_rng

added theorem uniformEquicontinuous_iff_range

added theorem uniformEquicontinuous_restrict_iff

deleted theorem uniform_equicontinuous_infi_dom