neg_pi_div_two_lt_arg_iff — Mathlib

English

For any z ∈ ℂ, -(π/2) < arg z iff either Re z > 0 or Im z ≥ 0.

Русский

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

LaTeX

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

Lean4

theorem neg_pi_div_two_lt_arg_iff {z : ℂ} : -(π / 2) < arg z ↔ 0 < re z ∨ 0 ≤ im z :=
  by
  rw [lt_iff_le_and_ne, neg_pi_div_two_le_arg_iff, ne_comm, Ne, arg_eq_neg_pi_div_two_iff]
  rcases lt_trichotomy z.re 0 with hre | hre | hre
  · simp [hre.ne, hre.not_ge, hre.not_gt]
  · simp [hre]
  · simp [hre, hre.le, hre.ne']

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