lipschitz): continuity on product of continuity in 1 var and Lipschitz continuity in another (#9758)

Commit

4 years ago

feat(topology/metric_space/lipschitz): continuity on product of continuity in 1 var and Lipschitz continuity in another (#9758) Also apply the new lemma to `continuous_bounded_map`s and add a few lemmas there.

Author

urkud

Parents

939e8b9a

mathlib3 59db9032 - feat(topology/metric_space/lipschitz): continuity on product of continuity in 1 var and Lipschitz continuity in another (#9758)

mathlib3
59db9032 - feat(topology/metric_space/lipschitz): continuity on product of continuity in 1 var and Lipschitz continuity in another (#9758)