sin_arctan_nonneg

Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

English

0 ≤ sin(arctan x) iff 0 ≤ x.

Русский

0 ≤ sin(arctan x) тогда и только если 0 ≤ x.

LaTeX

$$$0 \\le \\\\sin(\\\\arctan x) \\Leftrightarrow 0 \\le x.$$$

Lean4

@[simp]
theorem sin_arctan_nonneg : 0 ≤ sin (arctan x) ↔ 0 ≤ x := by simpa using sin_arctan_strictMono.le_iff_le (a := 0)

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

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

Разделы

Аффилиация

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