Commit 2022-05-19 09:41 6906b6f7
View on Github →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.