Def BoundedContinuousFunction.coeFnMonoidHom

Modification history

2026-10-21 11:53

Mathlib/Topology/ContinuousMap/Bounded/Basic.lean

feat: use `IsApply` for `BoundedContinuousFunction` (#45087)

Deleted BoundedContinuousFunction.coeFnMonoidHom View on Github →

2025-10-30 18:35

Mathlib/Topology/ContinuousMap/Bounded/Basic.lean

feat(BoundedContinuousFunction): multiplicative versions (#31089) …

Added BoundedContinuousFunction.coeFnMonoidHom View on Github →