Mathlib Changelog
v4
Changelog
About
Github
Theorem
BoundedContinuousFunction.norm_integral_le_norm
Modification history
2023-09-27 23:08
Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean
feat: Lemmas about integrals of bounded continuous functions. (#7222) …
Added
BoundedContinuousFunction.norm_integral_le_norm
View on Github →