isOpenMap

Mathlib.Topology.IsLocalHomeomorph

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

← MathLib Explorer

English

A local homeomorphism is an open map.

Русский

Локальная гомеоморфия является открытым отображением.

LaTeX

$$$\operatorname{IsLocalHomeomorph}(f) \Rightarrow \operatorname{IsOpenMap}(f)$$$

Lean4

/-- A local homeomorphism is an open map. -/
protected theorem isOpenMap (hf : IsLocalHomeomorph f) : IsOpenMap f :=
  IsOpenMap.of_nhds_le fun x ↦ ge_of_eq (hf.map_nhds_eq x)

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

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

Разделы

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

Аффилиация

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