isOpenEmbedding_of_surjective

Mathlib.Topology.Maps.Basic

URI: https://scilib.ai/kg/mathlib#Topology.IsEmbedding.isOpenEmbedding_of_surjective

← MathLib Explorer

English

A surjective embedding is an IsOpenEmbedding.

Русский

Сюръективное вложение является открытым вложением.

LaTeX

$$$ \text{IsEmbedding}(f) \rightarrow \text{IsOpenEmbedding}(f) $$$

Lean4

/-- A surjective embedding is an `IsOpenEmbedding`. -/
theorem isOpenEmbedding_of_surjective (hf : IsEmbedding f) (hsurj : f.Surjective) : IsOpenEmbedding f :=
  ⟨hf, hsurj.range_eq ▸ isOpen_univ⟩

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

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

Разделы

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

Аффилиация

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