ofRestrict

Mathlib.Geometry.RingedSpace.OpenImmersion

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict

← MathLib Explorer

English

Restriction of an open immersion along hf yields an open immersion.

Русский

Ограничение открытого вложения вдоль hf даёт открытое вложение.

LaTeX

$$$\text{IsOpenImmersion}(Y_{|hf})$$$

Lean4

instance ofRestrict {X : TopCat} (Y : SheafedSpace C) {f : X ⟶ Y.carrier} (hf : IsOpenEmbedding f) :
    IsOpenImmersion (Y.ofRestrict hf) :=
  PresheafedSpace.IsOpenImmersion.ofRestrict _ hf

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

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

Разделы

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

Аффилиация

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