isOpenEmbedding

Mathlib.AlgebraicGeometry.OpenImmersion

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.Hom.isOpenEmbedding

English

If f is an open immersion, then the base map f.base is an open embedding.

Русский

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

LaTeX

$$$\\text{If } f\\text{ is open immersion, then } f.{\\text{base}}\\text{ is an open embedding.}$$$

Lean4

theorem isOpenEmbedding : IsOpenEmbedding f.base :=
  H.base_open

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

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

Разделы

Аффилиация

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