circleMap — Mathlib

English

The exponential map parameterizes a circle: θ ↦ c + R e^{i θ} gives the circle of center c and radius |R| in the complex plane.

Русский

Пусть c ∈ ℂ и R ∈ ℝ. Отображение θ ↦ c + R e^{i θ} задаёт окружность с центром в c и радиусом |R| на комплексной плоскости.

LaTeX

$$$ circleMap c R θ = c + R e^{i \theta} $$$

Lean4

/-- The exponential map $θ ↦ c + R e^{θi}$. The range of this map is the circle in `ℂ` with center
`c` and radius `|R|`. -/
def circleMap (c : ℂ) (R : ℝ) : ℝ → ℂ := fun θ => c + R * exp (θ * I)

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