Documentation Verification Report

Equivalence

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

Statistics

Metric	Count
Definitions `congrFullSubcategory`, `topEquivalence`	2
Theorems `congrFullSubcategory_counitIso`, `congrFullSubcategory_functor`, `congrFullSubcategory_inverse`, `congrFullSubcategory_unitIso`, `essSurj_ιOfLE_iff`, `instIsEquivalenceFullSubcategoryIsoClosureιOfLE`, `isEquivalence_ιOfLE_iff`, `topEquivalence_counitIso`, `topEquivalence_functor`, `topEquivalence_inverse`, `topEquivalence_unitIso`	11
Total	13

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
`congrFullSubcategory` 📖	CompOp	4 math math: `congrFullSubcategory_inverse`, `congrFullSubcategory_counitIso`, `congrFullSubcategory_unitIso`, `congrFullSubcategory_functor`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congrFullSubcategory_counitIso` 📖	mathematical	`CategoryTheory.ObjectProperty.inverseImage` `functor`	`counitIso` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `congrFullSubcategory` `CategoryTheory.Functor.FullyFaithful.preimageIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.whiskeringRight` `CategoryTheory.ObjectProperty.ι` `CategoryTheory.Functor.FullyFaithful.whiskeringRight` `CategoryTheory.ObjectProperty.fullyFaithfulι` `CategoryTheory.Functor.comp` `CategoryTheory.ObjectProperty.lift` `inverse` `CategoryTheory.Functor.id` `CategoryTheory.Functor.isoWhiskerLeft`	—	—
`congrFullSubcategory_functor` 📖	mathematical	`CategoryTheory.ObjectProperty.inverseImage` `functor`	`CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `congrFullSubcategory` `CategoryTheory.ObjectProperty.lift` `CategoryTheory.Functor.comp` `CategoryTheory.ObjectProperty.ι`	—	—
`congrFullSubcategory_inverse` 📖	mathematical	`CategoryTheory.ObjectProperty.inverseImage` `functor`	`inverse` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `congrFullSubcategory` `CategoryTheory.ObjectProperty.lift` `CategoryTheory.Functor.comp` `CategoryTheory.ObjectProperty.ι`	—	—
`congrFullSubcategory_unitIso` 📖	mathematical	`CategoryTheory.ObjectProperty.inverseImage` `functor`	`unitIso` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `congrFullSubcategory` `CategoryTheory.Functor.FullyFaithful.preimageIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.whiskeringRight` `CategoryTheory.ObjectProperty.ι` `CategoryTheory.Functor.FullyFaithful.whiskeringRight` `CategoryTheory.ObjectProperty.fullyFaithfulι` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.ObjectProperty.lift` `inverse` `CategoryTheory.Functor.isoWhiskerLeft`	—	—

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
`topEquivalence` 📖	CompOp	4 math math: `topEquivalence_counitIso`, `topEquivalence_unitIso`, `topEquivalence_inverse`, `topEquivalence_functor`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`essSurj_ιOfLE_iff` 📖	mathematical	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le`	`CategoryTheory.Functor.EssSurj` `FullSubcategory` `FullSubcategory.category` `ιOfLE` `isoClosure`	—	`FullSubcategory.property` `full_ι` `faithful_ι`
`instIsEquivalenceFullSubcategoryIsoClosureιOfLE` 📖	mathematical	—	`CategoryTheory.Functor.IsEquivalence` `FullSubcategory` `FullSubcategory.category` `isoClosure` `ιOfLE` `le_isoClosure`	—	`le_isoClosure` `isEquivalence_ιOfLE_iff` `le_refl`
`isEquivalence_ιOfLE_iff` 📖	mathematical	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le`	`CategoryTheory.Functor.IsEquivalence` `FullSubcategory` `FullSubcategory.category` `ιOfLE` `isoClosure`	—	`essSurj_ιOfLE_iff` `CategoryTheory.Functor.IsEquivalence.essSurj` `faithful_ιOfLE` `full_ιOfLE`
`topEquivalence_counitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.counitIso` `FullSubcategory` `Top.top` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra` `FullSubcategory.category` `topEquivalence` `CategoryTheory.Iso.refl` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `lift` `CategoryTheory.Functor.id` `ι`	—	—
`topEquivalence_functor` 📖	mathematical	—	`CategoryTheory.Equivalence.functor` `FullSubcategory` `Top.top` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra` `FullSubcategory.category` `topEquivalence` `ι`	—	—
`topEquivalence_inverse` 📖	mathematical	—	`CategoryTheory.Equivalence.inverse` `FullSubcategory` `Top.top` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra` `FullSubcategory.category` `topEquivalence` `lift` `CategoryTheory.Functor.id`	—	—
`topEquivalence_unitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.unitIso` `FullSubcategory` `Top.top` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra` `FullSubcategory.category` `topEquivalence` `CategoryTheory.Iso.refl` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id`	—	—

---

← Back to Index