English
For any z ∈ ℂ, arg z ≤ π/2 if and only if either Re z ≥ 0 or Im z < 0.
Русский
Для любого z ∈ ℂ выполняется arg z ≤ π/2 тогда и только тогда, когда Re z ≥ 0 или Im z < 0.
LaTeX
$$$\\\\arg z \\\\le \\\\frac{\\\\pi}{2} \\\\iff \\\\Re z \\\\ge 0 \\\\lor \\\\Im z < 0$$$
Lean4
theorem arg_le_pi_div_two_iff {z : ℂ} : arg z ≤ π / 2 ↔ 0 ≤ re z ∨ im z < 0 :=
by
rcases le_or_gt 0 (re z) with hre | hre
· simp only [hre, arg_of_re_nonneg hre, Real.arcsin_le_pi_div_two, true_or]
simp only [hre.not_ge, false_or]
rcases le_or_gt 0 (im z) with him | him
· simp only [him.not_gt]
rw [iff_false, not_le, arg_of_re_neg_of_im_nonneg hre him, ← sub_lt_iff_lt_add, half_sub,
Real.neg_pi_div_two_lt_arcsin, neg_im, neg_div, neg_lt_neg_iff, div_lt_one, ← abs_of_nonneg him, abs_im_lt_norm]
exacts [hre.ne, norm_pos_iff.mpr <| ne_of_apply_ne re hre.ne]
· simp only [him]
rw [iff_true, arg_of_re_neg_of_im_neg hre him]
exact (sub_le_self _ Real.pi_pos.le).trans (Real.arcsin_le_pi_div_two _)
