Commit 2023-05-29 23:41 5519d19e

View on Github →

feat: forward-port 19107 (#4470) Forward-port leanprover-community/mathlib#19107

Estimated changes

Modified Mathlib/Analysis/NormedSpace/OperatorNorm.lean

deleted def ContinuousLinearEquiv.arrowCongr

deleted def ContinuousLinearEquiv.arrowCongrSL

Modified Mathlib/Analysis/NormedSpace/PiLp.lean

deleted theorem PiLp.continuousLinearEquiv_invFun

Modified Mathlib/Topology/Algebra/Module/Basic.lean

Modified Mathlib/Topology/Algebra/Module/StrongTopology.lean

added def ContinuousLinearEquiv.arrowCongr

added def ContinuousLinearEquiv.arrowCongrSL

added def ContinuousLinearEquiv.arrowCongrₛₗ

added theorem ContinuousLinearEquiv.arrowCongrₛₗ_continuous

Modified Mathlib/Topology/Constructions.lean

added theorem inducing_const_prod

added theorem inducing_prod_const

Modified Mathlib/Topology/FiberBundle/Basic.lean

deleted def FiberPrebundle.fiberTopology

deleted theorem FiberPrebundle.inducing_totalSpaceMk

added theorem FiberPrebundle.inducing_totalSpaceMk_of_inducing_comp

modified def FiberPrebundle.toFiberBundle

Modified Mathlib/Topology/VectorBundle/Basic.lean

deleted def VectorPrebundle.fiberTopology

deleted theorem VectorPrebundle.inducing_totalSpaceMk

modified def VectorPrebundle.toFiberBundle