image_circleMap_Ioc — Mathlib

English

The image of Ioc under circleMap is the sphere with center c and radius |R|.

Русский

Образ Ioc через circleMap — сфера с центром c и радиусом |R|.

LaTeX

$$$circleMap\ c\ R '' Ioc\ 0\ (2\pi) = sphere\ c\ |R|$$$

Lean4

/-- The image of `(0, 2π]` under `circleMap c R` is the circle with center `c` and radius `|R|`. -/
@[simp]
theorem image_circleMap_Ioc (c : ℂ) (R : ℝ) : circleMap c R '' Ioc 0 (2 * π) = sphere c |R| := by
  rw [← range_circleMap, ← (periodic_circleMap c R).image_Ioc Real.two_pi_pos 0, zero_add]

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