Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous.const_clm_comp

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.const_clm_compView on Github →