Theorem ContinuousLinearMap.opNorm_extend_le

Modification history

2024-02-27 00:53

Mathlib/Analysis/NormedSpace/OperatorNorm.lean

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

Modified ContinuousLinearMap.opNorm_extend_le View on Github →

2024-02-04 13:16

Mathlib/Analysis/NormedSpace/OperatorNorm.lean

chore: rename op_norm to opNorm (#10185)

Added ContinuousLinearMap.opNorm_extend_le View on Github →