feat: add Set.IccExtend_eq_self (#4454)

Partial forward-port of leanprover-community/mathlib#19097 Also rename `Set.Icc_extend_coe` to `Set.IccExtend_val`.
leanprover-community · May 28, 2023 · 0f5133e · 0f5133e
1 parent 115b6c3
commit 0f5133e
Show file tree

Hide file tree

Showing 4 changed files with 19 additions and 6 deletions.
diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
@@ -57,7 +57,7 @@ theorem neg_pi_div_two_le_arcsin (x : ℝ) : -(π / 2) ≤ arcsin x :=
 #align real.neg_pi_div_two_le_arcsin Real.neg_pi_div_two_le_arcsin
 
 theorem arcsin_projIcc (x : ℝ) : arcsin (projIcc (-1) 1 (neg_le_self zero_le_one) x) = arcsin x :=
-  by rw [arcsin, Function.comp_apply, Icc_extend_coe, Function.comp_apply, IccExtend,
+  by rw [arcsin, Function.comp_apply, IccExtend_val, Function.comp_apply, IccExtend,
         Function.comp_apply]
 #align real.arcsin_proj_Icc Real.arcsin_projIcc
 

diff --git a/Mathlib/Data/Set/Intervals/ProjIcc.lean b/Mathlib/Data/Set/Intervals/ProjIcc.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov, Patrick Massot
 
 ! This file was ported from Lean 3 source module data.set.intervals.proj_Icc
-! leanprover-community/mathlib commit aba57d4d3dae35460225919dcd82fe91355162f9
+! leanprover-community/mathlib commit 42e9a1fd3a99e10f82830349ba7f4f10e8961c2a
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -135,9 +135,22 @@ theorem IccExtend_of_mem (f : Icc a b → β) (hx : x ∈ Icc a b) : IccExtend h
 #align set.Icc_extend_of_mem Set.IccExtend_of_mem
 
 @[simp]
-theorem Icc_extend_coe (f : Icc a b → β) (x : Icc a b) : IccExtend h f x = f x :=
+theorem IccExtend_val (f : Icc a b → β) (x : Icc a b) : IccExtend h f x = f x :=
   congr_arg f <| projIcc_val h x
-#align set.Icc_extend_coe Set.Icc_extend_coe
+#align set.Icc_extend_coe Set.IccExtend_val
+
+/-- 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. -/
+theorem IccExtend_eq_self (f : α → β) (ha : ∀ x < a, f x = f a) (hb : ∀ x, b < x → f x = f b) :
+    IccExtend h (f ∘ (↑)) = f := by
+  ext x
+  cases' lt_or_le x a with hxa hax
+  · simp [IccExtend_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 [IccExtend_val, comp_apply]
+    · simp [IccExtend_of_right_le _ _ hbx.le, hb x hbx]
+#align set.Icc_extend_eq_self Set.IccExtend_eq_self
 
 end Set
 

diff --git a/Mathlib/Topology/Homotopy/Basic.lean b/Mathlib/Topology/Homotopy/Basic.lean
@@ -185,7 +185,7 @@ theorem extend_apply_of_one_le (F : Homotopy f₀ f₁) {t : ℝ} (ht : 1 ≤ t)
 
 @[simp]
 theorem extend_apply_coe (F : Homotopy f₀ f₁) (t : I) (x : X) : F.extend t x = F (t, x) :=
-  ContinuousMap.congr_fun (Set.Icc_extend_coe (zero_le_one' ℝ) F.curry t) x
+  ContinuousMap.congr_fun (Set.IccExtend_val (zero_le_one' ℝ) F.curry t) x
 #align continuous_map.homotopy.extend_apply_coe ContinuousMap.Homotopy.extend_apply_coe
 
 @[simp]

diff --git a/Mathlib/Topology/PathConnected.lean b/Mathlib/Topology/PathConnected.lean
@@ -277,7 +277,7 @@ theorem extend_one : γ.extend 1 = y := by simp
 @[simp]
 theorem extend_extends' {X : Type _} [TopologicalSpace X] {a b : X} (γ : Path a b)
     (t : (Icc 0 1 : Set ℝ)) : γ.extend t = γ t :=
-  Icc_extend_coe _ γ t
+  IccExtend_val _ γ t
 #align path.extend_extends' Path.extend_extends'
 
 @[simp]