Documentation Verification Report

Terminal

📁 Source: Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean

Statistics

Metric	Count
Definitions `isInitialIffObj`, `isInitialObj`, `isInitialOfObj`, `isTerminalIffObj`, `isTerminalObj`, `isTerminalOfObj`, `iso`, `iso`, `isColimitMapCoconeEmptyCoconeEquiv`, `isColimitOfHasInitialOfPreservesColimit`, `isLimitMapConeEmptyConeEquiv`, `isLimitOfHasTerminalOfPreservesLimit`	12
Theorems `iso_hom`, `of_iso_comparison`, `iso_hom`, `of_iso_comparison`, `hasInitial_of_hasInitial_of_preservesColimit`, `hasTerminal_of_hasTerminal_of_preservesLimit`, `instIsIsoInitialComparison`, `instIsIsoTerminalComparison`, `preservesColimitsOfShape_pempty_of_preservesInitial`, `preservesInitial_of_isIso`, `preservesInitial_of_iso`, `preservesLimitsOfShape_pempty_of_preservesTerminal`, `preservesTerminal_of_isIso`, `preservesTerminal_of_iso`	14
Total	26

CategoryTheory.Limits

Definitions

Name	Category	Theorems
`isColimitMapCoconeEmptyCoconeEquiv` 📖	CompOp	—
`isColimitOfHasInitialOfPreservesColimit` 📖	CompOp	—
`isLimitMapConeEmptyConeEquiv` 📖	CompOp	—
`isLimitOfHasTerminalOfPreservesLimit` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasInitial_of_hasInitial_of_preservesColimit` 📖	mathematical	—	`HasInitial`	—	`hasColimit_of_iso`
`hasTerminal_of_hasTerminal_of_preservesLimit` 📖	mathematical	—	`HasTerminal`	—	`hasLimit_of_iso`
`instIsIsoInitialComparison` 📖	mathematical	—	`CategoryTheory.IsIso` `initial` `CategoryTheory.Functor.obj` `initialComparison`	—	`PreservesInitial.iso_hom` `CategoryTheory.Iso.isIso_inv`
`instIsIsoTerminalComparison` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `terminal` `terminalComparison`	—	`PreservesTerminal.iso_hom` `CategoryTheory.Iso.isIso_hom`
`preservesColimitsOfShape_pempty_of_preservesInitial` 📖	mathematical	—	`PreservesColimitsOfShape` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory`	—	`preservesColimit_of_iso_diagram`
`preservesInitial_of_isIso` 📖	mathematical	—	`PreservesColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.empty`	—	`PreservesInitial.of_iso_comparison` `Unique.instSubsingleton`
`preservesInitial_of_iso` 📖	mathematical	—	`PreservesColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.empty`	—	`preservesInitial_of_isIso` `CategoryTheory.Iso.isIso_hom`
`preservesLimitsOfShape_pempty_of_preservesTerminal` 📖	mathematical	—	`PreservesLimitsOfShape` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory`	—	`preservesLimit_of_iso_diagram`
`preservesTerminal_of_isIso` 📖	mathematical	—	`PreservesLimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.empty`	—	`PreservesTerminal.of_iso_comparison` `Unique.instSubsingleton`
`preservesTerminal_of_iso` 📖	mathematical	—	`PreservesLimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.empty`	—	`preservesTerminal_of_isIso` `CategoryTheory.Iso.isIso_hom`

CategoryTheory.Limits.IsInitial

Definitions

Name	Category	Theorems
`isInitialIffObj` 📖	CompOp	—
`isInitialObj` 📖	CompOp	—
`isInitialOfObj` 📖	CompOp	—

CategoryTheory.Limits.IsTerminal

Definitions

Name	Category	Theorems
`isTerminalIffObj` 📖	CompOp	—
`isTerminalObj` 📖	CompOp	—
`isTerminalOfObj` 📖	CompOp	—

CategoryTheory.Limits.PreservesInitial

Definitions

Name	Category	Theorems
`iso` 📖	CompOp	1 math math: `iso_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iso_hom` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.initial` `iso` `CategoryTheory.Limits.initialComparison`	—	—
`of_iso_comparison` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.empty`	—	`CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape`

CategoryTheory.Limits.PreservesTerminal

Definitions

Name	Category	Theorems
`iso` 📖	CompOp	1 math math: `iso_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.terminal` `iso` `CategoryTheory.Limits.terminalComparison`	—	—
`of_iso_comparison` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.empty`	—	`CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape`

---

← Back to Index