Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-18 17:04 5f62d3bb

View on Github →

feat(topology/bounded_continuous_functions): more general uniform convergence (#2165)

feat(topology/buonded_continuous_functions): more general uniform convergence
yury's comments

Estimated changes

Modified src/topology/bounded_continuous_function.lean

modified def bounded_continuous_function

added theorem continuous_at_of_locally_uniform_limit_of_continuous_at

modified theorem continuous_of_locally_uniform_limit_of_continuous

modified theorem continuous_of_uniform_limit_of_continuous

added theorem continuous_on_of_locally_uniform_limit_of_continuous_on

added theorem continuous_on_of_uniform_limit_of_continuous_on

added theorem continuous_within_at_of_locally_uniform_limit_of_continuous_within_at

Modified src/topology/continuous_on.lean

added theorem continuous_on.continuous_at

added theorem continuous_on.continuous_within_at

added theorem continuous_on_empty

modified theorem continuous_on_iff_is_closed

Modified src/topology/metric_space/basic.lean

added theorem metric.ball_zero

added theorem metric.continuous_at_iff'

added theorem metric.continuous_on_iff'

added theorem metric.continuous_on_iff

added theorem metric.continuous_within_at_iff'

added theorem metric.continuous_within_at_iff

Modified src/topology/metric_space/emetric_space.lean

added theorem emetric.ball_zero