Theorem ContinuousLinearMap.op_nnnorm_eq_of_bounds

Modification history

2024-02-04 13:16

Mathlib/Analysis/NormedSpace/OperatorNorm.lean

chore: rename op_norm to opNorm (#10185)

Deleted ContinuousLinearMap.op_nnnorm_eq_of_bounds View on Github →

2024-01-06 05:23

Mathlib/Analysis/NormedSpace/OperatorNorm.lean

fix(Analysis/NormedSpace/OperatorNorm): muddled norm and nnnorm (#9473) …

Modified ContinuousLinearMap.op_nnnorm_eq_of_bounds View on Github →

2023-05-17 20:21

Mathlib/Analysis/NormedSpace/OperatorNorm.lean

feat: port Analysis.NormedSpace.OperatorNorm (#3903)

Added ContinuousLinearMap.op_nnnorm_eq_of_bounds View on Github →