Commit 2025-07-05 16:53 93595bf1
View on Github →chore: rename continuous_iff_continuousOn_univ to continuousOn_univ (#26733)
This matches e.g. contDiffOn_univ, contMDiffOn_univ and (m)differentiableOn_univ.
Also flip the lemma and make it @[simp].
Zulip discussion