English
The exponential function provides a partial homeomorphism between ℝ and (0, ∞), with log as its inverse on the appropriate domains; the map is open and continuous on its domain.
Русский
Экспонента задаёт частичную гомоморфную биективность между ℝ и (0, ∞) с логарифмом в роли обратной функции на соответствующих областях; отображение открытое и непрерывное на своей области.
LaTeX
$$$$ \\exp: \\mathbb{R} \\dashrightarrow (0,\\infty) \\quad \\text{and} \\quad \\log: (0,\\infty) \\to \\mathbb{R} \\text{ with inverse relations on domains.} $$$$
Lean4
theorem tendsto_log_comp_add_sub_log (y : ℝ) : Tendsto (fun x : ℝ => log (x + y) - log x) atTop (𝓝 0) :=
by
have : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0)) :=
tendsto_const_nhds.add (tendsto_const_nhds.div_atTop tendsto_id)
rw [← comap_exp_nhds_exp, exp_zero, tendsto_comap_iff, ← add_zero (1 : ℝ)]
refine this.congr' ?_
filter_upwards [eventually_gt_atTop (0 : ℝ), eventually_gt_atTop (-y)] with x hx₀ hxy
rw [comp_apply, exp_sub, exp_log, exp_log, one_add_div] <;> linarith
