mathlib3 documentation

analysis.normed.group.ball_sphere

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
@[simp]
theorem coe_neg_sphere {E : Type u_1} [seminormed_add_comm_group E] {r : } (v : (metric.sphere 0 r)) :
@[protected, instance]

We equip the ball, in a seminormed group, with a formal operation of negation, namely the antipodal map.

Equations
@[simp]
theorem coe_neg_ball {E : Type u_1} [seminormed_add_comm_group E] {r : } (v : (metric.ball 0 r)) :
@[protected, instance]

We equip the closed ball, in a seminormed group, with a formal operation of negation, namely the antipodal map.

Equations
@[simp]
theorem coe_neg_closed_ball {E : Type u_1} [seminormed_add_comm_group E] {r : } (v : (metric.closed_ball 0 r)) :