cos_surjective — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem cos_surjective : Function.Surjective cos := by
  intro x
  obtain ⟨w, w₀, hw⟩ : ∃ w ≠ 0, 1 * (w * w) + -2 * x * w + 1 = 0 :=
    by
    rcases exists_quadratic_eq_zero one_ne_zero ⟨_, (cpow_nat_inv_pow _ two_ne_zero).symm.trans <| pow_two _⟩ with
      ⟨w, hw⟩
    refine ⟨w, ?_, hw⟩
    rintro rfl
    simp only [zero_add, one_ne_zero, mul_zero] at hw
  refine ⟨log w / I, cos_eq_iff_quadratic.2 ?_⟩
  rw [div_mul_cancel₀ _ I_ne_zero, exp_log w₀]
  convert hw using 1
  ring

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