From 9e0bb4b20b36bc625bbf1654e8c0e17e2efe3aa4 Mon Sep 17 00:00:00 2001
From: Joseph Myers <jsm@polyomino.org.uk>
Date: Mon, 22 Aug 2022 22:24:49 +0000
Subject: [PATCH 1/2] feat(analysis/special_functions/trigonometric/angle):
 continuity and signs
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Add the lemmas that `real.angle.sign` is continuous away from 0 and π,
and thus that any function to angles that is continuous on a connected
set and does not take the value 0 or π on that set produces angles
with constant sign on that set (this is a general principle for use in
proving results about when two oriented angles in a geometrical
configuration must have the same sign).
---
 .../trigonometric/angle.lean                  | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

diff --git a/src/analysis/special_functions/trigonometric/angle.lean b/src/analysis/special_functions/trigonometric/angle.lean
index 056fb76939a8c..345ad66a091db 100644
--- a/src/analysis/special_functions/trigonometric/angle.lean
+++ b/src/analysis/special_functions/trigonometric/angle.lean
@@ -6,7 +6,7 @@ Authors: Calle Sönne
 import analysis.special_functions.trigonometric.basic
 import algebra.char_zero.quotient
 import algebra.order.to_interval_mod
-import data.sign
+import topology.instances.sign
 
 /-!
 # The type of angles
@@ -521,6 +521,23 @@ lemma eq_iff_abs_to_real_eq_of_sign_eq {θ ψ : angle} (h : θ.sign = ψ.sign) :
   θ = ψ ↔ |θ.to_real| = |ψ.to_real| :=
 by simpa [h] using @eq_iff_sign_eq_and_abs_to_real_eq θ ψ
 
+lemma continuous_at_sign {θ : angle} (h0 : θ ≠ 0) (hpi : θ ≠ π) : continuous_at sign θ :=
+(continuous_at_sign_of_ne_zero (sin_ne_zero_iff.2 ⟨h0, hpi⟩)).comp continuous_sin.continuous_at
+
+/-- Suppose a function to angles is continuous on a connected set and never takes the values `0`
+or `π` on that set. Then the values of the function on that set all have the same sign. -/
+lemma sign_eq_of_continuous_on {α : Type*} [topological_space α] {f : α → angle} {s : set α}
+  {x y : α} (hc : is_connected s) (hf : continuous_on f s) (hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ π)
+  (hx : x ∈ s) (hy : y ∈ s) : (f y).sign = (f x).sign :=
+begin
+  have hf' : continuous_on (sign ∘ f) s,
+  { refine (continuous_at.continuous_on (λ θ hθ, _)).comp hf (set.maps_to_image f s),
+    obtain ⟨z, hz, rfl⟩ := hθ,
+    exact continuous_at_sign (hs _ hz).1 (hs _ hz).2 },
+  exact (hc.image _ hf').is_preconnected.subsingleton
+    (set.mem_image_of_mem _ hy) (set.mem_image_of_mem _ hx)
+end
+
 end angle
 
 end real

From 28df91b1de7c5a270637dc773081a05b75d65c83 Mon Sep 17 00:00:00 2001
From: Joseph Myers <jsm@polyomino.org.uk>
Date: Tue, 23 Aug 2022 17:36:49 +0000
Subject: [PATCH 2/2] Factor out continuous_on lemma.

---
 .../trigonometric/angle.lean                  | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

diff --git a/src/analysis/special_functions/trigonometric/angle.lean b/src/analysis/special_functions/trigonometric/angle.lean
index 345ad66a091db..a62838aba9a26 100644
--- a/src/analysis/special_functions/trigonometric/angle.lean
+++ b/src/analysis/special_functions/trigonometric/angle.lean
@@ -524,19 +524,22 @@ by simpa [h] using @eq_iff_sign_eq_and_abs_to_real_eq θ ψ
 lemma continuous_at_sign {θ : angle} (h0 : θ ≠ 0) (hpi : θ ≠ π) : continuous_at sign θ :=
 (continuous_at_sign_of_ne_zero (sin_ne_zero_iff.2 ⟨h0, hpi⟩)).comp continuous_sin.continuous_at
 
+lemma _root_.continuous_on.angle_sign_comp {α : Type*} [topological_space α] {f : α → angle}
+  {s : set α} (hf : continuous_on f s) (hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ π) :
+  continuous_on (sign ∘ f) s :=
+begin
+  refine (continuous_at.continuous_on (λ θ hθ, _)).comp hf (set.maps_to_image f s),
+  obtain ⟨z, hz, rfl⟩ := hθ,
+  exact continuous_at_sign (hs _ hz).1 (hs _ hz).2
+end
+
 /-- Suppose a function to angles is continuous on a connected set and never takes the values `0`
 or `π` on that set. Then the values of the function on that set all have the same sign. -/
 lemma sign_eq_of_continuous_on {α : Type*} [topological_space α] {f : α → angle} {s : set α}
   {x y : α} (hc : is_connected s) (hf : continuous_on f s) (hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ π)
   (hx : x ∈ s) (hy : y ∈ s) : (f y).sign = (f x).sign :=
-begin
-  have hf' : continuous_on (sign ∘ f) s,
-  { refine (continuous_at.continuous_on (λ θ hθ, _)).comp hf (set.maps_to_image f s),
-    obtain ⟨z, hz, rfl⟩ := hθ,
-    exact continuous_at_sign (hs _ hz).1 (hs _ hz).2 },
-  exact (hc.image _ hf').is_preconnected.subsingleton
-    (set.mem_image_of_mem _ hy) (set.mem_image_of_mem _ hx)
-end
+(hc.image _ (hf.angle_sign_comp hs)).is_preconnected.subsingleton
+  (set.mem_image_of_mem _ hy) (set.mem_image_of_mem _ hx)
 
 end angle