Theorem ContinuousLinearMap.dist_le_opNorm

Modification history

2024-02-27 00:53

Mathlib/Analysis/NormedSpace/OperatorNorm.lean

chore(Analysis/NormedSpace): split up OperatorNorm.lean (#10990) …

Modified ContinuousLinearMap.dist_le_opNorm View on Github →

2024-02-04 13:16

Mathlib/Analysis/NormedSpace/OperatorNorm.lean

chore: rename op_norm to opNorm (#10185)

Added ContinuousLinearMap.dist_le_opNorm View on Github →