arg_nonneg_iff — Mathlib

English

0 ≤ arg z iff 0 ≤ Im(z) (with the convention for z = 0).

Русский

0 ≤ arg z тогда и только тогда, когда 0 ≤ Im(z) (с оговоркой для z = 0).

LaTeX

$$$0 \\le \\\\arg z \\\\Longleftrightarrow 0 \\le \\\\Im(z)$$$

Lean4

@[simp]
theorem arg_nonneg_iff {z : ℂ} : 0 ≤ arg z ↔ 0 ≤ z.im :=
  by
  rcases eq_or_ne z 0 with (rfl | h₀); · simp
  calc
    0 ≤ arg z ↔ 0 ≤ Real.sin (arg z) :=
      ⟨fun h => Real.sin_nonneg_of_mem_Icc ⟨h, arg_le_pi z⟩,
        by
        contrapose!
        intro h
        exact Real.sin_neg_of_neg_of_neg_pi_lt h (neg_pi_lt_arg _)⟩
    _ ↔ _ := by rw [sin_arg, le_div_iff₀ (norm_pos_iff.mpr h₀), zero_mul]

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