surjOn_exp_neg_pi_pi — Mathlib

English

Let exp: R → Circle be the unit-circle-valued exponential map. Then every point on the unit circle is obtained as exp t for some t with −π < t ≤ π; i.e., the image of the interval (−π, π] is the whole unit circle.

Русский

Пусть exp: ℝ → Окружность является отображением экспоненты на единичную окружность. Тогда каждая точка на единичной окружности получается в виде exp t для некоторого t, удовлетворяющего −π < t ≤ π; то есть прообраз экспоненты на интервале (−π, π] покрывает всю окружность.

LaTeX

$$$$ \forall z \in S^1,\ \exists t \in (-\pi,\pi],\ \exp t = z. $$$$

Lean4

theorem surjOn_exp_neg_pi_pi : SurjOn exp (Ioc (-π) π) univ :=
  argPartialEquiv.symm.surjOn

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