feat(analysis/calculus/bump_function_inner): add `real.smooth_transit…

…ion.proj_Icc` (#19097)

Also add `real.smooth_transition.continuous_at`.

From the sphere eversion project

src/analysis/calculus/bump_function_inner.lean

@@ -236,6 +236,16 @@ zero_of_nonpos le_rfl
 @[simp] protected lemma one : smooth_transition 1 = 1 :=
 one_of_one_le le_rfl
 
+/-- Since `real.smooth_transition` is constant on $(-∞, 0]$ and $[1, ∞)$, applying it to the
+projection of `x : ℝ` to $[0, 1]$ gives the same result as applying it to `x`. -/
+@[simp] protected lemma proj_Icc :
+  smooth_transition (proj_Icc (0 : ℝ) 1 zero_le_one x) = smooth_transition x :=
+begin
+  refine congr_fun (Icc_extend_eq_self zero_le_one smooth_transition (λ x hx, _) (λ x hx, _)) x,
+  { rw [smooth_transition.zero, zero_of_nonpos hx.le] },
+  { rw [smooth_transition.one, one_of_one_le hx.le] }
+end
+
 lemma le_one (x : ℝ) : smooth_transition x ≤ 1 :=
 (div_le_one (pos_denom x)).2 $ le_add_of_nonneg_right (nonneg _)
 
@@ -260,6 +270,9 @@ smooth_transition.cont_diff.cont_diff_at
 protected lemma continuous : continuous smooth_transition :=
 (@smooth_transition.cont_diff 0).continuous
 
+protected lemma continuous_at : continuous_at smooth_transition x :=
+smooth_transition.continuous.continuous_at
+
 end smooth_transition
 
 end real

src/data/set/intervals/proj_Icc.lean

@@ -114,6 +114,20 @@ congr_arg f $ proj_Icc_of_mem h hx
   Icc_extend h f x = f x :=
 congr_arg f $ proj_Icc_coe h x
 
+/-- If `f : α → β` is a constant both on $(-∞, a]$ and on $[b, +∞)$, then the extension of this
+function from $[a, b]$ to the whole line is equal to the original function. -/
+lemma Icc_extend_eq_self (f : α → β) (ha : ∀ x < a, f x = f a) (hb : ∀ x, b < x → f x = f b) :
+  Icc_extend h (f ∘ coe) = f :=
+begin
+  ext x,
+  cases lt_or_le x a with hxa hax,
+  { simp [Icc_extend_of_le_left _ _ hxa.le, ha x hxa] },
+  { cases le_or_lt x b with hxb hbx,
+    { lift x to Icc a b using ⟨hax, hxb⟩,
+      rw [Icc_extend_coe] },
+    { simp [Icc_extend_of_right_le _ _ hbx.le, hb x hbx] } }
+end
+
 end set
 
 open set