mathlib3
e968b6d1 - feat(topology/continuous_function/bounded): add `bounded_continuous_function.tendsto_iff_tendsto_uniformly` (#12894)

Commit
3 years ago
feat(topology/continuous_function/bounded): add `bounded_continuous_function.tendsto_iff_tendsto_uniformly` (#12894) This establishes that convergence in the metric on bounded continuous functions is equivalent to uniform convergence of the respective functions.
Author
Parents
Loading