sin_neg_of_neg_of_neg_pi_lt

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

← MathLib Explorer

English

For all x with -π < x < 0, sin x < 0.

Русский

Для любого x с -π < x < 0 синус x меньше нуля.

LaTeX

$$$\forall x \in (-\pi,0),\ \sin x < 0$$$

Lean4

theorem sin_neg_of_neg_of_neg_pi_lt {x : ℝ} (hx0 : x < 0) (hpx : -π < x) : sin x < 0 :=
  neg_pos.1 <| sin_neg x ▸ sin_pos_of_pos_of_lt_pi (neg_pos.2 hx0) (neg_lt.1 hpx)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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