Commit 2025-11-29 16:30 20a9b318

View on Github →

feat: instantiate ContinuousEval for BoundedContinuousFunction (#32233)

Estimated changes

Modified Mathlib/Topology/ContinuousMap/Bounded/Basic.lean

deleted theorem BoundedContinuousFunction.continuous_eval

deleted theorem BoundedContinuousFunction.continuous_eval_const

added theorem BoundedContinuousFunction.lipschitz_eval_const

deleted theorem BoundedContinuousFunction.lipschitz_evalx

Modified Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean