Theorems · Definition · real analysis
expNegInvGlue
ℝ → ℝ
expNegInvGlue is the real function given by x ↦ exp (-1/x) for x > 0 and 0
for x ≤ 0. It is a basic building block to construct smooth partitions of unity. Its main property
is that it vanishes for x ≤ 0, it is positive for x > 0, and the junction between the two
behaviors is flat enough to retain smoothness. The fact that this function is C^∞ is proved in
expNegInvGlue.contDiff.
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 143 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by18
Results whose statement or proof uses this declaration.
- Real.smoothTransitionproof · cited by 17
- Real.smoothTransition.pos_denomstatement · cited by 8
- expNegInvGlue.zero_of_nonposstatement · cited by 6
- expNegInvGlue.pos_of_posstatement · cited by 5
- expNegInvGlue.nonnegstatement · cited by 4
- Real.smoothTransition.one_of_one_leproof · cited by 3
- expNegInvGlue.differentiable_polynomial_eval_inv_mulstatement · cited by 2
- expNegInvGlue.hasDerivAt_polynomial_eval_inv_mulstatement and proof · cited by 2
- Real.smoothTransition.lt_one_of_lt_oneproof · cited by 1
- Real.smoothTransition.monotoneproof · cited by 1
- expNegInvGlue.contDiffstatement and proof · cited by 1
- expNegInvGlue.contDiff_polynomial_eval_inv_mulstatement and proof · cited by 1