image_exp_Ioc_eq_sphere — Mathlib

English

The image of the map θ ↦ exp(i θ) on θ ∈ (-π, π] is exactly the unit circle. Equivalently, the set {exp(i θ) : θ ∈ (-π, π]} equals {z ∈ ℂ : |z| = 1}.

Русский

Образ отображения θ ↦ e^{iθ} при θ ∈ (-π, π] совпадает с единичной окружностью; то есть {e^{iθ} : θ ∈ (-π, π]} = {z ∈ ℂ : |z| = 1}.

LaTeX

$$$\\\\{ e^{i\\\\theta} : \\\\theta \\\\in (-\\\\pi, \\\\pi] \\\\} = \\\\{ z \\\\in \\\\mathbb{C} : |z| = 1 \}$$$

Lean4

theorem image_exp_Ioc_eq_sphere : (fun θ : ℝ ↦ exp (θ * I)) '' Set.Ioc (-π) π = sphere 0 1 := by ext;
  simpa using norm_eq_one_iff'.symm

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