arsinh — Mathlib

English

If f tends to a along l, then arsinh ∘ f tends to arsinh(a) along l.

Русский

Если f стремится к a вдоль фильтра l, то arsinh(f) стремится к arsinh(a) вдоль l.

LaTeX

$$$\\forall \\alpha,\\ l,\\ f:\\alpha \\to \\mathbb{R},\\ a:\\mathbb{R},\\ (\\operatorname{Tendsto} f\\ l\\ (\\mathcal{N}(a)))\\Rightarrow \\operatorname{Tendsto}(\\lambda x. \\operatorname{arsinh}(f x))\\ l\\ (\\mathcal{N}(\\operatorname{arsinh}(a))).$$$

Lean4

theorem arsinh {α : Type*} {l : Filter α} {f : α → ℝ} {a : ℝ} (h : Tendsto f l (𝓝 a)) :
    Tendsto (fun x => arsinh (f x)) l (𝓝 (arsinh a)) :=
  (continuous_arsinh.tendsto _).comp h

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