Documentation Verification Report

CompactlyGenerated

📁 Source: Mathlib/Topology/Category/CompactlyGenerated.lean

Statistics

Metric	Count
Definitions `compactlyGeneratedToTop`, `fullyFaithfulCompactlyGeneratedToTop`, `homeoOfIso`, `instCategory`, `instCoeSortType`, `instConcreteCategoryContinuousMapCarrierToTop`, `instInhabited`, `isoEquivHomeo`, `isoOfHomeo`, `of`, `ofHom`, `toTop`	12
Theorems `compactlyGeneratedToTop_map`, `compactlyGeneratedToTop_obj`, `homeoOfIso_apply`, `homeoOfIso_symm_apply`, `instFaithfulTopCatCompactlyGeneratedToTop`, `instFullTopCatCompactlyGeneratedToTop`, `is_compactly_generated`, `isoEquivHomeo_apply`, `isoEquivHomeo_symm_apply`, `isoOfHomeo_hom`, `isoOfHomeo_inv`	11
Total	23

CompactlyGenerated

Definitions

Name	Category	Theorems
`compactlyGeneratedToTop` 📖	CompOp	4 math math: `compactlyGeneratedToTop_obj`, `compactlyGeneratedToTop_map`, `instFullTopCatCompactlyGeneratedToTop`, `instFaithfulTopCatCompactlyGeneratedToTop`
`fullyFaithfulCompactlyGeneratedToTop` 📖	CompOp	—
`homeoOfIso` 📖	CompOp	3 math math: `homeoOfIso_apply`, `homeoOfIso_symm_apply`, `isoEquivHomeo_apply`
`instCategory` 📖	CompOp	11 math math: `homeoOfIso_apply`, `CondensedSet.instIsIsoFunctorCompactlyGeneratedCounitCompactlyGeneratedAdjunction`, `compactlyGeneratedToTop_obj`, `compactlyGeneratedToTop_map`, `isoOfHomeo_hom`, `isoOfHomeo_inv`, `homeoOfIso_symm_apply`, `isoEquivHomeo_symm_apply`, `isoEquivHomeo_apply`, `instFullTopCatCompactlyGeneratedToTop`, `instFaithfulTopCatCompactlyGeneratedToTop`
`instCoeSortType` 📖	CompOp	—
`instConcreteCategoryContinuousMapCarrierToTop` 📖	CompOp	2 math math: `homeoOfIso_apply`, `homeoOfIso_symm_apply`
`instInhabited` 📖	CompOp	—
`isoEquivHomeo` 📖	CompOp	2 math math: `isoEquivHomeo_symm_apply`, `isoEquivHomeo_apply`
`isoOfHomeo` 📖	CompOp	3 math math: `isoOfHomeo_hom`, `isoOfHomeo_inv`, `isoEquivHomeo_symm_apply`
`of` 📖	CompOp	—
`ofHom` 📖	CompOp	2 math math: `isoOfHomeo_hom`, `isoOfHomeo_inv`
`toTop` 📖	CompOp	9 math math: `homeoOfIso_apply`, `compactlyGeneratedToTop_obj`, `compactlyGeneratedToTop_map`, `isoOfHomeo_hom`, `isoOfHomeo_inv`, `homeoOfIso_symm_apply`, `is_compactly_generated`, `isoEquivHomeo_symm_apply`, `isoEquivHomeo_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compactlyGeneratedToTop_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CompactlyGenerated` `instCategory` `TopCat` `TopCat.instCategory` `compactlyGeneratedToTop` `CategoryTheory.InducedCategory.Hom.hom` `toTop`	—	—
`compactlyGeneratedToTop_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CompactlyGenerated` `instCategory` `TopCat` `TopCat.instCategory` `compactlyGeneratedToTop` `toTop`	—	—
`homeoOfIso_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `TopCat.carrier` `toTop` `TopCat.str` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `homeoOfIso` `CategoryTheory.ConcreteCategory.hom` `CompactlyGenerated` `instCategory` `ContinuousMap` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrierToTop` `CategoryTheory.Iso.hom`	—	—
`homeoOfIso_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `TopCat.carrier` `toTop` `TopCat.str` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `homeoOfIso` `CategoryTheory.ConcreteCategory.hom` `CompactlyGenerated` `instCategory` `ContinuousMap` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrierToTop` `CategoryTheory.Iso.inv`	—	—
`instFaithfulTopCatCompactlyGeneratedToTop` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CompactlyGenerated` `instCategory` `TopCat` `TopCat.instCategory` `compactlyGeneratedToTop`	—	`CategoryTheory.Functor.FullyFaithful.faithful`
`instFullTopCatCompactlyGeneratedToTop` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CompactlyGenerated` `instCategory` `TopCat` `TopCat.instCategory` `compactlyGeneratedToTop`	—	`CategoryTheory.Functor.FullyFaithful.full`
`is_compactly_generated` 📖	mathematical	—	`UCompactlyGeneratedSpace` `TopCat.carrier` `toTop` `TopCat.str`	—	—
`isoEquivHomeo_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.Iso` `CompactlyGenerated` `instCategory` `Homeomorph` `TopCat.carrier` `toTop` `TopCat.str` `EquivLike.toFunLike` `Equiv.instEquivLike` `isoEquivHomeo` `homeoOfIso`	—	—
`isoEquivHomeo_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Homeomorph` `TopCat.carrier` `toTop` `TopCat.str` `CategoryTheory.Iso` `CompactlyGenerated` `instCategory` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `isoEquivHomeo` `isoOfHomeo`	—	—
`isoOfHomeo_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CompactlyGenerated` `instCategory` `isoOfHomeo` `ofHom` `TopCat.carrier` `TopCat.str` `is_compactly_generated` `DFunLike.coe` `Homeomorph` `toTop` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`is_compactly_generated`
`isoOfHomeo_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CompactlyGenerated` `instCategory` `isoOfHomeo` `ofHom` `TopCat.carrier` `TopCat.str` `is_compactly_generated` `DFunLike.coe` `Homeomorph` `toTop` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm`	—	`is_compactly_generated`

---

← Back to Index