isLocalHomeomorph

Mathlib.Topology.IsLocalHomeomorph

URI: https://scilib.ai/kg/mathlib#IsLocalHomeomorph.Homeomorph.isLocalHomeomorph

← MathLib Explorer

English

A homeomorphism is a local homeomorphism.

Русский

Гомеоморфизм — это локальная гомеоморфия.

LaTeX

$$$\operatorname{IsLocalHomeomorph}(h) \text{ for } h \text{ a } X \simeq_t Y$$$

Lean4

/-- A homeomorphism is a local homeomorphism. -/
theorem isLocalHomeomorph (h : X ≃ₜ Y) : IsLocalHomeomorph h := fun _ ↦ ⟨h.toOpenPartialHomeomorph, trivial, rfl⟩

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

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

Разделы

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

Аффилиация

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