ofRestrict — Mathlib

English

For any open immersion f, the stalk maps f.stalkMap x are isomorphisms for all x in X; i.e., f.stalkMap x ∈ IsIso.

Русский

Для любого открытого вложения f отображения stalkMap x являются изоморфизмами для каждого x в X.

LaTeX

$$$$ \forall x, \; IsIso(f.stalkMap x) $$$$

Lean4

instance ofRestrict : IsOpenImmersion (X.ofRestrict h) :=
  show PresheafedSpace.IsOpenImmersion (X.toPresheafedSpace.ofRestrict h) by infer_instance

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