Theorem BoundedContinuousFunction.mul_apply

Modification history

2024-05-19 19:30

Mathlib/Topology/ContinuousFunction/Bounded.lean

feat: BoundedMul class to generalize multiplication of bounded continuous functions. (#12790) …

Modified BoundedContinuousFunction.mul_apply View on Github →

2023-05-21 21:51

Mathlib/Topology/ContinuousFunction/Bounded.lean

feat: port Topology.ContinuousFunction.Bounded (#4075)

Added BoundedContinuousFunction.mul_apply View on Github →