arg_one_add_mem_Ioo — Mathlib

English

Let z be a complex number with |z| < 1. Then the argument of 1 + z lies strictly between -π/2 and π/2.

Русский

Пусть z — комплексное число, удовлетворяющее |z| < 1. Тогда аргумент числа 1 + z лежит строго в интервале (-π/2, π/2).

LaTeX

$$$$\\forall z \\in \\mathbb{C}, \\ \\|z\\| < 1 \\quad\\Rightarrow\\quad (1 + z).arg \\in \\left(-\\frac{\\pi}{2}, \\frac{\\pi}{2}\\right).$$$$

Lean4

/-- The argument of `1 + z` for `z` in the open unit disc is always in `(-π / 2, π / 2)`. -/
theorem arg_one_add_mem_Ioo {z : ℂ} (hz : ‖z‖ < 1) : (1 + z).arg ∈ Set.Ioo (-(π / 2)) (π / 2) :=
  by
  rw [Set.mem_Ioo, ← abs_lt, abs_arg_lt_pi_div_two_iff, add_re, one_re, ← neg_lt_iff_pos_add']
  exact Or.inl (abs_lt.mp ((abs_re_le_norm z).trans_lt hz)).1

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