isOpenMap_im

Mathlib.Analysis.Complex.ReImTopology

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

English

The imaginary part map is an open map: it sends open sets in ℂ to open sets in ℝ.

Русский

Мнимая часть — открытое отображение: открытые множества в ℂ отображаются в открытые множества ℝ.

LaTeX

$$IsOpenMap( Im ) on ℂ → ℝ.$$

Lean4

theorem isOpenMap_im : IsOpenMap im :=
  isHomeomorphicTrivialFiberBundle_im.isOpenMap_proj

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

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

Разделы

Аффилиация

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