sin_surjective — Mathlib

English

Sin is surjective on the complex numbers: for every x ∈ ℂ there exists z ∈ ℂ with sin z = x.

Русский

Синус отображает всё множество комплексных чисел: для любого x ∈ ℂ найдётся z ∈ ℂ такое, что sin z = x.

LaTeX

$$$$ \forall x \in \mathbb{C},\quad \exists z \in \mathbb{C} \text{ such that } \sin z = x. $$$$

Lean4

theorem sin_surjective : Function.Surjective sin := by
  intro x
  rcases cos_surjective x with ⟨z, rfl⟩
  exact ⟨z + π / 2, sin_add_pi_div_two z⟩

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