Commit 2022-04-25 06:23 91b80842

chore(analysis/normed_space/finite_dimension): extract some lemmas from existentials (#13600) A few proofs in this file prove an existential where a stronger statement in terms of the witness exists. This:

• Removes basis.sup_norm_le_norm and replaces it with the more general statement pi.sum_norm_apply_le_norm
• Renames basis.op_norm_le to basis.exists_op_norm_le
• Creates a new basis.op_norm_le stated without the existential
• Adds the nnnorm version of some norm lemmas. In some cases it's easier to prove these first, and derive the norm versions from them.