isDenseEmbedding

Mathlib.Topology.Homeomorph.Lemmas

URI: https://scilib.ai/kg/mathlib#Homeomorph.isDenseEmbedding

English

A homeomorphism h is a dense embedding; its range is dense and the map is an embedding.

Русский

Гомеоморфизм является плотным вложением: его образ плотен и отображение вложение.

LaTeX

$$$IsDenseEmbedding\\, h$$$

Lean4

theorem isDenseEmbedding (h : X ≃ₜ Y) : IsDenseEmbedding h :=
  { h.isEmbedding with dense := h.surjective.denseRange }

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

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

Разделы

Аффилиация

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