tan_neg_of_neg_of_pi_div_two_lt

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

← MathLib Explorer

English

If x < 0 and -π/2 < x, then tan x < 0.

Русский

Если x < 0 и -π/2 < x, то tan x < 0.

LaTeX

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

Lean4

theorem tan_neg_of_neg_of_pi_div_two_lt {x : ℝ} (hx0 : x < 0) (hpx : -(π / 2) < x) : tan x < 0 :=
  neg_pos.1 (tan_neg x ▸ tan_pos_of_pos_of_lt_pi_div_two (by linarith) (by linarith [pi_pos]))

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

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

Разделы

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

Аффилиация

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