tan_nonpos_of_nonpos_of_neg_pi_div_two_le

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

← MathLib Explorer

English

If x ≤ 0 and -(π/2) ≤ x, then tan x ≤ 0.

Русский

Если x ≤ 0 и -(π/2) ≤ x, то tan x ≤ 0.

LaTeX

$$$x \\le 0 \\land -\\\\frac{\\\\pi}{2} \\le x \\Rightarrow \\\\tan x \\le 0$$$

Lean4

theorem tan_nonpos_of_nonpos_of_neg_pi_div_two_le {x : ℝ} (hx0 : x ≤ 0) (hpx : -(π / 2) ≤ x) : tan x ≤ 0 :=
  neg_nonneg.1 (tan_neg x ▸ tan_nonneg_of_nonneg_of_le_pi_div_two (by linarith) (by linarith))

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

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

Разделы

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

Аффилиация

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