Commit 2024-04-10 20:53 58eba780

View on Github →

feat(Multilinear/Topology): define topology on ContinuousMultilinearMaps (#10777) Define UniformSpace instance that doesn't depend on the norm, replace uniformity in the SeminormedAddCommGroup instance.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/NormedSpace/HahnBanach/SeparatingDual.lean

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

deleted def ContinuousMultilinearMap.apply

deleted theorem ContinuousMultilinearMap.apply_apply

deleted theorem ContinuousMultilinearMap.continuous_eval_left

deleted theorem ContinuousMultilinearMap.hasSum_eval

deleted theorem ContinuousMultilinearMap.tsum_eval

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

added def ContinuousMultilinearMap.apply

added theorem ContinuousMultilinearMap.apply_apply

added theorem ContinuousMultilinearMap.continuous_coe_fun

added theorem ContinuousMultilinearMap.continuous_eval_const

added theorem ContinuousMultilinearMap.embedding_toUniformOnFun

added theorem ContinuousMultilinearMap.hasBasis_nhds_zero

added theorem ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis

added theorem ContinuousMultilinearMap.hasSum_eval

added def ContinuousMultilinearMap.toUniformOnFun

added theorem ContinuousMultilinearMap.toUniformOnFun_toFun

added theorem ContinuousMultilinearMap.tsum_eval

added theorem ContinuousMultilinearMap.uniformContinuous_coe_fun

added theorem ContinuousMultilinearMap.uniformContinuous_eval_const

added theorem ContinuousMultilinearMap.uniformEmbedding_toUniformOnFun