continuous

Mathlib.Topology.IsLocalHomeomorph

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

← MathLib Explorer

English

A local homeomorphism is continuous.

Русский

Локальная гомеоморфия непрерывна.

LaTeX

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

Lean4

/-- A local homeomorphism is continuous. -/
protected theorem continuous (hf : IsLocalHomeomorph f) : Continuous f :=
  continuousOn_univ.mp hf.isLocalHomeomorphOn.continuousOn

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

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

Разделы

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

Аффилиация

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