Commit 2023-05-22 16:35 de4c745f

View on Github →

feat: port Topology.Sheaves.PUnit (#4173)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Sheaves/PUnit.lean

added theorem TopCat.Presheaf.isSheaf_iff_isTerminal_of_indiscrete

added theorem TopCat.Presheaf.isSheaf_of_isTerminal_of_indiscrete

added theorem TopCat.Presheaf.isSheaf_on_pUnit_iff_isTerminal

added theorem TopCat.Presheaf.isSheaf_on_pUnit_of_isTerminal