mathlib
54349530 - feat(topology/continuous_on): Continuity on an open (#17089)

Commit

3 years ago

feat(topology/continuous_on): Continuity on an open (#17089) A function is `continuous_on` an open iff it's `continuous_at` every of its points.

Author

YaelDillies

Parents