Commit 2026-10-21 11:53 903930a2

View on Github →

feat: use IsApply for BoundedContinuousFunction (#45087)

Estimated changes

Modified Mathlib/Analysis/Fourier/FourierTransform.lean

Modified Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean

Modified Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

deleted theorem MeasureTheory.FiniteMeasure.smul_apply

Modified Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean

Modified Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

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

deleted def BoundedContinuousFunction.coeFnMonoidHom

deleted theorem BoundedContinuousFunction.coe_mul

deleted theorem BoundedContinuousFunction.coe_one

deleted theorem BoundedContinuousFunction.coe_pow

deleted theorem BoundedContinuousFunction.coe_prod

deleted theorem BoundedContinuousFunction.coe_smul

deleted theorem BoundedContinuousFunction.coe_sub

deleted theorem BoundedContinuousFunction.intCast_apply

deleted theorem BoundedContinuousFunction.mul_apply

deleted theorem BoundedContinuousFunction.natCast_apply

deleted theorem BoundedContinuousFunction.pow_apply

deleted theorem BoundedContinuousFunction.prod_apply

deleted theorem BoundedContinuousFunction.smul_apply

deleted theorem BoundedContinuousFunction.sub_apply

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

deleted theorem BoundedContinuousFunction.coe_intCast

deleted theorem BoundedContinuousFunction.coe_natCast

deleted theorem BoundedContinuousFunction.coe_neg

deleted theorem BoundedContinuousFunction.coe_zsmul

deleted theorem BoundedContinuousFunction.neg_apply

deleted theorem BoundedContinuousFunction.zsmul_apply

Modified Mathlib/Topology/ContinuousMap/BoundedCompactlySupported.lean

Modified Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean

Modified Mathlib/Topology/UrysohnsBounded.lean