Normal form for constant functions

Stream: mathlib4

[Michael Rothgang]

Mathlib is slightly inconsistent about stating lemmas "a constant function has property X": mostly, we use fun _ => c. Examples: docs#continuous_const, docs#differentiable_const, docs#contDiff_const
docs#contMDiff_const, docs#mdifferentiable_const, docs#measurable_const, docs#aemeasurable_const, docs#MeasureTheory.aestronglyMeasurable_const (notice the different namespace; should this be fixed?), docs#monotone_const

In the other direction, we have much fewer examples: the following is exhaustive. We have docs#Function.const_mono and docs#Function.const_strictMono, docs#Function.smul_const, docs#Function.one_le_const, docs#isClosedMap_const, docs#fderiv_const, docs#fderivWithin_const, docs#derivWithin_const (and are missing deriv_const), docs#HolderWith.const.

We have a few constructions like SimpleFunc.const, AffineMap.const or ContinuousMap.const, but these are not the norm either.

Should we standardise this one way or the other? One historical reason could have been that fun_prop did not support Function.const as well; this is fixed now.

[Ruben Van de Velde]

The other direction is docs#Function.const

It seems much less likely to occur naturally in a goal, so my impression is that fun _ => c will be more useful