2022-10-24 21:05
src/analysis/normed_space/operator_norm.lean
feat(analysis/normed_space/operator_norm): characterize the operator norm over a `densely_normed_field` in terms of the supremum (#16963) …
Added continuous_linear_map.exists_lt_apply_of_lt_op_norm