tendsto_sin_pi_div_two

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

URI: https://scilib.ai/kg/mathlib#Real.tendsto_sin_pi_div_two

English

As x approaches π/2 from below, sin x tends to 1.

Русский

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

LaTeX

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

Lean4

theorem tendsto_sin_pi_div_two : Tendsto sin (𝓝[<] (π / 2)) (𝓝 1) :=
  by
  convert continuous_sin.continuousWithinAt.tendsto
  simp

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

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

Разделы

Аффилиация

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