Commit 2025-05-19 07:32 ec3711de

View on Github →

chore(Topology/ContinuousMap): remove assumptions (#24985)

  • ContinuousSMul R C(α, M) and ContinuousConstSMul R C(α, M) no longer needs LocallyCompactSpace α.
  • ContinuousLinearMap.compLeftContinuous is upgraded to a continuous linear map.
  • ContinuousLinearMap.compLeftContinuousCompact is removed because it is a special case of the new ContinuousLinearMap.compLeftContinuous.
  • Also added ContinuousLinearMap.const : M →L[R] C(α, M).

Estimated changes