strictMonoOn_tan — Mathlib

English

Tan is strictly monotone on (-π/2, π/2).

Русский

Тангенс строго монотонен на (-π/2, π/2).

LaTeX

$$$\\forall x,y\\in\\left(-\\\\frac{\\\\pi}{2},\\\\frac{\\\\pi}{2}\\right),\\ x

Lean4

theorem strictMonoOn_tan : StrictMonoOn tan (Ioo (-(π / 2)) (π / 2)) :=
  by
  rintro x hx y hy hlt
  rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos, div_lt_div_iff₀ (cos_pos_of_mem_Ioo hx) (cos_pos_of_mem_Ioo hy), mul_comm,
    ← sub_pos, ← sin_sub]
  exact sin_pos_of_pos_of_lt_pi (sub_pos.2 hlt) <| by linarith [hx.1, hy.2]

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