arg_mem_Ioc — Mathlib

English

For any complex z, arg z ∈ (-π, π].

Русский

Для любого z ∈ ℂ, arg z ∈ (-π, π].

LaTeX

$$$\\\\arg z \\\\in (-\\\\pi, \\\\pi]$$$

Lean4

theorem arg_mem_Ioc (z : ℂ) : arg z ∈ Set.Ioc (-π) π :=
  by
  have hπ : 0 < π := Real.pi_pos
  rcases eq_or_ne z 0 with (rfl | hz)
  · simp [hπ, hπ.le]
  rcases existsUnique_add_zsmul_mem_Ioc Real.two_pi_pos (arg z) (-π) with ⟨N, hN, -⟩
  rw [two_mul, neg_add_cancel_left, ← two_mul, zsmul_eq_mul] at hN
  rw [← norm_mul_cos_add_sin_mul_I z, ← cos_add_int_mul_two_pi _ N, ← sin_add_int_mul_two_pi _ N]
  have := arg_mul_cos_add_sin_mul_I (norm_pos_iff.mpr hz) hN
  push_cast at this
  rwa [this]

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