Commit 2025-11-19 00:44 ddfe9337

View on Github →

feat(Topology/Algebra): the equivalence of continuous linear maps and UniformConvergenceCLM (#31756)

Estimated changes

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

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

added def ContinuousLinearMap.toUniformConvergenceCLM

added theorem ContinuousLinearMap.toUniformConvergenceCLM_apply

added theorem ContinuousLinearMap.toUniformConvergenceCLM_continuous

added theorem ContinuousLinearMap.toUniformConvergenceCLM_symm_apply