Commit 2024-02-14 07:40 98a6b538

View on Github →

chore: redistribute tags for fun_prop regarding continuity across the library (#10494)

Estimated changes

deleted theorem Continuous.div₀
deleted theorem ContinuousAt.comp'
deleted theorem ContinuousAt.div₀
deleted theorem ContinuousOn.comp''
deleted theorem ContinuousOn.div₀
deleted theorem continuousAt_id'
deleted theorem continuousAt_pi'
deleted theorem continuousOn_apply
deleted theorem continuousOn_id'
deleted theorem continuousOn_pi'
added theorem Continuous.div₀
added theorem ContinuousAt.div₀
added theorem ContinuousOn.div₀
added theorem ContinuousAt.comp'
added theorem continuousAt_id'
added theorem continuousAt_pi'
added theorem ContinuousOn.comp''
added theorem continuousOn_apply
added theorem continuousOn_id'
added theorem continuousOn_pi'