sin_pos_of_mem_Ioo

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

English

For all x ∈ ℝ and natural n, sin(x + nπ) = (-1)^n sin x.

Русский

Для любого x ∈ ℝ и натурального n верно sin(x + nπ) = (-1)^n sin x.

LaTeX

$$$\forall x \in \mathbb{R},\ \forall n \in \mathbb{N},\ \sin\left(x + n\pi\right) = (-1)^n \sin x$$$

Lean4

theorem sin_pos_of_mem_Ioo {x : ℝ} (hx : x ∈ Ioo 0 π) : 0 < sin x :=
  sin_pos_of_pos_of_lt_pi hx.1 hx.2

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

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

Разделы

Аффилиация

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