PUnit

📁 Source: Mathlib/Topology/Sheaves/PUnit.lean

Statistics

Metric	Count
Definitions	0
Theorems isSheaf_iff_isTerminal_of_indiscrete, isSheaf_of_isTerminal_of_indiscrete, isSheaf_on_punit_iff_isTerminal, isSheaf_on_punit_of_isTerminal	4
Total	4

TopCat.Presheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSheaf_iff_isTerminal_of_indiscrete 📖	mathematical	TopCat.str Top.top TopologicalSpace TopCat.carrier OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	IsSheaf CategoryTheory.Limits.IsTerminal CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op Bot.bot OrderBot.toBot Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Order.Frame.toHeytingAlgebra TopologicalSpace.Opens.instFrame HeytingAlgebra.toOrderBot	—	isSheaf_of_isTerminal_of_indiscrete
isSheaf_of_isTerminal_of_indiscrete 📖	mathematical	TopCat.str Top.top TopologicalSpace TopCat.carrier OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	IsSheaf	—	eq_or_ne existsUnique_iff_exists CategoryTheory.Limits.IsTerminal.hom_ext le_bot_iff CategoryTheory.Sieve.arrows_eq_top_iff CategoryTheory.Sieve.id_mem_iff_eq_top TopologicalSpace.Opens.eq_bot_or_top isEmpty_or_nonempty SetLike.ext'_iff Set.univ_eq_empty_iff CategoryTheory.Presieve.isSheafFor_top
isSheaf_on_punit_iff_isTerminal 📖	mathematical	—	IsSheaf TopCat.of instTopologicalSpacePUnit CategoryTheory.Limits.IsTerminal CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op Bot.bot OrderBot.toBot Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Order.Frame.toHeytingAlgebra TopologicalSpace.Opens.instFrame HeytingAlgebra.toOrderBot	—	isSheaf_on_punit_of_isTerminal
isSheaf_on_punit_of_isTerminal 📖	mathematical	—	IsSheaf TopCat.of instTopologicalSpacePUnit	—	isSheaf_of_isTerminal_of_indiscrete Unique.instSubsingleton

---

← Back to Index