Theorem ContinuousMapZero.integral_apply

Modification history

2025-04-15 08:42

Mathlib/MeasureTheory/Integral/Bochner/ContinuousLinearMap.lean

chore: split `MeasureTheory.Integral.SetIntegral` (#24070) …

Modified ContinuousMapZero.integral_apply View on Github →

2024-08-29 21:20

Mathlib/MeasureTheory/Integral/SetIntegral.lean

feat(ContinuousFunctionalCalculus): show that the non-unital CFC commutes with integration (#16255) …

Added ContinuousMapZero.integral_apply View on Github →