tendsto_cos_neg_pi_div_two — Mathlib

English

As x approaches −π/2 from the left, cos x tends to 0.

Русский

При приближении x к −π/2 слева, cos x стремится к 0.

LaTeX

$$$$\lim_{x \to (-\frac{\pi}{2})^-} \cos x = 0.$$$$

Lean4

theorem tendsto_cos_neg_pi_div_two : Tendsto cos (𝓝[>] (-(π / 2))) (𝓝[>] 0) :=
  by
  apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
  · convert continuous_cos.continuousWithinAt.tendsto
    simp
  · filter_upwards [Ioo_mem_nhdsGT (neg_lt_self pi_div_two_pos)] with x hx
    exact cos_pos_of_mem_Ioo hx

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