sin_eq_sin_iff — Mathlib

English

sin x = sin y iff there exists k ∈ ℤ with y = 2kπ + x or y = (2k+1)π − x.

Русский

sin x = sin y эквивалентно существованию k ∈ ℤ с y = 2kπ + x или y = (2k+1)π − x.

LaTeX

$$$$ \sin x = \sin y \iff \exists k \in \mathbb{Z},\ y = 2k\pi + x \ \text{or}\ y = (2k+1)\pi - x. $$$$

Lean4

theorem sin_eq_sin_iff {x y : ℝ} : sin x = sin y ↔ ∃ k : ℤ, y = 2 * k * π + x ∨ y = (2 * k + 1) * π - x :=
  mod_cast @Complex.sin_eq_sin_iff x y

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