Theorem: mem_open_closed (Ray/Hartogs/Osgood.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
z c : ℂ
r : ℝ
⊢ z ∈ ball c r → z ∈ closedBall c r
Tactic:
simp only [Metric.mem_ball, Metric.mem_closedBall]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
z c : ℂ
r : ℝ
⊢ dist z c < r → dist z c ≤ r

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
z c : ℂ
r : ℝ
⊢ dist z c < r → dist z c ≤ r
Tactic:
exact le_of_lt
State after:
no goals