tan_lt_tan_of_lt_of_lt_pi_div_two

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

← MathLib Explorer

English

If -(π/2) < x < y < π/2, then tan x < tan y.

Русский

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

LaTeX

$$$-(\\\\frac{\\\\pi}{2}) < x < y < (\\\\frac{\\\\pi}{2}) \\Rightarrow \\\\tan x < \\\\tan y$$$

Lean4

theorem tan_lt_tan_of_lt_of_lt_pi_div_two {x y : ℝ} (hx₁ : -(π / 2) < x) (hy₂ : y < π / 2) (hxy : x < y) :
    tan x < tan y :=
  strictMonoOn_tan ⟨hx₁, hxy.trans hy₂⟩ ⟨hx₁.trans hxy, hy₂⟩ hxy

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

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

Разделы

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

Аффилиация

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