neg_pi_lt_arg

Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

English

-π < arg x for any x ∈ ℂ.

Русский

-π < arg x для любого x ∈ ℂ.

LaTeX

$$$-\\\\pi < \\\\arg x$$$

Lean4

theorem neg_pi_lt_arg (x : ℂ) : -π < arg x :=
  (arg_mem_Ioc x).1

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

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

Разделы

Аффилиация

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