polarCoord_target

Mathlib.Analysis.SpecialFunctions.PolarCoord

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

English

The polarCoord.target is the set {(r, θ): r > 0, -π < θ < π}.

Русский

Цель полярной карты — множество { (r, θ) : r > 0, -π < θ < π }.

LaTeX

$$$$ \mathrm{Complex}.\mathrm{polarCoord}.target = \{ (r,\theta) \in \mathbb{R} \times \mathbb{R} : r > 0, -\pi < \theta < \pi \}. $$$$

Lean4

protected theorem polarCoord_target : Complex.polarCoord.target = Set.Ioi (0 : ℝ) ×ˢ Set.Ioo (-π) π :=
  rfl

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

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

Разделы

Аффилиация

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