E : Type ?u.59862
inst✝ : NormedAddCommGroup E
R : ℝ
z w : ℂ
hw : w ∈ ball z R
this : ∀ (θ : ℝ), circleMap z R θ - w ≠ 0
⊢ Continuous fun θ => (circleMap z R θ - w)⁻¹
E : Type ?u.59862
inst✝ : NormedAddCommGroup E
R : ℝ
z w : ℂ
hw : w ∈ ball z R
⊢ Continuous fun θ => (circleMap z R θ - w)⁻¹
have : ∀ θ, circleMap z R θ - w ≠ 0 := by
  simp_rw [sub_ne_zero]
  exact fun θ => circleMap_ne_mem_ball hw θ
no goals
E : Type ?u.59862
inst✝ : NormedAddCommGroup E
R : ℝ
z w : ℂ
hw : w ∈ ball z R
this : ∀ (θ : ℝ), circleMap z R θ - w ≠ 0
⊢ Continuous fun θ => (circleMap z R θ - w)⁻¹
exact Continuous.inv₀ (by continuity) this
E : Type ?u.59862
inst✝ : NormedAddCommGroup E
R : ℝ
z w : ℂ
hw : w ∈ ball z R
⊢ ∀ (θ : ℝ), circleMap z R θ ≠ w
E : Type ?u.59862
inst✝ : NormedAddCommGroup E
R : ℝ
z w : ℂ
hw : w ∈ ball z R
⊢ ∀ (θ : ℝ), circleMap z R θ - w ≠ 0
simp_rw [sub_ne_zero]
no goals
E : Type ?u.59862
inst✝ : NormedAddCommGroup E
R : ℝ
z w : ℂ
hw : w ∈ ball z R
⊢ ∀ (θ : ℝ), circleMap z R θ ≠ w
exact fun θ => circleMap_ne_mem_ball hw θ
no goals
E : Type ?u.59862
inst✝ : NormedAddCommGroup E
R : ℝ
z w : ℂ
hw : w ∈ ball z R
this : ∀ (θ : ℝ), circleMap z R θ - w ≠ 0
⊢ Continuous fun θ => circleMap z R θ - w
continuity