Shorter notation for ContinuousWithinAt, DifferentiableWithi

Stream: mathlib4

[Michael Rothgang]

In #mathlib4 > Differential geometry elaborators experiment, @Sébastien Gouëzel proposed using shorter notation for ContMDiffWithinAt (or rather, its custom elaborator), namely writing CMAt[s] f x for ContMDiffWithinAt f s x. I like that a lot, which is why the elaborators implement this. However, this makes me wonder: should we do something similar to ContinuousWithinAt and DifferentiableWithinAt?

[Michael Rothgang]

For example, we could have new notation

• in the Topology namespace: ContinuousAt[s] f x for ContinuousWithinAt f s x (analogous to 𝓝[s] x for nhdsWithin x s),
• in the ContDiff namespace: DifferentiableAt[s] f x (or even DiffAt, though perhaps that's too short) for DifferentiableWithinAt f s x

What do you think? CC @Patrick Massot @Yury G. Kudryashov @Heather Macbeth @Floris van Doorn

[Sébastien Gouëzel]

I think that the elaborators are really justified in manifold theory as they make it possible to hide the model with corners. In other parts of the library where there is no such issue, they're probably less useful: a good notation can definitely be nice, but it's also one more thing to learn and another source of confusion for newcomers.

[Michael Rothgang]

I agree with your point. The counter-argument is that this loses a bit of consistency --- as you'd haveDifferentiableWithinAt f s x but MDiffAt[s] f x.