Commit 2025-08-06 01:05 edfb965a

View on Github →

refactor(Analysis/NormedSpace/OperatorNorm): rearrange variables (#28012) As requested in #27912.

Estimated changes

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean

modified theorem ContinuousLinearMap.exists_lt_apply_of_lt_opNNNorm

modified theorem ContinuousLinearMap.exists_lt_apply_of_lt_opNorm

modified theorem ContinuousLinearMap.exists_nnnorm_eq_one_lt_apply_of_lt_opNNNorm

modified theorem ContinuousLinearMap.isLeast_opNNNorm

modified theorem ContinuousLinearMap.le_opENorm

modified theorem ContinuousLinearMap.le_opNNNorm

modified theorem ContinuousLinearMap.lipschitz

modified theorem ContinuousLinearMap.nndist_le_opNNNorm

modified theorem ContinuousLinearMap.opENorm_comp_le

modified theorem ContinuousLinearMap.opNNNorm_comp_le

modified theorem ContinuousLinearMap.sSup_sphere_eq_nnnorm

modified theorem ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm

modified theorem ContinuousLinearMap.sSup_unitClosedBall_eq_norm

modified theorem ContinuousLinearMap.sSup_unit_ball_eq_nnnorm

modified theorem ContinuousLinearMap.sSup_unit_ball_eq_norm