Over

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

Statistics

Metric	Count
Definitions overEquivalence	1
Theorems coe_overEquivalence_functor_obj, coe_overEquivalence_inverse_obj_left, overEquivalence_counitIso_hom_app, overEquivalence_counitIso_inv_app, overEquivalence_inverse_obj_right_as, overEquivalence_unitIso_hom_app_left, overEquivalence_unitIso_inv_app_left	7
Total	8

TopologicalSpace.Opens

Definitions

Name	Category	Theorems
overEquivalence 📖	CompOp	7 math math: coe_overEquivalence_functor_obj, overEquivalence_unitIso_hom_app_left, overEquivalence_counitIso_inv_app, overEquivalence_unitIso_inv_app_left, coe_overEquivalence_inverse_obj_left, overEquivalence_inverse_obj_right_as, overEquivalence_counitIso_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_overEquivalence_functor_obj 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens SetLike.instMembership instSetLike instTopologicalSpaceSubtype CategoryTheory.Functor.obj CategoryTheory.Over Preorder.smallCategory PartialOrder.toPreorder instPartialOrder CategoryTheory.instCategoryOver CategoryTheory.Equivalence.functor overEquivalence Set.preimage CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit	—	—
coe_overEquivalence_inverse_obj_left 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens instSetLike CategoryTheory.Comma.left Preorder.smallCategory PartialOrder.toPreorder instPartialOrder CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj SetLike.instMembership instTopologicalSpaceSubtype CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Equivalence.inverse overEquivalence Set.image	—	—
overEquivalence_counitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app TopologicalSpace.Opens SetLike.instMembership instSetLike instTopologicalSpaceSubtype Preorder.smallCategory PartialOrder.toPreorder instPartialOrder CategoryTheory.Functor.comp CategoryTheory.Over CategoryTheory.instCategoryOver Set.image SetLike.coe CategoryTheory.homOfLE CategoryTheory.Over.homMk CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit Set.preimage CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso overEquivalence CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct	—	—
overEquivalence_counitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app TopologicalSpace.Opens SetLike.instMembership instSetLike instTopologicalSpaceSubtype Preorder.smallCategory PartialOrder.toPreorder instPartialOrder CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Over CategoryTheory.instCategoryOver Set.image SetLike.coe CategoryTheory.homOfLE CategoryTheory.Over.homMk CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Set.preimage CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso overEquivalence CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct	—	—
overEquivalence_inverse_obj_right_as 📖	mathematical	—	CategoryTheory.Discrete.as CategoryTheory.Comma.right TopologicalSpace.Opens Preorder.smallCategory PartialOrder.toPreorder instPartialOrder CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj SetLike.instMembership instSetLike instTopologicalSpaceSubtype CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Equivalence.inverse overEquivalence	—	—
overEquivalence_unitIso_hom_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left TopologicalSpace.Opens Preorder.smallCategory PartialOrder.toPreorder instPartialOrder CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.comp SetLike.instMembership instSetLike instTopologicalSpaceSubtype Set.preimage SetLike.coe CategoryTheory.Comma.left CategoryTheory.homOfLE Set.image CategoryTheory.Over.homMk CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso overEquivalence CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct	—	—
overEquivalence_unitIso_inv_app_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left TopologicalSpace.Opens Preorder.smallCategory PartialOrder.toPreorder instPartialOrder CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Functor.comp SetLike.instMembership instSetLike instTopologicalSpaceSubtype Set.preimage SetLike.coe CategoryTheory.Comma.left CategoryTheory.homOfLE Set.image CategoryTheory.Over.homMk CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso overEquivalence CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct	—	—

---

← Back to Index