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

Commit

4 years ago

feat(analysis/normed_space/operator_norm): lemmas about `E →L[𝕜] F →L[𝕜] G` (#6102) Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Author

urkud

Parents