continuousOn_prod_circle_transform_function

English

The map w ↦ (circleMap z R w.snd − w.fst)^{-1}^2 is continuous on the product closedBall z r × univ, for r<R.

Русский

Карта w ↦ (circleMap z R w.snd − w.fst)^{-1}^2 непрерывна на произведении замкнутого шара и всем единичным множеством, если r<R.

LaTeX

$$$$ \\text{continuousOn} \\left( w \\mapsto (\\text{circleMap } z R w.snd - w.fst)^{-2} \\right) (\\text{closedBall } z r \\times \\text{univ}). $$$$

Lean4

theorem continuousOn_prod_circle_transform_function {R r : ℝ} (hr : r < R) {z : ℂ} :
    ContinuousOn (fun w : ℂ × ℝ => (circleMap z R w.snd - w.fst)⁻¹ ^ 2) (closedBall z r ×ˢ univ) :=
  by
  simp_rw [← one_div]
  apply_rules [ContinuousOn.pow, ContinuousOn.div, continuousOn_const]
  · exact ((continuous_circleMap z R).comp_continuousOn continuousOn_snd).sub continuousOn_fst
  · rintro ⟨a, b⟩ ⟨ha, -⟩
    have ha2 : a ∈ ball z R := closedBall_subset_ball hr ha
    exact sub_ne_zero.2 (circleMap_ne_mem_ball ha2 b)

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