Def ContinuousLinearMap.postcomp_compactConvergenceCLM

Modification history

2025-12-11 11:46

Mathlib/Topology/Algebra/Module/StrongTopology.lean

feat: specialize `[pre, post]comp_uniformConvergenceCLM` to `CompactConvergenceCLM` (#32395)

Added ContinuousLinearMap.postcomp_compactConvergenceCLM View on Github →