Documentation Verification Report

MayerVietoris

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

Statistics

Metric	Count
Definitions `mayerVietorisSquare`, `mayerVietorisSquare'`	2
Theorems `coe_mayerVietorisSquare_X₁`, `coe_mayerVietorisSquare_X₄`, `mayerVietorisSquare'_toSquare`, `mayerVietorisSquare_X₂`, `mayerVietorisSquare_X₃`	5
Total	7

Opens

Definitions

Name	Category	Theorems
`mayerVietorisSquare` 📖	CompOp	4 math math: `mayerVietorisSquare_X₃`, `mayerVietorisSquare_X₂`, `coe_mayerVietorisSquare_X₁`, `coe_mayerVietorisSquare_X₄`
`mayerVietorisSquare'` 📖	CompOp	1 math math: `mayerVietorisSquare'_toSquare`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mayerVietorisSquare_X₁` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Opens` `TopologicalSpace.Opens.instSetLike` `CategoryTheory.Square.X₁` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toSquare` `grothendieckTopology` `CategoryTheory.sheafToPresheaf_isRightAdjoint` `CategoryTheory.types` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Types.instFunLike` `CategoryTheory.Types.instConcreteCategory` `CategoryTheory.Functor.corepresentable_preservesLimitsOfShape` `CategoryTheory.forget` `CategoryTheory.Types.instIsCorepresentableForgetTypeHom` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.GrothendieckTopology.Cover.shape` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.Types.hasLimit` `UnivLE.small` `UnivLE.self` `CategoryTheory.Limits.MulticospanIndex.multicospan` `CategoryTheory.GrothendieckTopology.Cover.index` `CategoryTheory.Limits.Types.hasColimitsOfShape` `Opposite` `CategoryTheory.GrothendieckTopology.Cover` `CategoryTheory.Category.opposite` `CategoryTheory.GrothendieckTopology.instPreorderCover` `Opposite.small` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Types.instIsEquivalenceForgetTypeHom` `CategoryTheory.instReflectsIsomorphismsForgetTypeHom` `mayerVietorisSquare` `Set` `Set.instInter`	—	`CategoryTheory.sheafToPresheaf_isRightAdjoint` `CategoryTheory.Functor.corepresentable_preservesLimitsOfShape` `CategoryTheory.Types.instIsCorepresentableForgetTypeHom` `CategoryTheory.Limits.Types.hasLimit` `UnivLE.small` `UnivLE.self` `CategoryTheory.Limits.Types.hasColimitsOfShape` `Opposite.small` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Types.instIsEquivalenceForgetTypeHom` `CategoryTheory.instReflectsIsomorphismsForgetTypeHom`
`coe_mayerVietorisSquare_X₄` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Opens` `TopologicalSpace.Opens.instSetLike` `CategoryTheory.Square.X₄` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toSquare` `grothendieckTopology` `CategoryTheory.sheafToPresheaf_isRightAdjoint` `CategoryTheory.types` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Types.instFunLike` `CategoryTheory.Types.instConcreteCategory` `CategoryTheory.Functor.corepresentable_preservesLimitsOfShape` `CategoryTheory.forget` `CategoryTheory.Types.instIsCorepresentableForgetTypeHom` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.GrothendieckTopology.Cover.shape` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.Types.hasLimit` `UnivLE.small` `UnivLE.self` `CategoryTheory.Limits.MulticospanIndex.multicospan` `CategoryTheory.GrothendieckTopology.Cover.index` `CategoryTheory.Limits.Types.hasColimitsOfShape` `Opposite` `CategoryTheory.GrothendieckTopology.Cover` `CategoryTheory.Category.opposite` `CategoryTheory.GrothendieckTopology.instPreorderCover` `Opposite.small` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Types.instIsEquivalenceForgetTypeHom` `CategoryTheory.instReflectsIsomorphismsForgetTypeHom` `mayerVietorisSquare` `Set` `Set.instUnion`	—	`CategoryTheory.sheafToPresheaf_isRightAdjoint` `CategoryTheory.Functor.corepresentable_preservesLimitsOfShape` `CategoryTheory.Types.instIsCorepresentableForgetTypeHom` `CategoryTheory.Limits.Types.hasLimit` `UnivLE.small` `UnivLE.self` `CategoryTheory.Limits.Types.hasColimitsOfShape` `Opposite.small` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Types.instIsEquivalenceForgetTypeHom` `CategoryTheory.instReflectsIsomorphismsForgetTypeHom`
`mayerVietorisSquare'_toSquare` 📖	mathematical	`CategoryTheory.Square.X₄` `TopologicalSpace.Opens` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `CategoryTheory.Square.X₂` `CategoryTheory.Square.X₃` `CategoryTheory.Square.X₁` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	`CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toSquare` `grothendieckTopology` `CategoryTheory.sheafToPresheaf_isRightAdjoint` `CategoryTheory.types` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Types.instFunLike` `CategoryTheory.Types.instConcreteCategory` `CategoryTheory.Functor.corepresentable_preservesLimitsOfShape` `CategoryTheory.forget` `CategoryTheory.Types.instIsCorepresentableForgetTypeHom` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.GrothendieckTopology.Cover.shape` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.Types.hasLimit` `UnivLE.small` `UnivLE.self` `CategoryTheory.Limits.MulticospanIndex.multicospan` `CategoryTheory.GrothendieckTopology.Cover.index` `CategoryTheory.Limits.Types.hasColimitsOfShape` `Opposite` `CategoryTheory.GrothendieckTopology.Cover` `CategoryTheory.Category.opposite` `CategoryTheory.GrothendieckTopology.instPreorderCover` `Opposite.small` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Types.instIsEquivalenceForgetTypeHom` `CategoryTheory.instReflectsIsomorphismsForgetTypeHom` `mayerVietorisSquare'`	—	`CategoryTheory.sheafToPresheaf_isRightAdjoint` `CategoryTheory.Functor.corepresentable_preservesLimitsOfShape` `CategoryTheory.Types.instIsCorepresentableForgetTypeHom` `CategoryTheory.Limits.Types.hasLimit` `UnivLE.small` `UnivLE.self` `CategoryTheory.Limits.Types.hasColimitsOfShape` `Opposite.small` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Types.instIsEquivalenceForgetTypeHom` `CategoryTheory.instReflectsIsomorphismsForgetTypeHom`
`mayerVietorisSquare_X₂` 📖	mathematical	—	`CategoryTheory.Square.X₂` `TopologicalSpace.Opens` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toSquare` `grothendieckTopology` `CategoryTheory.sheafToPresheaf_isRightAdjoint` `CategoryTheory.types` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Types.instFunLike` `CategoryTheory.Types.instConcreteCategory` `CategoryTheory.Functor.corepresentable_preservesLimitsOfShape` `CategoryTheory.forget` `CategoryTheory.Types.instIsCorepresentableForgetTypeHom` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.GrothendieckTopology.Cover.shape` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.Types.hasLimit` `UnivLE.small` `UnivLE.self` `CategoryTheory.Limits.MulticospanIndex.multicospan` `CategoryTheory.GrothendieckTopology.Cover.index` `CategoryTheory.Limits.Types.hasColimitsOfShape` `Opposite` `CategoryTheory.GrothendieckTopology.Cover` `CategoryTheory.Category.opposite` `CategoryTheory.GrothendieckTopology.instPreorderCover` `Opposite.small` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Types.instIsEquivalenceForgetTypeHom` `CategoryTheory.instReflectsIsomorphismsForgetTypeHom` `mayerVietorisSquare`	—	`CategoryTheory.sheafToPresheaf_isRightAdjoint` `CategoryTheory.Functor.corepresentable_preservesLimitsOfShape` `CategoryTheory.Types.instIsCorepresentableForgetTypeHom` `CategoryTheory.Limits.Types.hasLimit` `UnivLE.small` `UnivLE.self` `CategoryTheory.Limits.Types.hasColimitsOfShape` `Opposite.small` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Types.instIsEquivalenceForgetTypeHom` `CategoryTheory.instReflectsIsomorphismsForgetTypeHom`
`mayerVietorisSquare_X₃` 📖	mathematical	—	`CategoryTheory.Square.X₃` `TopologicalSpace.Opens` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toSquare` `grothendieckTopology` `CategoryTheory.sheafToPresheaf_isRightAdjoint` `CategoryTheory.types` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Types.instFunLike` `CategoryTheory.Types.instConcreteCategory` `CategoryTheory.Functor.corepresentable_preservesLimitsOfShape` `CategoryTheory.forget` `CategoryTheory.Types.instIsCorepresentableForgetTypeHom` `CategoryTheory.Limits.WalkingMulticospan` `CategoryTheory.GrothendieckTopology.Cover.shape` `CategoryTheory.Limits.WalkingMulticospan.instSmallCategory` `CategoryTheory.Limits.Types.hasLimit` `UnivLE.small` `UnivLE.self` `CategoryTheory.Limits.MulticospanIndex.multicospan` `CategoryTheory.GrothendieckTopology.Cover.index` `CategoryTheory.Limits.Types.hasColimitsOfShape` `Opposite` `CategoryTheory.GrothendieckTopology.Cover` `CategoryTheory.Category.opposite` `CategoryTheory.GrothendieckTopology.instPreorderCover` `Opposite.small` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Types.instIsEquivalenceForgetTypeHom` `CategoryTheory.instReflectsIsomorphismsForgetTypeHom` `mayerVietorisSquare`	—	`CategoryTheory.sheafToPresheaf_isRightAdjoint` `CategoryTheory.Functor.corepresentable_preservesLimitsOfShape` `CategoryTheory.Types.instIsCorepresentableForgetTypeHom` `CategoryTheory.Limits.Types.hasLimit` `UnivLE.small` `UnivLE.self` `CategoryTheory.Limits.Types.hasColimitsOfShape` `Opposite.small` `CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint` `CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence` `CategoryTheory.Types.instIsEquivalenceForgetTypeHom` `CategoryTheory.instReflectsIsomorphismsForgetTypeHom`

---

← Back to Index