range_exp_mul_I — Mathlib

English

The set {e^{i t} : t ∈ ℝ} is exactly the unit circle; i.e., {e^{i t}} = {z ∈ ℂ : |z| = 1}.

Русский

Множество {e^{i t} : t ∈ ℝ} точно образует единичную окружность; то есть {e^{i t}} = {z ∈ ℂ : |z| = 1}.

LaTeX

$$$\\{e^{i t} : t \\in \\mathbb{R}\\} = \\{z \\in \\mathbb{C} : |z| = 1\\}$$$

Lean4

@[simp]
theorem range_exp_mul_I : (Set.range fun x : ℝ => exp (x * I)) = Metric.sphere 0 1 :=
  by
  ext x
  simp only [mem_sphere_zero_iff_norm, norm_eq_one_iff, Set.mem_range]

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