Documentation Verification Report

OpensLeCover

📁 Source: Mathlib/Topology/Sheaves/SheafCondition/OpensLeCover.lean

Statistics

Metric	Count
Definitions `IsSheafOpensLeCover`, `OpensLeCover`, `homToIndex`, `index`, `instCategoryOpensLeCover`, `instInhabitedOpensLeCoverOfNonempty`, `opensLeCoverCocone`, `generateEquivalenceOpensLe`, `generateEquivalenceOpensLe_functor'`, `generateEquivalenceOpensLe_inverse'`, `isLimitOpensLeEquivGenerate₁`, `isLimitOpensLeEquivGenerate₂`, `whiskerIsoMapGenerateCocone`	13
Theorems `isSheafOpensLeCover`, `generateEquivalenceOpensLe_counitIso`, `generateEquivalenceOpensLe_functor`, `generateEquivalenceOpensLe_functor'_map`, `generateEquivalenceOpensLe_functor'_obj_obj`, `generateEquivalenceOpensLe_inverse`, `generateEquivalenceOpensLe_inverse'_map`, `generateEquivalenceOpensLe_inverse'_obj_obj_hom`, `generateEquivalenceOpensLe_inverse'_obj_obj_left`, `generateEquivalenceOpensLe_inverse'_obj_obj_right_as`, `generateEquivalenceOpensLe_unitIso`, `isSheaf_iff_isSheafOpensLeCover`, `whiskerIsoMapGenerateCocone_hom_hom`, `whiskerIsoMapGenerateCocone_inv_hom`	14
Total	27

TopCat.Presheaf

Definitions

Name	Category	Theorems
`IsSheafOpensLeCover` 📖	MathDef	2 math math: `isSheafOpensLeCover_iff_isSheafPairwiseIntersections`, `isSheaf_iff_isSheafOpensLeCover`
`generateEquivalenceOpensLe` 📖	CompOp	6 math math: `generateEquivalenceOpensLe_unitIso`, `whiskerIsoMapGenerateCocone_inv_hom`, `generateEquivalenceOpensLe_functor`, `generateEquivalenceOpensLe_counitIso`, `whiskerIsoMapGenerateCocone_hom_hom`, `generateEquivalenceOpensLe_inverse`
`generateEquivalenceOpensLe_functor'` 📖	CompOp	5 math math: `generateEquivalenceOpensLe_functor'_obj_obj`, `generateEquivalenceOpensLe_unitIso`, `generateEquivalenceOpensLe_functor`, `generateEquivalenceOpensLe_counitIso`, `generateEquivalenceOpensLe_functor'_map`
`generateEquivalenceOpensLe_inverse'` 📖	CompOp	7 math math: `generateEquivalenceOpensLe_unitIso`, `generateEquivalenceOpensLe_inverse'_obj_obj_right_as`, `generateEquivalenceOpensLe_inverse'_obj_obj_hom`, `generateEquivalenceOpensLe_counitIso`, `generateEquivalenceOpensLe_inverse'_obj_obj_left`, `generateEquivalenceOpensLe_inverse'_map`, `generateEquivalenceOpensLe_inverse`
`isLimitOpensLeEquivGenerate₁` 📖	CompOp	—
`isLimitOpensLeEquivGenerate₂` 📖	CompOp	—
`whiskerIsoMapGenerateCocone` 📖	CompOp	2 math math: `whiskerIsoMapGenerateCocone_inv_hom`, `whiskerIsoMapGenerateCocone_hom_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`generateEquivalenceOpensLe_counitIso` 📖	mathematical	`iSup` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice`	`CategoryTheory.Equivalence.counitIso` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Over` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.instCategoryOver` `CategoryTheory.Sieve.arrows` `CategoryTheory.Sieve.generate` `presieveOfCoveringAux` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.hom` `SheafCondition.OpensLeCover` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SheafCondition.instCategoryOpensLeCover` `generateEquivalenceOpensLe` `CategoryTheory.eqToIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `generateEquivalenceOpensLe_inverse'` `generateEquivalenceOpensLe_functor'`	—	—
`generateEquivalenceOpensLe_functor` 📖	mathematical	`iSup` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice`	`CategoryTheory.Equivalence.functor` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Over` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.instCategoryOver` `CategoryTheory.Sieve.arrows` `CategoryTheory.Sieve.generate` `presieveOfCoveringAux` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.hom` `SheafCondition.OpensLeCover` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SheafCondition.instCategoryOpensLeCover` `generateEquivalenceOpensLe` `generateEquivalenceOpensLe_functor'`	—	—
`generateEquivalenceOpensLe_functor'_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Over` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.instCategoryOver` `CategoryTheory.Sieve.arrows` `CategoryTheory.Sieve.generate` `presieveOfCoveringAux` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.hom` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SheafCondition.OpensLeCover` `SheafCondition.instCategoryOpensLeCover` `generateEquivalenceOpensLe_functor'` `CategoryTheory.ObjectProperty.homMk` `Preorder.toLE` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.CommaMorphism.left` `CategoryTheory.InducedCategory.Hom.hom`	—	—
`generateEquivalenceOpensLe_functor'_obj_obj` 📖	mathematical	—	`CategoryTheory.ObjectProperty.FullSubcategory.obj` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Preorder.toLE` `CategoryTheory.Functor.obj` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Sieve.arrows` `CategoryTheory.Sieve.generate` `presieveOfCoveringAux` `CategoryTheory.Functor.id` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.hom` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SheafCondition.OpensLeCover` `SheafCondition.instCategoryOpensLeCover` `generateEquivalenceOpensLe_functor'`	—	—
`generateEquivalenceOpensLe_inverse` 📖	mathematical	`iSup` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice`	`CategoryTheory.Equivalence.inverse` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Over` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.instCategoryOver` `CategoryTheory.Sieve.arrows` `CategoryTheory.Sieve.generate` `presieveOfCoveringAux` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.hom` `SheafCondition.OpensLeCover` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SheafCondition.instCategoryOpensLeCover` `generateEquivalenceOpensLe` `generateEquivalenceOpensLe_inverse'`	—	—
`generateEquivalenceOpensLe_inverse'_map` 📖	mathematical	`iSup` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice`	`CategoryTheory.Functor.map` `SheafCondition.OpensLeCover` `SheafCondition.instCategoryOpensLeCover` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Over` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.instCategoryOver` `CategoryTheory.Sieve.arrows` `CategoryTheory.Sieve.generate` `presieveOfCoveringAux` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.hom` `CategoryTheory.ObjectProperty.FullSubcategory.category` `generateEquivalenceOpensLe_inverse'` `CategoryTheory.ObjectProperty.homMk` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `Preorder.toLE` `CategoryTheory.homOfLE` `CategoryTheory.Over.homMk` `CategoryTheory.InducedCategory.Hom.hom`	—	—
`generateEquivalenceOpensLe_inverse'_obj_obj_hom` 📖	mathematical	`iSup` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice`	`CategoryTheory.Comma.hom` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Sieve.arrows` `CategoryTheory.Sieve.generate` `presieveOfCoveringAux` `CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `SheafCondition.OpensLeCover` `SheafCondition.instCategoryOpensLeCover` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `generateEquivalenceOpensLe_inverse'` `CategoryTheory.homOfLE` `Preorder.toLE`	—	—
`generateEquivalenceOpensLe_inverse'_obj_obj_left` 📖	mathematical	`iSup` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice`	`CategoryTheory.Comma.left` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Sieve.arrows` `CategoryTheory.Sieve.generate` `presieveOfCoveringAux` `CategoryTheory.Functor.obj` `CategoryTheory.Comma.hom` `SheafCondition.OpensLeCover` `SheafCondition.instCategoryOpensLeCover` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `generateEquivalenceOpensLe_inverse'` `Preorder.toLE`	—	—
`generateEquivalenceOpensLe_inverse'_obj_obj_right_as` 📖	mathematical	`iSup` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice`	`CategoryTheory.Discrete.as` `CategoryTheory.Comma.right` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Sieve.arrows` `CategoryTheory.Sieve.generate` `presieveOfCoveringAux` `CategoryTheory.Functor.obj` `CategoryTheory.Comma.left` `CategoryTheory.Comma.hom` `SheafCondition.OpensLeCover` `SheafCondition.instCategoryOpensLeCover` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `generateEquivalenceOpensLe_inverse'`	—	—
`generateEquivalenceOpensLe_unitIso` 📖	mathematical	`iSup` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice`	`CategoryTheory.Equivalence.unitIso` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Over` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.instCategoryOver` `CategoryTheory.Sieve.arrows` `CategoryTheory.Sieve.generate` `presieveOfCoveringAux` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.hom` `SheafCondition.OpensLeCover` `CategoryTheory.ObjectProperty.FullSubcategory.category` `SheafCondition.instCategoryOpensLeCover` `generateEquivalenceOpensLe` `CategoryTheory.eqToIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `generateEquivalenceOpensLe_functor'` `generateEquivalenceOpensLe_inverse'`	—	—
`isSheaf_iff_isSheafOpensLeCover` 📖	mathematical	—	`IsSheaf` `IsSheafOpensLeCover`	—	`IsSheaf.isSheafOpensLeCover` `CategoryTheory.Presheaf.isSheaf_iff_isLimit` `CategoryTheory.Sieve.generate_sieve` `Equiv.nonempty_congr`
`whiskerIsoMapGenerateCocone_hom_hom` 📖	mathematical	`iSup` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice`	`CategoryTheory.Limits.ConeMorphism.hom` `Opposite` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Over` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.instCategoryOver` `CategoryTheory.Sieve.arrows` `CategoryTheory.Sieve.generate` `presieveOfCoveringAux` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.hom` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.comp` `SheafCondition.OpensLeCover` `SheafCondition.instCategoryOpensLeCover` `CategoryTheory.Equivalence.functor` `CategoryTheory.Equivalence.op` `generateEquivalenceOpensLe` `Preorder.toLE` `CategoryTheory.Functor.op` `CategoryTheory.ObjectProperty.ι` `CategoryTheory.Limits.Cone.whisker` `CategoryTheory.Functor.mapCone` `CategoryTheory.Limits.Cocone.op` `SheafCondition.opensLeCoverCocone` `CategoryTheory.Presieve.category` `CategoryTheory.Presieve.diagram` `CategoryTheory.Presieve.cocone` `CategoryTheory.Iso.hom` `CategoryTheory.Limits.Cone` `CategoryTheory.Limits.Cone.category` `whiskerIsoMapGenerateCocone` `CategoryTheory.Functor.map` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.eqToHom` `CategoryTheory.CategoryStruct.opposite` `CategoryTheory.Category.toCategoryStruct`	—	—
`whiskerIsoMapGenerateCocone_inv_hom` 📖	mathematical	`iSup` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice`	`CategoryTheory.Limits.ConeMorphism.hom` `Opposite` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Over` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.instCategoryOver` `CategoryTheory.Sieve.arrows` `CategoryTheory.Sieve.generate` `presieveOfCoveringAux` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.hom` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.comp` `SheafCondition.OpensLeCover` `SheafCondition.instCategoryOpensLeCover` `CategoryTheory.Equivalence.functor` `CategoryTheory.Equivalence.op` `generateEquivalenceOpensLe` `Preorder.toLE` `CategoryTheory.Functor.op` `CategoryTheory.ObjectProperty.ι` `CategoryTheory.Functor.mapCone` `CategoryTheory.Presieve.category` `CategoryTheory.Presieve.diagram` `CategoryTheory.Limits.Cocone.op` `CategoryTheory.Presieve.cocone` `CategoryTheory.Limits.Cone.whisker` `SheafCondition.opensLeCoverCocone` `CategoryTheory.Iso.inv` `CategoryTheory.Limits.Cone` `CategoryTheory.Limits.Cone.category` `whiskerIsoMapGenerateCocone` `CategoryTheory.Functor.map` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.eqToHom` `CategoryTheory.CategoryStruct.opposite` `CategoryTheory.Category.toCategoryStruct`	—	—

TopCat.Presheaf.IsSheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSheafOpensLeCover` 📖	mathematical	`TopCat.Presheaf.IsSheaf`	`CategoryTheory.Limits.IsLimit` `Opposite` `CategoryTheory.ObjectProperty.FullSubcategory` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Preorder.toLE` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `CategoryTheory.ObjectProperty.ι` `CategoryTheory.Functor.mapCone` `CategoryTheory.Limits.Cocone.op` `TopCat.Presheaf.SheafCondition.opensLeCoverCocone`	—	`Equiv.nonempty_congr` `CategoryTheory.Presheaf.isSheaf_iff_isLimit` `TopCat.Presheaf.presieveOfCovering.mem_grothendieckTopology`

TopCat.Presheaf.SheafCondition

Definitions

Name	Category	Theorems
`OpensLeCover` 📖	CompOp	19 math math: `TopCat.Presheaf.generateEquivalenceOpensLe_functor'_obj_obj`, `TopCat.Presheaf.generateEquivalenceOpensLe_unitIso`, `pairwiseToOpensLeCover_map`, `TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_right_as`, `TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_hom`, `pairwiseToOpensLeCover_obj`, `TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom`, `instFinalPairwiseOpensLeCoverPairwiseToOpensLeCover`, `TopCat.Presheaf.generateEquivalenceOpensLe_functor`, `TopCat.Presheaf.generateEquivalenceOpensLe_counitIso`, `Alexandrov.lowerCone_π_app`, `instNonemptyStructuredArrowPairwiseOpensLeCoverPairwiseToOpensLeCover`, `TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom`, `Alexandrov.projSup_obj`, `TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_left`, `TopCat.Presheaf.generateEquivalenceOpensLe_functor'_map`, `TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_map`, `Alexandrov.projSup_map`, `TopCat.Presheaf.generateEquivalenceOpensLe_inverse`
`instCategoryOpensLeCover` 📖	CompOp	19 math math: `TopCat.Presheaf.generateEquivalenceOpensLe_functor'_obj_obj`, `TopCat.Presheaf.generateEquivalenceOpensLe_unitIso`, `pairwiseToOpensLeCover_map`, `TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_right_as`, `TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_hom`, `pairwiseToOpensLeCover_obj`, `TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom`, `instFinalPairwiseOpensLeCoverPairwiseToOpensLeCover`, `TopCat.Presheaf.generateEquivalenceOpensLe_functor`, `TopCat.Presheaf.generateEquivalenceOpensLe_counitIso`, `Alexandrov.lowerCone_π_app`, `instNonemptyStructuredArrowPairwiseOpensLeCoverPairwiseToOpensLeCover`, `TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom`, `Alexandrov.projSup_obj`, `TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_obj_obj_left`, `TopCat.Presheaf.generateEquivalenceOpensLe_functor'_map`, `TopCat.Presheaf.generateEquivalenceOpensLe_inverse'_map`, `Alexandrov.projSup_map`, `TopCat.Presheaf.generateEquivalenceOpensLe_inverse`
`instInhabitedOpensLeCoverOfNonempty` 📖	CompOp	—
`opensLeCoverCocone` 📖	CompOp	3 math math: `TopCat.Presheaf.whiskerIsoMapGenerateCocone_inv_hom`, `TopCat.Presheaf.whiskerIsoMapGenerateCocone_hom_hom`, `TopCat.Presheaf.IsSheaf.isSheafOpensLeCover`

TopCat.Presheaf.SheafCondition.OpensLeCover

Definitions

Name	Category	Theorems
`homToIndex` 📖	CompOp	—
`index` 📖	CompOp	—

---

← Back to Index