comap_exp_nhdsGT_zero — Mathlib

English

The preimage under exp of neighborhoods shrinking to 0 from the right lies arbitrarily far to the left (towards −∞).

Русский

Предобраз экспоненты от окрестностей, сходящихся к 0 справа, лежит произвольно далеко слева (к −∞).

LaTeX

$$$\\exp^{-1}((0,\\varepsilon)) = (-\\infty, \\ln\\varepsilon) \\quad (\\varepsilon>0).$$$

Lean4

@[simp]
theorem comap_exp_nhdsGT_zero : comap exp (𝓝[>] 0) = atBot := by rw [← map_exp_atBot, comap_map exp_injective]

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