Theorem ContinuousLinearMap.exists_lt_apply_of_lt_op_norm
Modification history
2024-02-04 13:16
Mathlib/Analysis/NormedSpace/OperatorNorm.lean
chore: rename op_norm to opNorm (#10185)
Deleted ContinuousLinearMap.exists_lt_apply_of_lt_op_normView on Github →