Commit 2025-08-05 22:50 2530d06a
View on Github →feat(Analysis/NormedSpace/OperatorNorm): characterize the operator norm via sphere 0 1 (#27912)
Namely that sSup ((fun x => ‖f x‖₊) '' Metric.sphere 0 1) = ‖f‖₊, which we previously had for ball and closedBall.
From lean-matrix-cookbook