Negation on spheres and balls #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define has_involutive_neg instances for spheres, open balls, and closed balls in a
semi normed group.
@[protected, instance]
We equip the sphere, in a seminormed group, with a formal operation of negation, namely the antipodal map.
Equations
- metric.sphere.has_involutive_neg = {neg := subtype.map has_neg.neg metric.sphere.has_involutive_neg._proof_1, neg_neg := _}
@[simp]
theorem
coe_neg_sphere
{E : Type u_1}
[seminormed_add_comm_group E]
{r : ℝ}
(v : ↥(metric.sphere 0 r)) :
@[protected, instance]
@[protected, instance]
We equip the ball, in a seminormed group, with a formal operation of negation, namely the antipodal map.
Equations
- metric.ball.has_involutive_neg = {neg := subtype.map has_neg.neg metric.ball.has_involutive_neg._proof_1, neg_neg := _}
@[simp]
theorem
coe_neg_ball
{E : Type u_1}
[seminormed_add_comm_group E]
{r : ℝ}
(v : ↥(metric.ball 0 r)) :
@[protected, instance]
@[protected, instance]
We equip the closed ball, in a seminormed group, with a formal operation of negation, namely the antipodal map.
Equations
- metric.closed_ball.has_involutive_neg = {neg := subtype.map has_neg.neg metric.closed_ball.has_involutive_neg._proof_1, neg_neg := _}
@[simp]
theorem
coe_neg_closed_ball
{E : Type u_1}
[seminormed_add_comm_group E]
{r : ℝ}
(v : ↥(metric.closed_ball 0 r)) :
@[protected, instance]