Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-06 14:57 41e1ab75

View on Github →

feat(topology/uniform_space/equicontinuity): definition and basic properties of [uniform] equicontinuity (#16467)

Estimated changes

Modified src/topology/continuous_function/bounded.lean

added theorem bounded_continuous_function.embedding_coe_fn

deleted theorem bounded_continuous_function.equicontinuous_of_continuity_modulus

added theorem bounded_continuous_function.inducing_coe_fn

Created src/topology/metric_space/equicontinuity.lean

added theorem metric.equicontinuous_at_iff

added theorem metric.equicontinuous_at_iff_right

added theorem metric.equicontinuous_at_of_continuity_modulus

added theorem metric.equicontinuous_of_continuity_modulus

added theorem metric.uniform_equicontinuous_iff

added theorem metric.uniform_equicontinuous_iff_right

added theorem metric.uniform_equicontinuous_of_continuity_modulus

Modified src/topology/metric_space/gromov_hausdorff_realized.lean

Modified src/topology/uniform_space/compact.lean

added theorem compact_space.uniform_equicontinuous_of_equicontinuous

Created src/topology/uniform_space/equicontinuity.lean

added theorem equicontinuous.closure'

added theorem equicontinuous.closure

added theorem equicontinuous.comp

added theorem equicontinuous.continuous

added def equicontinuous

added theorem equicontinuous_at.closure'

added theorem equicontinuous_at.closure

added theorem equicontinuous_at.comp

added theorem equicontinuous_at.continuous_at

added def equicontinuous_at

added theorem equicontinuous_at_iff_continuous_at

added theorem equicontinuous_at_iff_pair

added theorem equicontinuous_at_iff_range

added theorem equicontinuous_iff_continuous

added theorem equicontinuous_iff_range

added theorem filter.has_basis.equicontinuous_at_iff

added theorem filter.has_basis.equicontinuous_at_iff_left

added theorem filter.has_basis.equicontinuous_at_iff_right

added theorem filter.has_basis.uniform_equicontinuous_iff

added theorem filter.has_basis.uniform_equicontinuous_iff_left

added theorem filter.has_basis.uniform_equicontinuous_iff_right

added theorem filter.tendsto.continuous_at_of_equicontinuous_at

added theorem filter.tendsto.continuous_of_equicontinuous_at

added theorem filter.tendsto.uniform_continuous_of_uniform_equicontinuous

added theorem uniform_equicontinuous.closure'

added theorem uniform_equicontinuous.closure

added theorem uniform_equicontinuous.comp

added theorem uniform_equicontinuous.equicontinuous

added theorem uniform_equicontinuous.uniform_continuous

added def uniform_equicontinuous

added theorem uniform_equicontinuous_at_iff_range

added theorem uniform_equicontinuous_iff_uniform_continuous

added theorem uniform_inducing.equicontinuous_at_iff

added theorem uniform_inducing.equicontinuous_iff

added theorem uniform_inducing.uniform_equicontinuous_iff