Commit 2026-09-30 18:47 fe2d8262

View on Github →

feat(Topology/Algebra): continuity of composing by a ContinuousAffineMap (#43339) This allows upgrading signedDist to a ContinuousAffineMap.

Estimated changes

Modified Mathlib/Geometry/Euclidean/SignedDist.lean

Modified Mathlib/Topology/Algebra/ContinuousAffineMap/Topology.lean

added theorem ContinuousAffineMap.continuous_postcomp

added theorem ContinuousAffineMap.continuous_precomp

added def ContinuousAffineMap.postcompA

added theorem ContinuousAffineMap.postcompA_apply

added theorem ContinuousAffineMap.postcompA_contLinear

added def ContinuousAffineMap.precompA

added theorem ContinuousAffineMap.precompA_apply

added theorem ContinuousAffineMap.precompA_contLinear

added def ContinuousAffineMap.precompL

added theorem ContinuousAffineMap.precompL_toContinuousAffineMap

added def ContinuousLinearMap.postcompContinuousAffineMap

added theorem ContinuousLinearMap.postcompContinuousAffineMap_toContinuousAffineMap