Def BoundedContinuousFunction.toContinuousMapMonoidHom

Modification history

2025-10-30 18:35
Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
feat(BoundedContinuousFunction): multiplicative versions (#31089) …
Added BoundedContinuousFunction.toContinuousMapMonoidHomView on Github →