isOpenEmbedding_exp — Mathlib

English

The exponential map is an open embedding from the real line into the positive reals.

Русский

Экспоненциальная карта является открытым вложением от ℝ в положительные вещественные числа.

LaTeX

$$$\\text{IsOpenEmbedding}(\\exp) \\text{ on }\\mathbb{R} \\to (0,\\infty).$$$

Lean4

theorem isOpenEmbedding_exp : IsOpenEmbedding exp :=
  isOpen_Ioi.isOpenEmbedding_subtypeVal.comp expOrderIso.toHomeomorph.isOpenEmbedding

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