bump_function_inner): add `real.smooth_transition.proj_Icc` (#19097)

Commit

2 years ago

feat(analysis/calculus/bump_function_inner): add `real.smooth_transition.proj_Icc` (#19097) Also add `real.smooth_transition.continuous_at`. From the sphere eversion project

Author

urkud

Parents

c2258f7b

mathlib3 42e9a1fd - feat(analysis/calculus/bump_function_inner): add `real.smooth_transition.proj_Icc` (#19097)

mathlib3
42e9a1fd - feat(analysis/calculus/bump_function_inner): add `real.smooth_transition.proj_Icc` (#19097)