range_exp — Mathlib

English

The range of the complex exponential is the set of all nonzero complex numbers.

Русский

Область значения комплексной экспоненты совпадает с множеством всех ненулевых комплексных чисел.

LaTeX

$$$\{\exp z : z \in \mathbb{C}\} = \mathbb{C} \setminus \{0\}.$$$

Lean4

@[simp]
theorem range_exp : Set.range exp = {0}ᶜ :=
  Set.ext fun x =>
    ⟨by
      rintro ⟨x, rfl⟩
      exact exp_ne_zero x, fun hx => ⟨log x, exp_log hx⟩⟩

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