Theorems · Definition · real analysis
Real.smoothTransition
ℝ → ℝ
An infinitely smooth function f : ℝ → ℝ such that f x = 0 for x ≤ 0,
f x = 1 for 1 ≤ x, and 0 < f x < 1 for 0 < x < 1.
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 144 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.
- Realstatement and proof · cited by 25,697
- expNegInvGlueproof · cited by 17
Cited by18
Results whose statement or proof uses this declaration.
- Real.smoothTransition.contDiffstatement · cited by 3
- Real.smoothTransition.one_of_one_lestatement · cited by 3
- Manifold.exists_lt_locally_constant_of_riemannianEDist_ltproof · cited by 3
- Real.smoothTransition.zero_of_nonposstatement · cited by 2
- Real.smoothTransition.continuousstatement · cited by 1
- Real.smoothTransition.le_onestatement · cited by 1
- Real.smoothTransition.lt_one_of_lt_onestatement · cited by 1
- Real.smoothTransition.monotonestatement · cited by 1
- Real.smoothTransition.nonnegstatement · cited by 1
- Real.smoothTransition.onestatement · cited by 1
- Real.smoothTransition.zerostatement · cited by 1
- Real.smoothTransition.zero_iff_nonposstatement · cited by 1