Theorem ContinuousLinearMap.norm_single_le_one

Modification history

2025-08-08 00:06
Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean
feat: integrability in a product space (#27674) …
Added ContinuousLinearMap.norm_single_le_oneView on Github →