tan_div_sqrt_one_add_tan_sq

Mathlib.Analysis.Complex.Trigonometric

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

← MathLib Explorer

English

If 0 < cos x, then tan x / sqrt(1 + tan^2 x) = sin x.

Русский

Если cos x > 0, тогда tan x / sqrt(1 + tan^2 x) = sin x.

LaTeX

$$\$0 < \\cos x \\Rightarrow \\dfrac{\\tan x}{\\sqrt{1 + \\tan^2 x}} = \\sin x\$$$

Lean4

theorem tan_div_sqrt_one_add_tan_sq {x : ℝ} (hx : 0 < cos x) : tan x / √(1 + tan x ^ 2) = sin x := by
  rw [← tan_mul_cos hx.ne', ← inv_sqrt_one_add_tan_sq hx, div_eq_mul_inv]

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

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

Разделы

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

Аффилиация

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