Commit 2021-02-13 09:47 445e6fc0

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.