Commit 2024-10-27 20:54 c57a78f1

View on Github →

feat(Topology/Algebra): generalize CompleteSpace instances (#17244)

Estimated changes

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

added theorem ContinuousAlternatingMap.isUniformInducing_postcomp

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

added theorem ContinuousLinearMap.range_coeFn_eq

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

modified theorem ContinuousMultilinearMap.embedding_toUniformOnFun

added theorem ContinuousMultilinearMap.isUniformInducing_postcomp

added theorem ContinuousMultilinearMap.isUniformInducing_toUniformOnFun

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

added theorem ContinuousLinearMap.completeSpace

added theorem UniformConvergenceCLM.completeSpace

added theorem UniformConvergenceCLM.isUniformInducing_coeFn

added theorem UniformConvergenceCLM.isUniformInducing_postcomp

modified def UniformConvergenceCLM