instOfRestrict — Mathlib

English

There exists an instance showing that restricting LocallyRingedSpace along an open embedding preserves the open immersion property.

Русский

Существуют примеры, показывающие, что ограничение LocallyRingedSpace вдоль открытого вложения сохраняет свойство открытого вложения.

LaTeX

$$$\text{instance } ofRestrict\; (X)\; (hf) : \text{IsOpenImmersion}(X|_{hf})$$$

Lean4

instance (X : LocallyRingedSpace) {U : TopCat} (f : U ⟶ X.toTopCat) (hf : IsOpenEmbedding f) :
    LocallyRingedSpace.IsOpenImmersion (X.ofRestrict hf) :=
  PresheafedSpace.IsOpenImmersion.ofRestrict X.toPresheafedSpace hf

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