Theorem BoundedContinuousFunction.lipschitz_eval_const

Modification history

2025-11-29 16:30

Mathlib/Topology/ContinuousMap/Bounded/Basic.lean

feat: instantiate `ContinuousEval` for `BoundedContinuousFunction` (#32233)

Added BoundedContinuousFunction.lipschitz_eval_const View on Github →