Theorem ContinuousLinearMap.postcompContinuousAffineMap_toContinuousAffineMap

Modification history

2026-09-30 18:47
Mathlib/Topology/Algebra/ContinuousAffineMap/Topology.lean
feat(Topology/Algebra): continuity of composing by a `ContinuousAffineMap` (#43339) …
Added ContinuousLinearMap.postcompContinuousAffineMap_toContinuousAffineMapView on Github →