Commit 2025-08-13 19:34 f9a48618

View on Github →

feat(Topology): induction for sheafification (#26258)

Estimated changes

Modified Mathlib/Topology/Sheaves/LocalPredicate.lean

modified theorem TopCat.PrelocalPredicate.sheafifyOf

added theorem TopCat.PrelocalPredicate.sheafify_inductionOn'

added theorem TopCat.PrelocalPredicate.sheafify_inductionOn

added theorem TopCat.PrelocalPredicate.sheafify_inductionOn₂'

added theorem TopCat.PrelocalPredicate.sheafify_inductionOn₂