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 CategoryTheory.Category.opposite Preorder.smallCategory TopologicalSpace.Opens.instPartialOrder Opposite.op Bot.bot OrderBot.toBot 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