isLocalHomeomorph_circleExp — Mathlib

English

The exponential map from the real line to the unit circle is a local homeomorphism.

Русский

Экспоненциальное отображение из вещественной линии в единичную окружность является локальным гомеоморфизмом.

LaTeX

$$$ Circle.exp \\;:\\; \\mathbb{R} \\to Circle \\text{ is a local homeomorph of }\\mathbb{R}$.$$

Lean4

theorem isLocalHomeomorph_circleExp : IsLocalHomeomorph Circle.exp :=
  by
  have : Fact (0 < 2 * π) := ⟨by positivity⟩
  exact homeomorphCircle'.isLocalHomeomorph.comp (isLocalHomeomorph_coe (2 * π))

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