circleMap_mem_closedBall — Mathlib

English

For any c ∈ ℂ and R ≥ 0, the image circleMap c R θ lies in the closed ball around c with radius R.

Русский

Для любого c ∈ ℂ и R ≥ 0 образ circleMap c R θ лежит в замкнутом шаре вокруг c радиуса R.

LaTeX

$$$ circleMap c R θ \in closedBall c R $$$

Lean4

theorem circleMap_mem_closedBall (c : ℂ) {R : ℝ} (hR : 0 ≤ R) (θ : ℝ) : circleMap c R θ ∈ closedBall c R :=
  sphere_subset_closedBall (circleMap_mem_sphere c hR θ)

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