strictMonoOn_sin

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

English

The sine function is strictly increasing on the interval [−π/2, π/2].

Русский

Функция синус строго возрастает на промежутке [−π/2, π/2].

LaTeX

$$$$\text{StrictMonoOn}(\sin, [-\tfrac{\pi}{2}, \tfrac{\pi}{2}])$$$$

Lean4

theorem strictMonoOn_sin : StrictMonoOn sin (Icc (-(π / 2)) (π / 2)) := fun _ hx _ hy hxy =>
  sin_lt_sin_of_lt_of_le_pi_div_two hx.1 hy.2 hxy

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

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

Разделы

Аффилиация

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