|
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
analysis/theories/hoelder.v
Line 370 in c5ea0ab
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 particulareminkowskimight be a misnommer.@CohenCyril @proux01 @hoheinzollern @t6s