ofRestrict_stalkMap_isIso — Mathlib

English

For any open immersion f and any point x, the stalk map associated with restricting along f is an isomorphism.

Русский

Для любого открытого вложения f и любой точки x отображение stalk, связанное с ограничением вдоль f, является изоморфизмом.

LaTeX

$$IsIso((X.ofRestrict h).stalkMap x)$$

Lean4

instance ofRestrict_stalkMap_isIso : IsIso ((X.ofRestrict h).stalkMap x) :=
  PresheafedSpace.ofRestrict_stalkMap_isIso X.toPresheafedSpace h x

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