Theorem CategoryTheory.Sieve.W_shrinkFunctor_ι_of_mem

Modification history

2026-03-16 11:24
Mathlib/CategoryTheory/Sites/Localization.lean
refactor(CategoryTheory/Sites): remove universe parameter from `Functor.IsContinuous` (#36459) …
Added CategoryTheory.Sieve.W_shrinkFunctor_ι_of_memView on Github →