isOpenMap

Mathlib.Topology.Covering

URI: https://scilib.ai/kg/mathlib#IsCoveringMap.isOpenMap

English

A covering map is an open map.

Русский

Покровное отображение является открытым отображением.

LaTeX

$$$\forall f:\ E\to X,\ IsCoveringMap(f) \Rightarrow \IsOpenMap(f)$$$

Lean4

protected theorem isOpenMap : IsOpenMap f :=
  hf.isLocalHomeomorph.isOpenMap

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

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

Разделы

Аффилиация

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