Commit 2025-03-07 15:46 ea26f90f

View on Github →

chore(Topology/ContinuousOn): re-use variables (#22691)

Estimated changes

Modified Mathlib/Topology/ContinuousOn.lean

modified theorem Continuous.comp_continuousOn'

modified theorem ContinuousOn.union_continuousAt

modified theorem ContinuousOn.union_isClosed

modified theorem eventually_nhdsWithin_of_eventually_nhds

modified theorem nhdsWithin_prod