Theorem: mem_closed_ball_neg_iff_mem_neg_closed_ball (RMT4/to_mathlib.lean)

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝ : SeminormedAddCommGroup V
u v : V
⊢ u ∈ closedBall (-v) r ↔ -u ∈ closedBall v r
Tactic:
rw [← neg_closedBall r v]
State after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝ : SeminormedAddCommGroup V
u v : V
⊢ u ∈ -closedBall v r ↔ -u ∈ closedBall v r

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝ : SeminormedAddCommGroup V
u v : V
⊢ u ∈ -closedBall v r ↔ -u ∈ closedBall v r
Tactic:
rfl
State after:
no goals