Commit 2025-05-16 09:05 aee86c3f

View on Github →

feat(Topology): add ContinuousOn union API lemmas (#22684) Add lemmas to allow going from continuity on two open sets to continuity on their union. Note that there is already an existing lemma for continuity on the union of two closed sets.

Estimated changes

Modified Mathlib/Topology/ContinuousOn.lean

deleted theorem ContinuousOn.union_isClosed

added theorem ContinuousOn.union_of_isClosed

added theorem ContinuousOn.union_of_isOpen

added theorem continouousOn_union_iff_of_isClosed

added theorem continouousOn_union_iff_of_isOpen