range_circleMap — Mathlib

English

The image of circleMap over θ ∈ (0, 2π] is the circle with center c and radius |R|.

Русский

Образ circleMap по θ ∈ (0,2π] совпадает с окружностью с центром c и радиусом |R|.

LaTeX

$$$\operatorname{range}(circleMap\ c\ R) = \{ z: |z-c| = |R| \}$$$

Lean4

/-- The range of `circleMap c R` is the circle with center `c` and radius `|R|`. -/
@[simp]
theorem range_circleMap (c : ℂ) (R : ℝ) : range (circleMap c R) = sphere c |R| :=
  calc
    range (circleMap c R) = c +ᵥ R • range fun θ : ℝ => exp (θ * I) := by
      simp +unfoldPartialApp only [← image_vadd, ← image_smul, ← range_comp, vadd_eq_add, circleMap, comp_def,
        real_smul]
    _ = sphere c |R| := by
      rw [range_exp_mul_I, smul_sphere R 0 zero_le_one]
      simp

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