feat(analysis/special_functions/trigonometric/angle): topology (#14969)

Give `real.angle` the structure of a `topological_add_group` (rather
than just an `add_comm_group`), so that it's possible to talk about
continuity for functions involving this type, and add associated
continuity lemmas for `coe : ℝ → angle`, `real.angle.sin` and
`real.angle.cos`.

src/analysis/special_functions/trigonometric/angle.lean

@@ -19,18 +19,19 @@ noncomputable theory
 namespace real
 
 /-- The type of angles -/
+@[derive [add_comm_group, topological_space, topological_add_group]]
 def angle : Type :=
 ℝ ⧸ (add_subgroup.zmultiples (2 * π))
 
 namespace angle
 
-instance angle.add_comm_group : add_comm_group angle :=
-quotient_add_group.add_comm_group _
-
 instance : inhabited angle := ⟨0⟩
 
 instance : has_coe ℝ angle := ⟨quotient_add_group.mk' _⟩
 
+@[continuity] lemma continuous_coe : continuous (coe : ℝ → angle) :=
+continuous_quotient_mk
+
 /-- Coercion `ℝ → angle` as an additive homomorphism. -/
 def coe_hom : ℝ →+ angle := quotient_add_group.mk' _
 
@@ -149,12 +150,18 @@ def sin (θ : angle) : ℝ := sin_periodic.lift θ
 @[simp] lemma sin_coe (x : ℝ) : sin (x : angle) = real.sin x :=
 rfl
 
+@[continuity] lemma continuous_sin : continuous sin :=
+continuous_quotient_lift_on' _ real.continuous_sin
+
 /-- The cosine of a `real.angle`. -/
 def cos (θ : angle) : ℝ := cos_periodic.lift θ
 
 @[simp] lemma cos_coe (x : ℝ) : cos (x : angle) = real.cos x :=
 rfl
 
+@[continuity] lemma continuous_cos : continuous cos :=
+continuous_quotient_lift_on' _ real.continuous_cos
+
 end angle
 
 end real