arcsin_nhdsGE — Mathlib

English

If f tends to x with f ≥ x (one-sided from above), then arcsin f tends to arcsin x from above.

Русский

Если f стремится к x сверху, то arcsin f стремится к arcsin x сверху.

LaTeX

$$$\operatorname{Tendsto} f l (nhdsWithin x (Ici x)) \Rightarrow\operatorname{Tendsto}( \arcsin \circ f) l (nhdsWithin (\arcsin x) (Iic (\arcsin x)))$$$

Lean4

theorem arcsin_nhdsGE (h : Tendsto f l (𝓝[≥] x)) : Tendsto (arcsin <| f ·) l (𝓝[≥] (arcsin x)) :=
  ((continuous_arcsin.tendsto _).inf <| MapsTo.tendsto fun _ ↦ arcsin_le_arcsin).comp h

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