Double-check local notations in `hoelder.v`

[affeldt-aist]

analysis/theories/hoelder.v

Line 370 in c5ea0ab

Local Notation "'N_ p [ f ]" := (Lnorm mu p (EFin \o f)).

Lemmas relying on this specialization should be future proof for when the restriction on the argument of the norm is lifted, i.e., when this becomes Local Notation "'N_ p [ f ]" := (Lnorm mu p f), in particular eminkowski might be a misnommer.

@CohenCyril @proux01 @hoheinzollern @t6s