mathlib3

445e6fc0 - refactor(topology/{basic,continuous_on}): review `continuous_if` etc (#6182)

refactor(topology/{basic,continuous_on}): review `continuous_if` etc (#6182) * move `continuous_if` to `topology/continuous_on`, use weaker assumptions; * add `piecewise` versions of various `if` lemmas; * add a specialized `continuous_if_le` version; * use dot notation for `continuous_on.if` and `continuous_on.if'`; * minor golfing here and there.