Commit 2026-05-19 19:46 85ee9578

View on Github →

feat(Analysis): operator norm of a LinearIsometryEquiv (#39143) Also generalise a bunch of lemmas from NormedAddCommGroup + Nontrivial to SeminormedAddCommGroup + NontrivialTopology. From MeanFourier

Estimated changes

Modified Mathlib/Analysis/Normed/Operator/NormedSpace.lean

modified theorem ContinuousLinearMap.norm_inl

modified theorem ContinuousLinearMap.norm_inr

modified theorem ContinuousLinearMap.norm_single

modified def IsCoercive

modified theorem LinearIsometry.enorm_toContinuousLinearMap

modified theorem LinearIsometry.nnnorm_toContinuousLinearMap

modified theorem LinearIsometry.norm_toContinuousLinearMap

modified theorem LinearIsometry.norm_toContinuousLinearMap_comp

added theorem LinearIsometryEquiv.enorm_toContinuousLinearMap

added theorem LinearIsometryEquiv.nnnorm_toContinuousLinearMap

added theorem LinearIsometryEquiv.norm_toContinuousLinearMap

Modified Mathlib/Topology/ContinuousMap/Compact.lean

Modified Mathlib/Topology/Order.lean

added theorem Nontrivial.of_nontrivialTopology