mathlib

6906b6f7 - feat(analysis/normed_space/pi_Lp): add missing nnnorm lemmas (#14221)

feat(analysis/normed_space/pi_Lp): add missing nnnorm lemmas (#14221) This renames `pi_Lp.dist` to `pi_Lp.dist_eq` and `pi_Lp.edist` to `pi_Lp.edist_eq` to match `pi_Lp.norm_eq`. The `nndist` version of these lemmas is new. The `pi_Lp.norm_eq_of_L2` lemma was not stated at the correct generality, and has been moved to an earlier file where doing so is easier. The `nnnorm` version of this lemma is new. Also replaces some `∀` binders with `Π` to match the pretty-printer, and tidies some whitespace.