Theorem TopCat.PrelocalPredicate.sheafifyOf

Modification history

2025-08-13 19:34
Mathlib/Topology/Sheaves/LocalPredicate.lean
feat(Topology): induction for sheafification (#26258)
Modified TopCat.PrelocalPredicate.sheafifyOfView on Github →
2025-04-22 10:51
Mathlib/Topology/Sheaves/LocalPredicate.lean
chore: generalize universes for (pre)sheaves of types (#22824)
Modified TopCat.PrelocalPredicate.sheafifyOfView on Github →
2023-05-31 06:39
Mathlib/Topology/Sheaves/LocalPredicate.lean
feat: port Topology.Sheaves.LocalPredicate (#4497)
Added TopCat.PrelocalPredicate.sheafifyOfView on Github →