le_tan

Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

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

← MathLib Explorer

English

For 0 ≤ x < π/2, x ≤ tan x.

Русский

Для 0 ≤ x < π/2 выполняется x ≤ tan x.

LaTeX

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

Lean4

theorem le_tan {x : ℝ} (h1 : 0 ≤ x) (h2 : x < π / 2) : x ≤ tan x :=
  by
  rcases eq_or_lt_of_le h1 with (rfl | h1')
  · rw [tan_zero]
  · exact le_of_lt (lt_tan h1' h2)

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

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

Разделы

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

Аффилиация

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