range_arg

Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

← MathLib Explorer

English

The set of all arguments equals the interval (-π, π].

Русский

Множество всех значений аргумента равняется интервалу (-π, π].

LaTeX

$$$$\\{\\\\arg z : z \\\\in \\\\mathbb{C}\\\\} = (-\\\\pi, \\\\pi]$$$$

Lean4

@[simp]
theorem range_arg : Set.range arg = Set.Ioc (-π) π :=
  (Set.range_subset_iff.2 arg_mem_Ioc).antisymm fun _ hx => ⟨_, arg_cos_add_sin_mul_I hx⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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