Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-09 14:41 aa9e2b8f

View on Github →

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

Estimated changes

Modified src/analysis/normed_space/operator_norm.lean

added theorem continuous_linear_map.le_op_norm₂

added theorem continuous_linear_map.op_norm_le_bound₂

modified theorem linear_isometry.norm_to_continuous_linear_map

modified theorem linear_isometry.norm_to_continuous_linear_map_le

added theorem linear_map.mk_continuous_norm_le'

modified theorem linear_map.mk_continuous_norm_le

added def linear_map.mk_continuous₂

added theorem linear_map.mk_continuous₂_apply

added theorem linear_map.mk_continuous₂_norm_le'

added theorem linear_map.mk_continuous₂_norm_le