arg_lt_pi_div_two_iff — Mathlib

English

For any z ∈ ℂ, arg z < π/2 iff either Re z > 0 or Im z < 0 or z = 0.

Русский

Для любого z ∈ ℂ, arg z < π/2 тогда, когда либо Re z > 0, либо Im z < 0, либо z = 0.

LaTeX

$$$\\\\arg z < \\\\frac{\\\\pi}{2} \\\\iff 0 < \\\\Re z \\\\lor \\\\Im z < 0 \\\\lor z = 0$$$

Lean4

theorem arg_lt_pi_div_two_iff {z : ℂ} : arg z < π / 2 ↔ 0 < re z ∨ im z < 0 ∨ z = 0 :=
  by
  rw [lt_iff_le_and_ne, arg_le_pi_div_two_iff, Ne, arg_eq_pi_div_two_iff]
  rcases lt_trichotomy z.re 0 with hre | hre | hre
  · have : z ≠ 0 := by simp [Complex.ext_iff, hre.ne]
    simp [hre.ne, hre.not_ge, hre.not_gt, this]
  · have : z = 0 ↔ z.im = 0 := by simp [Complex.ext_iff, hre]
    simp [hre, this, or_comm, le_iff_eq_or_lt]
  · simp [hre, hre.le, hre.ne']

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