sin_nonpos_of_nonpos_of_neg_pi_le

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

← MathLib Explorer

English

For all x ≤ 0 and -π ≤ x, sin x ≤ 0.

Русский

Для всех x ≤ 0 и -π ≤ x синус x ≤ 0.

LaTeX

$$$\forall x \le 0 \ , -\pi \le x ,\ \sin x \le 0$$$

Lean4

theorem sin_nonpos_of_nonpos_of_neg_pi_le {x : ℝ} (hx0 : x ≤ 0) (hpx : -π ≤ x) : sin x ≤ 0 :=
  neg_nonneg.1 <| sin_neg x ▸ sin_nonneg_of_nonneg_of_le_pi (neg_nonneg.2 hx0) (neg_le.1 hpx)

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

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

Разделы

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

Аффилиация

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