Theorems · Theorem · category theory

TopCat.Presheaf.presheafEquivOfIso_unitIso_hom_app_app

∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H : X ≅ Y)
  (X_1 : CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C) (X_2 : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  ((TopCat.Presheaf.presheafEquivOfIso C H).unitIso.hom.app X_1).app X_2 = X_1.map (CategoryTheory.eqToHom ⋯)

Defined in

Mathlib.Topology.Sheaves.Presheaf

Cited by

1 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category