Documentation Verification Report

OfObjectProperty

📁 Source: Mathlib/CategoryTheory/MorphismProperty/OfObjectProperty.lean

Statistics

Metric	Count
Definitions `ofObjectProperty`	1
Theorems `instRespectsLeftOfObjectPropertyIsomorphismsOfIsClosedUnderIsomorphisms`, `instRespectsRightOfObjectPropertyIsomorphismsOfIsClosedUnderIsomorphisms`, `monotone_ofObjectProperty_left`, `monotone_ofObjectProperty_right`, `ofObjectProperty_iff`, `ofObjectProperty_inverseImage`, `ofObjectProperty_map_le`	7
Total	8

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
`ofObjectProperty` 📖	CompOp	11 math math: `CategoryTheory.ObjectProperty.IsClosedUnderKernels.kernels_le`, `CategoryTheory.ObjectProperty.IsClosedUnderCokernels.cokernels_le`, `CategoryTheory.ObjectProperty.isClosedUnderCokernels_iff`, `instRespectsRightOfObjectPropertyIsomorphismsOfIsClosedUnderIsomorphisms`, `ofObjectProperty_iff`, `monotone_ofObjectProperty_left`, `ofObjectProperty_inverseImage`, `instRespectsLeftOfObjectPropertyIsomorphismsOfIsClosedUnderIsomorphisms`, `CategoryTheory.ObjectProperty.isClosedUnderKernels_iff`, `ofObjectProperty_map_le`, `monotone_ofObjectProperty_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instRespectsLeftOfObjectPropertyIsomorphismsOfIsClosedUnderIsomorphisms` 📖	mathematical	—	`RespectsLeft` `CategoryTheory.Category.toCategoryStruct` `ofObjectProperty` `isomorphisms`	—	`CategoryTheory.ObjectProperty.prop_iff_of_isIso` `isomorphisms.iff`
`instRespectsRightOfObjectPropertyIsomorphismsOfIsClosedUnderIsomorphisms` 📖	mathematical	—	`RespectsRight` `CategoryTheory.Category.toCategoryStruct` `ofObjectProperty` `isomorphisms`	—	`CategoryTheory.ObjectProperty.prop_iff_of_isIso` `isomorphisms.iff`
`monotone_ofObjectProperty_left` 📖	mathematical	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le`	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `ofObjectProperty`	—	—
`monotone_ofObjectProperty_right` 📖	mathematical	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le`	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `ofObjectProperty`	—	—
`ofObjectProperty_iff` 📖	mathematical	—	`ofObjectProperty`	—	—
`ofObjectProperty_inverseImage` 📖	mathematical	—	`ofObjectProperty` `CategoryTheory.ObjectProperty.inverseImage` `inverseImage`	—	—
`ofObjectProperty_map_le` 📖	mathematical	—	`CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `instCompleteBooleanAlgebra` `map` `ofObjectProperty` `CategoryTheory.ObjectProperty.map`	—	—

---

← Back to Index