invApp_app — Mathlib

English

A variant of invApp_app using eqToHom rather than homOfLE, expressing compatibility with a subset relation.

Русский

Вариант invApp_app, использующий eqToHom вместо homOfLE, выражающий совместимость с подмножеством.

LaTeX

$$@[reassoc] invApp f U ≫ f.c.app (op (opensFunctor f |>.obj U)) = Y.presheaf.map (eqToHom (le_antisymm (Set.image_preimage_subset f.base U.1) (...) )).op$$

Lean4

@[simp, reassoc, elementwise]
theorem invApp_app (U : Opens X) :
    invApp f U ≫ f.c.app (op (opensFunctor f |>.obj U)) =
      X.presheaf.map (eqToHom (by simp [Opens.map, Set.preimage_image_eq _ H.base_open.injective])) :=
  by rw [invApp, Category.assoc, IsIso.inv_hom_id, Category.comp_id]

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