arccos_nhdsGE — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem arccos_nhdsGE (h : Tendsto f l (𝓝[≥] x)) : Tendsto (arccos <| f ·) l (𝓝[≤] (arccos x)) :=
  by
  refine ((continuous_arccos.tendsto _).inf <| MapsTo.tendsto fun y hy ↦ ?_).comp h
  simp only [mem_Ici, mem_Iic] at hy ⊢
  exact antitone_arccos hy

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