measurable_polarCoord_symm

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

URI: https://scilib.ai/kg/mathlib#NumberField.mixedEmbedding.measurable_polarCoord_symm

← MathLib Explorer

English

The inverse of the polar coordinate map is measurable.

Русский

Обратное к полярной координате отображение измеримо.

LaTeX

$$$\\mathrm{Measurable}((\\mathrm{polarCoord}(K)).\\mathrm{symm})$$$

Lean4

theorem measurable_polarCoord_symm : Measurable (mixedEmbedding.polarCoord K).symm :=
  by
  rw [polarCoord_symm_eq]
  exact (Homeomorph.measurable _).comp (measurable_polarCoordReal_symm K)

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

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

Разделы

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

Аффилиация

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