Commit 2026-03-05 00:53 891dd961

View on Github →

feat(ContinuousMultilinearMap): generalize some definitions (#34491) ... from normes spaces to topological vector spaces

Estimated changes

Modified Mathlib/Analysis/Normed/Module/Multilinear/Basic.lean

deleted def ContinuousLinearEquiv.continuousMultilinearMapCongrLeft

deleted theorem ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_apply

deleted theorem ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_symm

deleted def ContinuousLinearEquiv.continuousMultilinearMapCongrRight

deleted theorem ContinuousLinearEquiv.continuousMultilinearMapCongrRight_apply

deleted theorem ContinuousLinearEquiv.continuousMultilinearMapCongrRight_symm

deleted def ContinuousLinearMap.compContinuousMultilinearMapL

deleted def ContinuousMultilinearMap.compContinuousLinearMapL

deleted theorem ContinuousMultilinearMap.compContinuousLinearMapL_apply

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

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

added theorem continuous_of_tendsto_nhds_one

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

added def ContinuousLinearEquiv.continuousMultilinearMapCongrLeft

added theorem ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_apply

added theorem ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_symm

added def ContinuousLinearEquiv.continuousMultilinearMapCongrRight

added theorem ContinuousLinearEquiv.continuousMultilinearMapCongrRight_apply

added theorem ContinuousLinearEquiv.continuousMultilinearMapCongrRight_symm

added def ContinuousLinearMap.compContinuousMultilinearMapL

added theorem ContinuousLinearMap.compContinuousMultilinearMapL_apply

added def ContinuousMultilinearMap.compContinuousLinearMapL

added theorem ContinuousMultilinearMap.eventually_nhds_zero_mapsTo

added theorem ContinuousMultilinearMap.isVonNBounded_image2_apply

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