Documentation Verification Report

Sequential

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

Statistics

Metric	Count
Definitions `Sequential`, `fullyFaithfulSequentialToTop`, `homeoOfIso`, `instCategory`, `instCoeSortType`, `instConcreteCategoryContinuousMapCarrierToTop`, `instInhabited`, `isoEquivHomeo`, `isoOfHomeo`, `of`, `sequentialToTop`, `toTop`	12
Theorems `homeoOfIso_apply`, `homeoOfIso_symm_apply`, `instFaithfulTopCatSequentialToTop`, `instFullTopCatSequentialToTop`, `is_sequential`, `isoEquivHomeo_apply`, `isoEquivHomeo_symm_apply`, `isoOfHomeo_hom`, `isoOfHomeo_inv`, `sequentialToTop_map`, `sequentialToTop_obj`	11
Total	23

Sequential

Definitions

Name	Category	Theorems
`fullyFaithfulSequentialToTop` 📖	CompOp	—
`homeoOfIso` 📖	CompOp	3 math math: `homeoOfIso_apply`, `homeoOfIso_symm_apply`, `isoEquivHomeo_apply`
`instCategory` 📖	CompOp	11 math math: `homeoOfIso_apply`, `homeoOfIso_symm_apply`, `isoEquivHomeo_apply`, `isoEquivHomeo_symm_apply`, `sequentialToTop_obj`, `LightCondSet.instIsIsoFunctorSequentialCounitSequentialAdjunction`, `isoOfHomeo_inv`, `instFaithfulTopCatSequentialToTop`, `sequentialToTop_map`, `isoOfHomeo_hom`, `instFullTopCatSequentialToTop`
`instCoeSortType` 📖	CompOp	—
`instConcreteCategoryContinuousMapCarrierToTop` 📖	CompOp	2 math math: `homeoOfIso_apply`, `homeoOfIso_symm_apply`
`instInhabited` 📖	CompOp	—
`isoEquivHomeo` 📖	CompOp	2 math math: `isoEquivHomeo_apply`, `isoEquivHomeo_symm_apply`
`isoOfHomeo` 📖	CompOp	3 math math: `isoEquivHomeo_symm_apply`, `isoOfHomeo_inv`, `isoOfHomeo_hom`
`of` 📖	CompOp	—
`sequentialToTop` 📖	CompOp	4 math math: `sequentialToTop_obj`, `instFaithfulTopCatSequentialToTop`, `sequentialToTop_map`, `instFullTopCatSequentialToTop`
`toTop` 📖	CompOp	9 math math: `homeoOfIso_apply`, `homeoOfIso_symm_apply`, `isoEquivHomeo_apply`, `isoEquivHomeo_symm_apply`, `sequentialToTop_obj`, `isoOfHomeo_inv`, `sequentialToTop_map`, `isoOfHomeo_hom`, `is_sequential`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homeoOfIso_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `TopCat.carrier` `toTop` `TopCat.str` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `homeoOfIso` `CategoryTheory.ConcreteCategory.hom` `Sequential` `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` `Sequential` `instCategory` `ContinuousMap` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrierToTop` `CategoryTheory.Iso.inv`	—	—
`instFaithfulTopCatSequentialToTop` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `Sequential` `instCategory` `TopCat` `TopCat.instCategory` `sequentialToTop`	—	`CategoryTheory.InducedCategory.faithful`
`instFullTopCatSequentialToTop` 📖	mathematical	—	`CategoryTheory.Functor.Full` `Sequential` `instCategory` `TopCat` `TopCat.instCategory` `sequentialToTop`	—	`CategoryTheory.InducedCategory.full`
`is_sequential` 📖	mathematical	—	`SequentialSpace` `TopCat.carrier` `toTop` `TopCat.str`	—	—
`isoEquivHomeo_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.Iso` `Sequential` `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` `Sequential` `instCategory` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `isoEquivHomeo` `isoOfHomeo`	—	—
`isoOfHomeo_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `Sequential` `instCategory` `isoOfHomeo` `CategoryTheory.InducedCategory.homMk` `TopCat` `TopCat.instCategory` `toTop` `TopCat.ofHom` `TopCat.carrier` `TopCat.str` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	—
`isoOfHomeo_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `Sequential` `instCategory` `isoOfHomeo` `CategoryTheory.InducedCategory.homMk` `TopCat` `TopCat.instCategory` `toTop` `TopCat.ofHom` `TopCat.carrier` `TopCat.str` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm`	—	—
`sequentialToTop_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `Sequential` `instCategory` `TopCat` `TopCat.instCategory` `sequentialToTop` `CategoryTheory.InducedCategory.Hom.hom` `toTop`	—	—
`sequentialToTop_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Sequential` `instCategory` `TopCat` `TopCat.instCategory` `sequentialToTop` `toTop`	—	—

(root)

Definitions

Name	Category	Theorems
`Sequential` 📖	CompData	11 math math: `Sequential.homeoOfIso_apply`, `Sequential.homeoOfIso_symm_apply`, `Sequential.isoEquivHomeo_apply`, `Sequential.isoEquivHomeo_symm_apply`, `Sequential.sequentialToTop_obj`, `LightCondSet.instIsIsoFunctorSequentialCounitSequentialAdjunction`, `Sequential.isoOfHomeo_inv`, `Sequential.instFaithfulTopCatSequentialToTop`, `Sequential.sequentialToTop_map`, `Sequential.isoOfHomeo_hom`, `Sequential.instFullTopCatSequentialToTop`

---

← Back to Index