We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Analysis.Calculus.BumpFunctionInner
There are several sections in this file that can be moved to different files to reduce imports:
Analysis.Calculus.SmoothTransition
Real.expInvGlue
Real.smoothTransition
Analysis.Calculus.BumpFunction.Basic
HasContDiffBump
ContDiffBump
Analysis.Calculus.BumpFunction.Inner
Analysis.Calculus.BumpFunction.Normed
BumpFunction.normed
The text was updated successfully, but these errors were encountered:
BumpFunctionInner
2a2e08c
refactor: split BumpFunctionInner (#5940)
784034b
Fixes #4755
Successfully merging a pull request may close this issue.
There are several sections in this file that can be moved to different
files to reduce imports:
Analysis.Calculus.SmoothTransition
: definitions and lemmas aboutReal.expInvGlue
andReal.smoothTransition
.Analysis.Calculus.BumpFunction.Basic
: definition of the typeclassHasContDiffBump
and properties ofContDiffBump
.Analysis.Calculus.BumpFunction.Inner
: an instance for innerproduct spaces.
Analysis.Calculus.BumpFunction.Normed
: definition and lemmas aboutBumpFunction.normed
; this is the only file that will importmeasure theory.
The text was updated successfully, but these errors were encountered: