generalizingMap

Mathlib.Topology.Inseparable

URI: https://scilib.ai/kg/mathlib#IsOpenEmbedding.generalizingMap

English

If f is an open embedding, then f is a generalizing map.

Русский

Если f является открытым вложением, то оно является обобщающим отображением.

LaTeX

$$$\\\\text{IsOpenEmbedding}(f) \\\\Rightarrow \\\\text{GeneralizingMap}(f).$$$

Lean4

theorem generalizingMap (hf : IsOpenEmbedding f) : GeneralizingMap f :=
  hf.isInducing.generalizingMap hf.isOpen_range.stableUnderGeneralization

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

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

Разделы

Аффилиация

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