Commit 2024-03-05 08:34 f8120d5e

View on Github →

feat(OperatorNorm/Prod): norm of first/second projection (#11002) Operator norm of the projection maps E × F → E and E × F → F for (semi)normed spaces

Estimated changes

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean

added theorem ContinuousLinearMap.norm_fst

added theorem ContinuousLinearMap.norm_fst_le

added theorem ContinuousLinearMap.norm_snd

added theorem ContinuousLinearMap.norm_snd_le

modified theorem ContinuousLinearMap.opNNNorm_prod

modified theorem ContinuousLinearMap.opNorm_prod

modified def ContinuousLinearMap.prodₗᵢ