arg_neg_iff

Mathlib.Analysis.SpecialFunctions.Complex.Arg

URI: https://scilib.ai/kg/mathlib#Complex.arg_neg_iff

English

0 > arg z iff Im(z) < 0 (equivalently arg z < 0 iff Im z < 0).

Русский

arg z < 0 тогда и только тогда, когда Im(z) < 0.

LaTeX

$$$arg z < 0 \iff Im(z) < 0$$$

Lean4

@[simp]
theorem arg_neg_iff {z : ℂ} : arg z < 0 ↔ z.im < 0 :=
  lt_iff_lt_of_le_iff_le arg_nonneg_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru