isoRestrict_inv_ofRestrict — Mathlib

English

The inverse of the open-immersion restriction morphism composed with f equals the restricted target map, reflecting compatibility of the restriction isomorphism with the ambient map.

Русский

Обратный ограничитель изоморфизма совместимости ограничений удовлетворяет равенству с ограниченным отображением цели.

LaTeX

$$Eq ((IsOpenImmersion.isoRestrict f).inv ≫ f) (Y.ofRestrict _)$$

Lean4

@[reassoc (attr := simp)]
theorem isoRestrict_inv_ofRestrict : (isoRestrict f).inv ≫ f = Y.ofRestrict _ := by
  rw [Iso.inv_comp_eq, isoRestrict_hom_ofRestrict]

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