continuous_circleMap_inv — Mathlib

English

If w ∈ B(z,R), then θ ↦ (circleMap(z,R,θ) − w)^{-1} is continuous.

Русский

Если w ∈ B(z,R), то θ ↦ (circleMap(z,R,θ) − w)^{-1} непрерывна.

LaTeX

$$$\text{If } w \in B(z,R), \; \theta \mapsto (circleMap(z,R,\theta) - w)^{-1} \text{ is continuous}. $$$

Lean4

theorem continuous_circleMap_inv {R : ℝ} {z w : ℂ} (hw : w ∈ ball z R) : Continuous fun θ => (circleMap z R θ - w)⁻¹ :=
  by
  have : ∀ θ, circleMap z R θ - w ≠ 0 := by
    simp_rw [sub_ne_zero]
    exact fun θ => circleMap_ne_mem_ball hw θ
  exact Continuous.inv₀ (by fun_prop) this

Похожие утверждения