mathlib

65a44e6f - feat(analysis/normed_space/operator_norm): add 2 new versions of `op_norm_le_*` (#15417)

feat(analysis/normed_space/operator_norm): add 2 new versions of `op_norm_le_*` (#15417) * `continuous_linear_map.op_norm_le_bound'` requires an estimate on `∥f x∥` for any `x`, `∥x∥ ≠ 0`; * `continuous_linear_map.op_norm_le_of_unit_norm` works only for real linear map and requires that `∥f x∥ ≤ C` for all `x`, `∥x∥ = 1`.