arcsin

Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

URI: https://scilib.ai/kg/mathlib#Filter.Tendsto.arcsin

English

If f tends to x along l, then arcsin f tends to arcsin x.

Русский

Если f сходится к x вдоль фильтра l, то arcsin f сходится к arcsin x.

LaTeX

$$$\operatorname{Tendsto} f l (nhds x) \Rightarrow \operatorname{Tendsto} (\arcsin \circ f) l (nhds (\arcsin x))$$$

Lean4

protected theorem arcsin (h : Tendsto f l (𝓝 x)) : Tendsto (arcsin <| f ·) l (𝓝 (arcsin x)) :=
  (continuous_arcsin.tendsto _).comp h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru