ofRestrict_invApp — Mathlib

English

Restriction of invApp to a restricted open image is the identity map.

Русский

Ограничение invApp до ограниченного открытого изображения является тождественным отображением.

LaTeX

$$$ (Y.ofRestrict hf).invApp _ U = \mathrm{Id} _ $$$

Lean4

@[elementwise, simp]
theorem ofRestrict_invApp (X : LocallyRingedSpace) {Y : TopCat} {f : Y ⟶ TopCat.of X.carrier} (h : IsOpenEmbedding f)
    (U : Opens (X.restrict h).carrier) : (LocallyRingedSpace.IsOpenImmersion.ofRestrict X h).invApp _ U = 𝟙 _ :=
  PresheafedSpace.IsOpenImmersion.ofRestrict_invApp _ h U

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