isOpenMap_re

Mathlib.Analysis.Complex.ReImTopology

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

English

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

Русский

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

LaTeX

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

Lean4

theorem isOpenMap_re : IsOpenMap re :=
  isHomeomorphicTrivialFiberBundle_re.isOpenMap_proj

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

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

Разделы

Аффилиация

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