restrictTopIso — Mathlib

English

Restricting a sheafed space to the top open embedding yields an isomorphism with the original space.

Русский

Ограничение расслоенного пространства до верхнего открытого подпространства образует изоморфизм с исходным пространством.

LaTeX

$$$X\text{ restrict to top } \cong X$$$

Lean4

/-- The restriction of a sheafed space `X` to the top subspace is isomorphic to `X` itself.
-/
@[simps! hom inv]
def restrictTopIso (X : SheafedSpace C) : X.restrict (Opens.isOpenEmbedding ⊤) ≅ X :=
  isoMk (X.toPresheafedSpace.restrictTopIso)

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