continuous_polarCoord_symm

Mathlib.Analysis.SpecialFunctions.PolarCoord

URI: https://scilib.ai/kg/mathlib#continuous_polarCoord_symm

English

The inverse polar coordinate map on the complex plane is continuous.

Русский

Обратная полярная карта непрерывна.

LaTeX

$$$$ \text{Continuous}( \mathrm{polarCoord.symm} ). $$$$

Lean4

@[fun_prop]
theorem continuous_polarCoord_symm : Continuous polarCoord.symm :=
  .prodMk (by fun_prop) (by fun_prop)

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

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

Разделы

Аффилиация

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