arccos_nhdsLE — Mathlib

English

If f → x from below (nhdsWithin x Iic x), then arccos f → arccos x from above (nhdsWithin arccos x Ici (arccos x)).

Русский

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

LaTeX

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

Lean4

theorem arccos_nhdsLE (h : Tendsto f l (𝓝[≤] x)) : Tendsto (arccos <| f ·) l (𝓝[≥] (arccos x)) :=
  ((continuous_arccos.tendsto _).inf <| MapsTo.tendsto fun _ ↦ arccos_le_arccos).comp h

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