arctan_nonneg

Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

English

0 ≤ arctan x if and only if 0 ≤ x.

Русский

0 ≤ arctan x ⇔ 0 ≤ x.

LaTeX

$$$0 \\le \\arctan x \\Leftrightarrow 0 \\le x$$$

Lean4

@[simp]
theorem arctan_nonneg : 0 ≤ arctan x ↔ 0 ≤ x := by simpa only [arctan_zero] using arctan_le_arctan_iff (x := 0)

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

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

Разделы

Аффилиация

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