Prove existence of bump function for all epsilon #157212
Annotations
1 error and 2 warnings
check for unused imports
The process '/usr/bin/env' failed with exit code 1
|
check for unused imports:
Mathlib/MeasureTheory/Function/CompactDense.lean#L6
unused import (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)
|
check for unused imports:
Mathlib/MeasureTheory/Function/CompactDense.lean#L9
import #[Mathlib.Analysis.Convolution] instead
|
Loading