Theorem ContDiffBump.normed_le_div_measure_closedBall_rIn

Modification history

2024-08-09 00:58

Mathlib/Analysis/Calculus/BumpFunction/Normed.lean

chore: backports for leanprover/lean4#4814 (part 34) (#15607)

Modified ContDiffBump.normed_le_div_measure_closedBall_rIn View on Github →

2023-07-30 12:08

Mathlib/Analysis/Calculus/BumpFunction/Normed.lean

feat: The convolution of a locally integrable function f with a sequence of bump functions converges ae to f (#6102)

Added ContDiffBump.normed_le_div_measure_closedBall_rIn View on Github →