feat(analysis/normed_space/operator_norm): lemmas about `E →L[𝕜] F →L[𝕜] G` (#6102)
feat(analysis/normed_space/operator_norm): lemmas about `E →L[𝕜] F →L[𝕜] G` (#6102)



Co-authored-by: Bryan Gin-ge Chen <6e05157ce10643a7cfc5a3d4e29e4fa5cffe1fc6@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib