isLocalHomeomorph

Mathlib.Topology.Covering

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

← MathLib Explorer

English

Every covering map is a local homeomorphism.

Русский

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

LaTeX

$$$\forall f:\ E\to X,\ \IsCoveringMap(f) \Rightarrow \text{IsLocalHomeomorph}(f)$$$

Lean4

protected theorem isLocalHomeomorph : IsLocalHomeomorph f :=
  isLocalHomeomorph_iff_isLocalHomeomorphOn_univ.mpr hf.isCoveringMapOn.isLocalHomeomorphOn

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

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

Разделы

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

Аффилиация

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