map_exp_atBot — Mathlib

English

The image of the atBot filter under exp corresponds to the neighborhood of 0 from the right (Ioi 0).

Русский

Образ экспоненты от фильтра atBot соответствует окрестности 0 справа (Ioi 0).

LaTeX

$$$\\mathrm{map}(\\exp, \\mathrm{atBot}) = \\mathcal{N}_{(0,\\infty)}.$$$

Lean4

@[simp]
theorem map_exp_atBot : map exp atBot = 𝓝[>] 0 := by
  rw [← coe_comp_expOrderIso, ← Filter.map_map, expOrderIso.map_atBot, ← map_coe_Ioi_atBot]

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