Documentation Verification Report

CompleteLattice

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

Statistics

Metric	Count
Definitions	0
Theorems `instIsClosedUnderIsomorphismsISup`, `instIsClosedUnderIsomorphismsMax`, `instIsClosedUnderIsomorphismsMin`, `instIsClosedUnderIsomorphismsTop`, `isoClosure_iSup`, `isoClosure_sup`, `prop_iSup_iff`, `prop_inf_iff`, `prop_sup_iff`, `ι_map_top`	10
Total	10

CategoryTheory.ObjectProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsClosedUnderIsomorphismsISup` 📖	mathematical	`IsClosedUnderIsomorphisms`	`iSup` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.supSet` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Prop.instCompleteLattice`	—	`isoClosure_eq_self` `isoClosure_iSup`
`instIsClosedUnderIsomorphismsMax` 📖	mathematical	—	`IsClosedUnderIsomorphisms` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instMaxForall_mathlib` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Prop.instCompleteLattice`	—	`isoClosure_eq_self` `isoClosure_sup`
`instIsClosedUnderIsomorphismsMin` 📖	mathematical	—	`IsClosedUnderIsomorphisms` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instMinForall_mathlib` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `Prop.instCompleteLattice`	—	`IsClosedUnderIsomorphisms.of_iso`
`instIsClosedUnderIsomorphismsTop` 📖	mathematical	—	`IsClosedUnderIsomorphisms` `Top.top` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra`	—	—
`isoClosure_iSup` 📖	mathematical	—	`isoClosure` `iSup` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.supSet` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Prop.instCompleteLattice`	—	`le_antisymm` `isoClosure_le_iff` `instIsClosedUnderIsomorphismsIsoClosure` `LE.le.trans` `le_iSup` `le_isoClosure`
`isoClosure_sup` 📖	mathematical	—	`isoClosure` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instMaxForall_mathlib` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Prop.instCompleteLattice`	—	`monotone_isoClosure` `le_sup_left` `le_sup_right`
`prop_iSup_iff` 📖	mathematical	—	`iSup` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.supSet` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Prop.instCompleteLattice`	—	`iSup_apply` `iSup_Prop_eq`
`prop_inf_iff` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instMinForall_mathlib` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `Prop.instCompleteLattice`	—	—
`prop_sup_iff` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instMaxForall_mathlib` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Prop.instCompleteLattice`	—	—
`ι_map_top` 📖	mathematical	—	`map` `FullSubcategory` `FullSubcategory.category` `Top.top` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra` `ι` `isoClosure`	—	—

---

← Back to Index