inv_sqrt_one_add_tan_sq

Mathlib.Analysis.Complex.Trigonometric

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

← MathLib Explorer

English

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

Русский

Если cos x ≠ 0, то tan^2 x / (1 + tan^2 x) = sin^2 x.

LaTeX

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

Lean4

theorem inv_sqrt_one_add_tan_sq {x : ℝ} (hx : 0 < cos x) : (√(1 + tan x ^ 2))⁻¹ = cos x := by
  rw [← sqrt_sq hx.le, ← sqrt_inv, inv_one_add_tan_sq hx.ne']

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

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

Разделы

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

Аффилиация

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