Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-06 15:34 ff910dca

View on Github →

feat(topology/bounded_continuous_function): composition of limits when uniform convergence (#2260)

feat(topology/bounded_continuous_function): composition of limits when uniform convergence
better statement
uniform space version
cleanup
fix linter
reviewer's comments

Estimated changes

Modified src/analysis/analytic/basic.lean

added theorem has_fpower_series_on_ball.tendsto_locally_uniformly_on'

added theorem has_fpower_series_on_ball.tendsto_locally_uniformly_on

added theorem has_fpower_series_on_ball.tendsto_uniformly_on'

added theorem has_fpower_series_on_ball.tendsto_uniformly_on

added theorem has_fpower_series_on_ball.uniform_geometric_approx

deleted theorem has_fpower_series_on_ball.uniform_limit

Modified src/data/real/nnreal.lean

added theorem nnreal.val_eq_coe

Modified src/topology/basic.lean

added theorem filter.eventually.self_of_nhds

Modified src/topology/bounded_continuous_function.lean

deleted theorem continuous_at_of_locally_uniform_limit_of_continuous_at

deleted theorem continuous_of_locally_uniform_limit_of_continuous

deleted theorem continuous_of_uniform_limit_of_continuous

deleted theorem continuous_on_of_locally_uniform_limit_of_continuous_on

deleted theorem continuous_on_of_uniform_limit_of_continuous_on

deleted theorem continuous_within_at_of_locally_uniform_limit_of_continuous_within_at

Modified src/topology/continuous_on.lean

added theorem filter.eventually.self_of_nhds_within

Modified src/topology/metric_space/basic.lean

added theorem metric.emetric_ball_nnreal

added theorem metric.emetric_closed_ball_nnreal

added theorem metric.tendsto_locally_uniformly_iff

added theorem metric.tendsto_locally_uniformly_on_iff

added theorem metric.tendsto_uniformly_iff

added theorem metric.tendsto_uniformly_on_iff

Modified src/topology/metric_space/emetric_space.lean

added theorem emetric.tendsto_locally_uniformly_iff

added theorem emetric.tendsto_locally_uniformly_on_iff

added theorem emetric.tendsto_uniformly_iff

added theorem emetric.tendsto_uniformly_on_iff

Modified src/topology/uniform_space/basic.lean

deleted theorem mem_nhds_uniformity_iff

added theorem mem_nhds_uniformity_iff_left

added theorem mem_nhds_uniformity_iff_right

added theorem uniform.continuous_at_iff'_left

added theorem uniform.continuous_at_iff'_right

added theorem uniform.continuous_iff'_left

added theorem uniform.continuous_iff'_right

added theorem uniform.continuous_on_iff'_left

added theorem uniform.continuous_on_iff'_right

added theorem uniform.continuous_within_at_iff'_left

added theorem uniform.continuous_within_at_iff'_right

added theorem uniform.tendsto_nhds_left

added theorem uniform.tendsto_nhds_right

Modified src/topology/uniform_space/cauchy.lean

Modified src/topology/uniform_space/separation.lean

Created src/topology/uniform_space/uniform_convergence.lean

added theorem continuous_at_of_locally_uniform_approx_of_continuous_at

added theorem continuous_of_locally_uniform_approx_of_continuous

added theorem continuous_of_uniform_approx_of_continuous

added theorem continuous_on_of_locally_uniform_approx_of_continuous_on

added theorem continuous_on_of_uniform_approx_of_continuous_on

added theorem continuous_within_at_of_locally_uniform_approx_of_continuous_within_at

added theorem tendsto_comp_of_locally_uniform_limit

added theorem tendsto_comp_of_locally_uniform_limit_within

added theorem tendsto_locally_uniformly.comp

added theorem tendsto_locally_uniformly.continuous

added theorem tendsto_locally_uniformly.tendsto_comp

added def tendsto_locally_uniformly

added theorem tendsto_locally_uniformly_on.comp

added theorem tendsto_locally_uniformly_on.continuous_on

added theorem tendsto_locally_uniformly_on.mono

added theorem tendsto_locally_uniformly_on.tendsto_comp

added def tendsto_locally_uniformly_on

added theorem tendsto_locally_uniformly_on_univ

added theorem tendsto_uniformly.comp

added theorem tendsto_uniformly.continuous

added theorem tendsto_uniformly.tendsto_comp

added theorem tendsto_uniformly.tendsto_locally_uniformly

added theorem tendsto_uniformly.tendsto_uniformly_on

added def tendsto_uniformly

added theorem tendsto_uniformly_on.comp

added theorem tendsto_uniformly_on.continuous_on

added theorem tendsto_uniformly_on.mono

added theorem tendsto_uniformly_on.tendsto_comp

added theorem tendsto_uniformly_on.tendsto_locally_uniformly_on

added def tendsto_uniformly_on

added theorem tendsto_uniformly_on_univ