Documentation Verification Report

Retract

📁 Source: Mathlib/CategoryTheory/ObjectProperty/Retract.lean

Statistics

Metric	Count
Definitions `IsStableUnderRetracts`, `retractClosure`	2
Theorems `of_retract`, `instEssentiallySmallRetractClosureOfLocallySmall`, `instIsStableUnderRetractsRetractClosure`, `le_retractClosure`, `monotone_retractClosure`, `prop_of_retract`, `prop_retractClosure`, `prop_retractClosure_iff`, `retractClosure_eq_self`, `retractClosure_isoClosure`, `retractClosure_le_iff`	11
Total	13

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
`IsStableUnderRetracts` 📖	CompData	5 math math: `CategoryTheory.instIsStableUnderRetractsIsCardinalPresentable`, `isStableUnderRetracts_colimitsCardinalClosure`, `instIsStableUnderRetractsOfIsClosedUnderColimitsOfShapeWalkingParallelPair`, `CategoryTheory.instIsStableUnderRetractsIsInternallyProjective`, `instIsStableUnderRetractsRetractClosure`
`retractClosure` 📖	CompOp	10 math math: `monotone_retractClosure`, `IsCardinalFilteredGenerator.isPresentable_eq_retractClosure`, `prop_retractClosure_iff`, `retractClosure_eq_self`, `retractClosure_le_iff`, `retractClosure_isoClosure`, `instIsStableUnderRetractsRetractClosure`, `prop_retractClosure`, `le_retractClosure`, `instEssentiallySmallRetractClosureOfLocallySmall`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instEssentiallySmallRetractClosureOfLocallySmall` 📖	mathematical	—	`EssentiallySmall` `retractClosure`	—	`EssentiallySmall.exists_small_le` `CategoryTheory.Category.assoc` `CategoryTheory.Retract.retract_assoc` `instSmallOfObjOfSmall` `small_subtype` `small_sigma` `CategoryTheory.instSmallHomOfLocallySmall` `LE.le.trans` `monotone_retractClosure` `retractClosure_isoClosure` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.Retract.retract` `CategoryTheory.Category.comp_id`
`instIsStableUnderRetractsRetractClosure` 📖	mathematical	—	`IsStableUnderRetracts` `retractClosure`	—	—
`le_retractClosure` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le` `retractClosure`	—	—
`monotone_retractClosure` 📖	mathematical	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le`	`retractClosure`	—	—
`prop_of_retract` 📖	—	—	—	—	`IsStableUnderRetracts.of_retract`
`prop_retractClosure` 📖	mathematical	—	`retractClosure`	—	—
`prop_retractClosure_iff` 📖	mathematical	—	`retractClosure` `CategoryTheory.Retract`	—	—
`retractClosure_eq_self` 📖	mathematical	—	`retractClosure`	—	`le_antisymm` `prop_of_retract` `le_retractClosure`
`retractClosure_isoClosure` 📖	mathematical	—	`retractClosure` `isoClosure`	—	`le_antisymm` `monotone_retractClosure` `le_isoClosure`
`retractClosure_le_iff` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le` `retractClosure`	—	`LE.le.trans` `le_retractClosure` `monotone_retractClosure` `retractClosure_eq_self` `le_refl`

CategoryTheory.ObjectProperty.IsStableUnderRetracts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_retract` 📖	—	—	—	—	—

---

← Back to Index