Def CategoryTheory.Functor.restrictedTopology

Modification history

2026-06-05 16:26

Mathlib/CategoryTheory/Sites/InducedTopology.lean

refactor(CategoryTheory/Sites): replace `Functor.inducedTopology` (#39951) …

Added CategoryTheory.Functor.restrictedTopology View on Github →