abs_arg_le_pi

Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

English

The absolute value of the argument is bounded by π: |arg z| ≤ π.

Русский

Модуль аргумента ограничен: |arg z| ≤ π.

LaTeX

$$$|\\\\arg z| \\\\le \\\\pi$$$

Lean4

theorem abs_arg_le_pi (z : ℂ) : |arg z| ≤ π :=
  abs_le.2 ⟨(neg_pi_lt_arg z).le, arg_le_pi z⟩

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

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

Разделы

Аффилиация

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