feat: port Analysis.Normed.Group.BallSphere (#2771)

Mathlib.lean

@@ -241,6 +241,7 @@ import Mathlib.Algebra.Support
 import Mathlib.Algebra.Tropical.Basic
 import Mathlib.Algebra.Tropical.BigOperators
 import Mathlib.Algebra.Tropical.Lattice
+import Mathlib.Analysis.Normed.Group.BallSphere
 import Mathlib.Analysis.Normed.Group.Basic
 import Mathlib.Analysis.Normed.Group.Completion
 import Mathlib.Analysis.Normed.Group.Hom

Mathlib/Analysis/Normed/Group/BallSphere.lean

@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov, Heather Macbeth
+
+! This file was ported from Lean 3 source module analysis.normed.group.ball_sphere
+! leanprover-community/mathlib commit 3339976e2bcae9f1c81e620836d1eb736e3c4700
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Analysis.Normed.Group.Basic
+
+/-!
+# Negation on spheres and balls
+
+In this file we define `InvolutiveNeg` and `ContinuousNeg` instances for spheres, open balls, and
+closed balls in a semi normed group.
+-/
+
+
+open Metric Set
+
+variable {E : Type _} [i : SeminormedAddCommGroup E] {r : ℝ}
+
+/-- We equip the sphere, in a seminormed group, with a formal operation of negation, namely the
+antipodal map. -/
+instance : InvolutiveNeg (sphere (0 : E) r) where
+  neg := Subtype.map Neg.neg fun w => by simp
+  neg_neg x := Subtype.ext <| neg_neg x.1
+
+@[simp]
+theorem coe_neg_sphere {r : ℝ} (v : sphere (0 : E) r) : ↑(-v) = (-v : E) :=
+  rfl
+#align coe_neg_sphere coe_neg_sphere
+
+-- porting note: todo: need to specify instance to avoid timeout
+instance : ContinuousNeg (sphere (0 : E) r) :=
+  @Inducing.continuousNeg (sphere (0 : E) r) E _ _ _ _ TopologicalAddGroup.toContinuousNeg
+    Subtype.val inducing_subtype_val fun _ => rfl
+
+/-- We equip the ball, in a seminormed group, with a formal operation of negation, namely the
+antipodal map. -/
+instance {r : ℝ} : InvolutiveNeg (ball (0 : E) r) where
+  neg := Subtype.map Neg.neg fun w => by simp
+  neg_neg x := Subtype.ext <| neg_neg x.1
+
+@[simp] theorem coe_neg_ball {r : ℝ} (v : ball (0 : E) r) : ↑(-v) = (-v : E) := rfl
+#align coe_neg_ball coe_neg_ball
+
+-- porting note: todo: need to specify instance to avoid timeout
+instance : ContinuousNeg (ball (0 : E) r) :=
+  @Inducing.continuousNeg (ball (0 : E) r) E _ _ _ _ TopologicalAddGroup.toContinuousNeg
+    Subtype.val inducing_subtype_val fun _ => rfl
+
+/-- We equip the closed ball, in a seminormed group, with a formal operation of negation, namely the
+antipodal map. -/
+instance {r : ℝ} : InvolutiveNeg (closedBall (0 : E) r) where
+  neg := Subtype.map Neg.neg fun w => by simp
+  neg_neg x := Subtype.ext <| neg_neg x.1
+
+@[simp] theorem coe_neg_closedBall {r : ℝ} (v : closedBall (0 : E) r) : ↑(-v) = (-v : E) := rfl
+#align coe_neg_closed_ball coe_neg_closedBall
+
+-- porting note: todo: need to specify instance to avoid timeout
+instance : ContinuousNeg (closedBall (0 : E) r) :=
+  @Inducing.continuousNeg (closedBall (0 : E) r) E _ _ _ _ TopologicalAddGroup.toContinuousNeg
+    Subtype.val inducing_subtype_val fun _ => rfl