Theorem CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_restrictedTopology

Modification history

2026-06-05 16:26
Mathlib/CategoryTheory/MorphismProperty/CommaSites.lean
refactor(CategoryTheory/Sites): replace `Functor.inducedTopology` (#39951) …
Added CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_restrictedTopologyView on Github →