Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous.clm_comp_const

Modification history

2022-06-05 14:52
src/analysis/normed_space/operator_norm.lean
feat(src/analysis/normed_space): various improvements for continuous bilinear maps (#14539) …
Added continuous.clm_comp_constView on Github →